blob: 39290829137e9585ebed1c3b7b7610540a1c9887 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* -*- mode: coq; coq-prog-args: ("-vos") -*- *)
Set Default Proof Using "Type".
Section foo.
Context (A:Type).
Definition x : option A.
(* this can get printed with -vos since without "Proof." there's no Proof
using, even with a default annotation. *)
idtac "creating x without [Proof.]".
exact None.
Qed.
End foo.
|
