aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/SuggestProofUsing.v
blob: 00b6f8e1837e2606af8ae2606939bfc8cc6c8622 (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
Set Suggest Proof Using.

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.

End Sec.