aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/808_2411.v
blob: 1c13e745475bea75b7aa42640d4f4887c914a360 (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
Section test.
Variable n:nat.
Lemma foo: 0 <= n.
Proof.
(* declaring an Axiom during a proof makes it immediatly
   usable, juste as a full Definition. *)
Axiom bar : n = 1.
rewrite bar.
now apply le_S.
Qed.

Lemma foo' : 0 <= n.
Proof.
(* Declaring an Hypothesis during a proof is ok,
   but this hypothesis won't be usable by the current proof(s),
   only by later ones. *)
Hypothesis bar' : n = 1.
Fail rewrite bar'.
Abort.

Lemma foo'' : 0 <= n.
Proof.
rewrite bar'.
now apply le_S.
Qed.

End test.