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

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.  *)