← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/bugs/closed/shouldsucceed/808_2411.v

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/bugs/closed/shouldsucceed/808_2411.v
 
1
Section test.
 
2
Variable n:nat.
 
3
Lemma foo: 0 <= n.
 
4
Proof.
 
5
(* declaring an Axiom during a proof makes it immediatly
 
6
   usable, juste as a full Definition. *)
 
7
Axiom bar : n = 1.
 
8
rewrite bar.
 
9
now apply le_S.
 
10
Qed.
 
11
 
 
12
Lemma foo' : 0 <= n.
 
13
Proof.
 
14
(* Declaring an Hypothesis during a proof is ok,
 
15
   but this hypothesis won't be usable by the current proof(s),
 
16
   only by later ones. *)
 
17
Hypothesis bar' : n = 1.
 
18
Fail rewrite bar'.
 
19
Abort.
 
20
 
 
21
Lemma foo'' : 0 <= n.
 
22
Proof.
 
23
rewrite bar'.
 
24
now apply le_S.
 
25
Qed.
 
26
 
 
27
End test.
 
 
b'\\ No newline at end of file'