diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Program/Equality.v | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 06ff7cd10..d9d0073be 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -28,7 +28,7 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. Definition block {A : Type} (a : A) := a. Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. -Ltac unblock_goal := cbv beta delta [block]. +Ltac unblock_goal := unfold block in *. (** Notation for heterogenous equality. *) @@ -214,7 +214,8 @@ Ltac simplify_eqs := Ltac simplify_IH_hyps := repeat match goal with - | [ hyp : _ |- _ ] => specialize_eqs hyp + | [ hyp : context [ block _ ] |- _ ] => + specialize_eqs hyp end. (** We split substitution tactics in the two directions depending on which @@ -377,14 +378,23 @@ Ltac is_introduced H := end. Tactic Notation "intro_block" hyp(H) := - (is_introduced H ; block_goal ; revert_until H) || + (is_introduced H ; block_goal ; revert_until H ; block_goal) || (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). Tactic Notation "intro_block_id" ident(H) := - (is_introduced H ; block_goal ; revert_until H) || + (is_introduced H ; block_goal ; revert_until H; block_goal) || (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). -Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. +Ltac unblock_dep_elim := + match goal with + | |- block ?T => + match T with context [ block _ ] => + unfold block at 1 ; intros ; unblock_goal + end + | _ => unblock_goal + end. + +Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_dep_elim. Ltac do_intros H := (try intros until H) ; (intro_block_id H || intro_block H). @@ -395,7 +405,7 @@ Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim. Ltac do_depind tac H := (try intros until H) ; intro_block H ; - generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. + generalize_eqs_vars H ; tac H ; simpl_dep_elim. (** To dependent elimination on some hyp. *) @@ -412,8 +422,8 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id. (** A variant where generalized variables should be given by the user. *) Ltac do_depelim' rev tac H := - (try intros until H) ; block_goal ; rev H ; generalize_eqs H ; tac H ; simplify_dep_elim ; - simplify_IH_hyps ; unblock_goal. + (try intros until H) ; block_goal ; rev H ; + (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim. (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices. *) |