2 files changed, 10 insertions, 11 deletions
diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v
index 1b6bc0b38f..e4aaa49c2c 100644
--- a/contrib/correctness/examples/exp.v
+++ b/contrib/correctness/examples/exp.v
@@ -149,7 +149,7 @@ Correctness i_exp
     let e = ref n in
     begin
       while (notzerop_bool !e) do
-        { invariant (power x n)=(mult y (power m e)) as I
+        { invariant (power x n)=(mult y (power m e)) as Inv
           variant e for lt }
         (if not (even_odd_bool !e) then y := (mult !y !m))
           { (power x n) = (mult y (power m (double (div2 e)))) as Q };
@@ -161,11 +161,10 @@ Correctness i_exp
     { result=(power x n) }
 .
 Proof.
-Rewrite (odd_double e0 Test1) in I. Rewrite I. Simpl. Auto with arith.
+stop.
+Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith.
 
-Rewrite (even_double e0 Test1) in I. Rewrite I. Reflexivity.
-
-Split.
+Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity.
 
 Exact (lt_div2 e0 Test2).
 
@@ -177,8 +176,8 @@ Rewrite (power_2n m0 (div2 e0)). Reflexivity.
 
 Auto with arith.
 
-Decompose [and] I.
-Rewrite H0. Rewrite H1.
+Decompose [and] Inv.
+Rewrite H. Rewrite H0.
 Auto with arith.
 Save.
 
diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v
index dc55eafa13..e6beecccf8 100644
--- a/contrib/correctness/examples/exp_int.v
+++ b/contrib/correctness/examples/exp_int.v
@@ -27,7 +27,7 @@
 Require Zpower.
 Require Zcomplements.
 
-Require Programs.
+Require Correctness.
 Require ZArithRing.
 Require Omega.
 
@@ -52,12 +52,12 @@ Intro. Absurd `0 > 0`; [ Omega | Assumption ].
 Destruct p; Auto with zarith.
 
 Simpl.
-Intro p.
+Intro p0.
 Replace (POS (xI p0)) with `2*(POS p0)+1`.
 Omega.
 Simpl. Auto with zarith.
 
-Intro p.
+Intro p0.
 Simpl.
 Replace (POS (xO p0)) with `2*(POS p0)`.
 Omega.
@@ -120,7 +120,7 @@ Correctness i_exp
     let e = ref n in
     begin
       while !e > 0 do
-        { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as I
+        { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as Inv
           variant e }
         (if not (Zeven_odd_bool !e) then y := (Zmult !y !m))
           { (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q };