Commit 089ad9e8 authored by Michael Sammler's avatar Michael Sammler
Browse files

use check_injection_tac also in normalize_and_simpl_goal

parent 8b923b0b
Pipeline #55216 passed with stage
in 31 minutes and 21 seconds
...@@ -561,10 +561,6 @@ Ltac liFalse := ...@@ -561,10 +561,6 @@ Ltac liFalse :=
| |- False => li_shelve_sidecond | |- False => li_shelve_sidecond
end. end.
(* There can be some goals where one should not call injection on an
hypothesis that is introduced. The [li_impl_check_injection_tac] hook
allows the client to customize this. *)
Ltac li_impl_check_injection_tac := idtac.
Ltac liImpl := Ltac liImpl :=
lazymatch goal with lazymatch goal with
(* relying on the fact that unification variables cannot contain (* relying on the fact that unification variables cannot contain
...@@ -587,8 +583,9 @@ Ltac liImpl := ...@@ -587,8 +583,9 @@ Ltac liImpl :=
| |- false = false -> ?P _ => move => _; | |- false = false -> ?P _ => move => _;
match P with match P with
| _, _ => fail 1 "handled by do_forall" | _, _ => fail 1 "handled by do_forall"
| _ = _ => li_impl_check_injection_tac; | _ = _ =>
let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi check_injection_tac;
let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi
| _ => check_hyp_not_exists P; intros ?; subst | _ => check_hyp_not_exists P; intros ?; subst
| _ => move => _ | _ => move => _
end end
......
...@@ -91,7 +91,9 @@ Ltac normalize_and_simpl_goal_step := ...@@ -91,7 +91,9 @@ Ltac normalize_and_simpl_goal_step :=
| |- false = false -> ?P _ => move => _; | |- false = false -> ?P _ => move => _;
match P with match P with
| _, _ => case | _, _ => case
| _ = _ => let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi | _ = _ =>
check_injection_tac;
let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi
| _ => check_hyp_not_exists P; intros ?; subst | _ => check_hyp_not_exists P; intros ?; subst
| _ => move => _ | _ => move => _
end end
......
...@@ -6,6 +6,11 @@ Global Hint Extern 10 (CanSolve ?P) => (change P; can_solve_tac) : typeclass_ins ...@@ -6,6 +6,11 @@ Global Hint Extern 10 (CanSolve ?P) => (change P; can_solve_tac) : typeclass_ins
Ltac sidecond_hook := idtac. Ltac sidecond_hook := idtac.
Ltac unsolved_sidecond_hook := idtac. Ltac unsolved_sidecond_hook := idtac.
(* There can be some goals where one should not call injection on an
hypothesis that is introduced. The [check_injection_tac] hook is called
before injection and allows the client to customize this. *)
Ltac check_injection_tac := idtac.
(** * general normalization infrastructure *) (** * general normalization infrastructure *)
Ltac normalize_tac := fail "provide a normalize_tac!". Ltac normalize_tac := fail "provide a normalize_tac!".
Lemma tac_normalize_goal (P1 P2 : Prop): Lemma tac_normalize_goal (P1 P2 : Prop):
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment