blob: 3c163fb77221a45f2fb4eff047d31b944e5f8d54 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* -*- mode: coq; coq-prog-args: ("-vos") -*- *)
Section foo.
Context {H:True}.
Set Default Proof Using "Type".
Theorem test2 : True.
Proof.
(* BUG: this gets run when compiling with -vos *)
fail "proof with default using".
exact I.
Qed.
Theorem test3 : True.
Proof using Type.
(* this isn't run with -vos *)
fail "using".
exact I.
Qed.
End foo.
|
