test-suite/success/proof_using_noinit.v


1
2
3
4
5
6
7
8
9

(* -*- coq-prog-args: ("-noinit"); -*- *)

Section A.
Variable A : Prop.
Hypothesis a : A.
Lemma b : A.
Proof using a.
Admitted.
End A.