diff options
Diffstat (limited to 'test-suite/success/Generalize.v')
| -rw-r--r-- | test-suite/success/Generalize.v | 9 |
1 files changed, 5 insertions, 4 deletions
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. |