summaryrefslogtreecommitdiff
path: root/test-suite/success/Generalize.v
blob: 980c89dd9c21cd5e57762618e3ca3c21be48277b (plain)
1
2
3
4
5
6
7
8
(* Check Generalize Dependent *)

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.