blob: 69bf8d194a2a5f460b81bd337fe51e8cb074f84a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
Require Program.Tactics.
Set Suggest Proof Using.
Lemma nosec : nat. Proof. exact 0. Qed.
Lemma nosec_exactproof : bool. Proof false.
Program Definition nosec_program : nat := _.
Next Obligation. exact 1. Qed.
Lemma nosec_abstract : nat.
Proof. abstract exact 3. Defined.
Section Sec.
Variables A B : Type.
(* Some normal lemma. *)
Lemma Nat : Set.
Proof.
exact nat.
Qed.
(* Make sure All is suggested even though we add an unused variable
to the context. *)
Let foo : Type.
Proof.
exact (A -> B).
Qed.
(* Having a [Proof using] disables the suggestion message. *)
Definition bar : Type.
Proof using A.
exact A.
Qed.
(* Transparent definitions don't get a suggestion message. *)
Definition baz : Type.
Proof.
exact A.
Defined.
(* No suggest, is this OK? There's nowhere to put it anyway. *)
Program Definition program : nat := _.
Next Obligation. exact 1. Qed.
(* Must not suggest *)
Lemma sec_abstract : nat.
Proof. abstract exact 3. Defined.
(* Suggests even though there's nowhere to put it, bug? *)
Lemma sec_exactproof : bool. Proof true.
End Sec.
|
