aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-28 05:08:08 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-28 05:08:08 +0000
commit3f6196a6bdc7e5b0e6d8279a7b7b0de74faa3492 (patch)
treec87f3b728a904dcfa655982ee82255b82c8a825c /theories
parent0bfefe15d6c174c60cc0eb50a54254c20228f30e (diff)
Fix simplification of ind. hyps., recognized by a [block] in their type (bug #2674) and properly clear [block] at end of simplification (bug #2691).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14948 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Program/Equality.v26
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. *)