branchement extraction en standard (pas de Require)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 1 deletions

diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v
index 22eccbdba..730a25fd4 100644
--- a/contrib/correctness/preuves.v
+++ b/contrib/correctness/preuves.v
@@ -28,10 +28,15 @@ Save.
 
 Global Variable i : Z ref.
 Debug on.
-Correctness assign1 { `0 <= i` } begin i := !i + 1 end { `0 < i` }.
+Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }.
+Omega.
+Save.
 
 (**********************************************************************)
 
+Global Variable i : Z ref.
+Debug on.
+Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }.
 (**********************************************************************)
 
 Correctness echange