Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing zeta reductions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14564 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 62 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/shouldsucceed/2456.v
new file mode 100644
index 000000000..56f046c4d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2456.v
@@ -0,0 +1,53 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+    := MkCatch : forall (p : Patch from to),
+                 Catch from to.
+Implicit Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+        : forall {from mid1 mid2 to : nat},
+          Catch from mid1
+       -> Catch mid1 to
+       -> Catch from mid2
+       -> Catch mid2 to
+       -> Prop
+     := MkCatchCommute5 :
+           forall {from mid1 mid2 to : nat}
+                  (p : Patch from mid1)
+                  (q : Patch mid1 to)
+                  (q' : Patch from mid2)
+                  (p' : Patch mid2 to),
+           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+                       (p : Catch from mid1)
+                       (q : Catch mid1 to)
+                       (q' : Catch from mid2)
+                       (p' : Catch mid2 to)
+                     : Prop
+    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+                         CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+    := (CatchCommute p q q' p')
+    (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+      forall {from mid mid' to : nat}
+             {p   : Catch from mid}  {q   : Catch mid  to}
+             {q'  : Catch from mid'} {p'  : Catch mid' to}
+             {q'' : Catch from mid'} {p'' : Catch mid' to}
+             (commute1 : <<p, q>> <~> <<q', p'>>)
+             (commute2 : <<p, q>> <~> <<q'', p''>>),
+      (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+Admitted.
\ No newline at end of file
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index c41b8bffd..06ff7cd10 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 := unfold block in *.
+Ltac unblock_goal := cbv beta delta [block]. 
 
 (** Notation for heterogenous equality. *)
 
@@ -411,26 +411,26 @@ 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' tac H :=
-  (try intros until H) ; block_goal ; generalize_eqs H ; tac H ; simplify_dep_elim ; 
+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.
 
 (** 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.  *)
 
 Tactic Notation "dependent" "destruction" ident(H) := 
-  do_depelim' ltac:(fun hyp => do_case hyp) H.
+  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H.
 
 Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
-  do_depelim' ltac:(fun hyp => destruct hyp using c) H.
+  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the elimination. *)
 
 Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
-  do_depelim' ltac:(fun hyp => revert l ; do_case hyp) H.
+  do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_case hyp) H.
 
 Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
-  do_depelim' ltac:(fun hyp => revert l ; destruct hyp using c) H.
+  do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H.
 
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
    writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before
@@ -445,7 +445,7 @@ Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
-  do_depelim' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
+  do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_ind hyp) H.
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
-  do_depelim' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
+  do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H.