blob: 73131a3190db6039ac8924fd998fea86299fc72b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* -*- mode: coq; coq-prog-args: ("-vos") -*- *)
Section foo.
Context {H:True}.
Theorem test1 : True.
Proof.
(* this gets printed with -vos because there's no annotation (either [Set
Default Proof Using ...] or an explicit [Proof using ...]) *)
idtac "without using".
exact I.
Qed.
End foo.
|
