From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- test-suite/success/Generalize.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'test-suite/success/Generalize.v') diff --git a/test-suite/success/Generalize.v b/test-suite/success/Generalize.v index 0dc73991..980c89dd 100644 --- a/test-suite/success/Generalize.v +++ b/test-suite/success/Generalize.v @@ -1,7 +1,8 @@ (* Check Generalize Dependent *) -Lemma l1 : [a:=O;b:=a](c:b=b;d:(True->b=b))d=d. -Intros. -Generalize Dependent a. -Intros a b c d. +Lemma l1 : + let a := 0 in let b := a in forall (c : b = b) (d : True -> b = b), d = d. +intros. +generalize dependent a. +intros a b c d. Abort. -- cgit v1.2.3