From 999b303a775257ee076adffe6daa7d528bcd35bc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 Feb 2009 10:46:20 +0000
Subject: Add support for dependent "destruct" over terms in dependent types.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11944 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/destruct.v | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 5aa78816b0..59d583feec 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -1,6 +1,6 @@
 (* 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.
@@ -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,9 @@ 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.
-- 
cgit v1.2.3