4 files changed, 16 insertions, 11 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 170a56b28..cf233a988 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -89,8 +89,8 @@ let sig_n n =
 	    mind_entry_consnames = [ cname ];
 	    mind_entry_lc = [ lc ] } ] }
 	
-let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "pair",0),1)
-let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "exist",0),1)
+let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1)
+let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1)
 
 let tuple_ref dep n =
   if n = 2 & not dep then
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index d6f9e0e72..c71c91f93 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -29,9 +29,9 @@ let is_eta_redex bl al =
       Invalid_argument("List.for_all2") -> false
 
 let rec red = function
-    CC_letin (dep, ty, bl, e1, e2) ->
+  | CC_letin (dep, ty, bl, e1, e2) ->
       begin match red e2 with
-	  CC_tuple (false,tl,al) ->
+	| CC_tuple (false,tl,al) ->
 	    if is_eta_redex bl al then
 	      red e1
 	    else
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
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index b8ac08531..45ab72c38 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -105,16 +105,16 @@ let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0)
 (* ["(well_founded nat lt)"] *)
 let wf_nat_pattern = 
   PApp (PRef well_founded, [| PRef nat; PRef lt |])
-(* ["((well_founded Z (Zwf ?))"] *)
+(* ["((well_founded Z (Zwf ?1))"] *)
 let wf_z_pattern = 
   let zwf = ConstRef (coq_constant ["correctness";"Zwf"] "Zwf") in
-  PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta None |]) |])
-(* ["(and ? ?)"] *)
+  PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |])
+(* ["(and ?1 ?2)"] *)
 let and_pattern = 
-  PApp (PRef and_, [| PMeta None; PMeta None |])
-(* ["(eq ? ? ?)"] *)
+  PApp (PRef and_, [| PMeta (Some 1); PMeta (Some 2) |])
+(* ["(eq ?1 ?2 ?3)"] *)
 let eq_pattern = 
-  PApp (PRef eq, [| PMeta None; PMeta None; PMeta None |])
+  PApp (PRef eq, [| PMeta (Some 1); PMeta (Some 2); PMeta (Some 3) |])
 
 (* loop_ids: remove loop<i> hypotheses from the context, and rewrite
  * using Variant<i> hypotheses when needed. *)