Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 24 insertions, 5 deletions

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 5aa78816..8013e1d3 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -1,11 +1,11 @@
 (* Submitted by Robert Schneck *)
 
-Parameter A B C D : Prop.
+Parameters A B C D : Prop.
 Axiom X : A -> B -> C /\ D.
 
 Lemma foo : A -> B -> C.
 Proof.
-intros. 
+intros.
 destruct X. (* Should find axiom X and should handle arguments of X *)
 assumption.
 assumption.
@@ -45,9 +45,9 @@ Require Import List.
 Definition alist R := list (nat * R)%type.
 
 Section Properties.
-  Variables A : Type.
-  Variables a : A.
-  Variables E : alist A.
+  Variable A : Type.
+  Variable a : A.
+  Variable E : alist A.
 
   Lemma silly : E = E.
   Proof.
@@ -55,3 +55,22 @@ Section Properties.
   Abort.
 
 End Properties.
+
+(* This used not to work before revision 11944 *)
+
+Goal forall P:(forall n, 0=n -> Prop), forall H: 0=0, P 0 H.
+destruct H.
+Abort.
+
+(* The calls to "destruct" below did not work before revision 12356 *)
+
+Variable A0:Type.
+Variable P:A0->Type.
+Require Import JMeq.
+Goal forall a b (p:P a) (q:P b),
+  forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q).
+intros.
+destruct H.
+destruct H0.
+reflexivity.
+Qed.