réparation d'un bug de Correctness: whd_programs ne doit pas réduire les terms contenant des Evar pas des Metas; mise à jour des exemples

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

7 files changed, 58 insertions, 78 deletions

diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v
index 26b2af4cfd..4be00cd155 100644
--- a/contrib/correctness/examples/Handbook.v
+++ b/contrib/correctness/examples/Handbook.v
@@ -1,20 +1,14 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(* Certification of Imperative Programs                                     *)
-(* Jean-Christophe Filliâtre                                                *)
-(****************************************************************************)
-(*                                 Handbook.v                               *)
-(****************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
+
+(* $Id$ *)
 
 (* This file contains proofs of programs taken from the
  * "Handbook of Theoretical Computer Science", volume B,
diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v
index e4aaa49c2c..2c5a169a56 100644
--- a/contrib/correctness/examples/exp.v
+++ b/contrib/correctness/examples/exp.v
@@ -161,11 +161,11 @@ Correctness i_exp
     { result=(power x n) }
 .
 Proof.
-stop.
 Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith.
 
 Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity.
 
+Split.
 Exact (lt_div2 e0 Test2).
 
 Rewrite Q. Unfold double. Unfold square.
diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v
index d0c77e9803..0e35f6c51a 100644
--- a/contrib/correctness/examples/exp_int.v
+++ b/contrib/correctness/examples/exp_int.v
@@ -1,20 +1,14 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(* Certification of Imperative Programs                                     *)
-(* Jean-Christophe Filliâtre                                                *)
-(****************************************************************************)
-(*                                  exp_int.v                               *)
-(****************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
+
+(* $Id$ *)
 
 (* Efficient computation of X^n using
  * 
@@ -146,6 +140,7 @@ Omega.
 Decompose [and] Inv.
 Rewrite (Zeven_div2 e0 Test1) in H. Rewrite H.
 Auto with zarith.
+Split.
 (* Zwf *)
 Unfold Zwf.
 Repeat Split.
diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v
index a6c443807c..fba440bb17 100644
--- a/contrib/correctness/examples/fact.v
+++ b/contrib/correctness/examples/fact.v
@@ -1,20 +1,14 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(* Certification of Imperative Programs                                     *)
-(* Jean-Christophe Filliâtre                                                *)
-(****************************************************************************)
-(*                                   fact.v                                 *)
-(****************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
+
+(* $Id$ *)
 
 (* Proof of an imperative program computing the factorial (over type nat) *)
 
@@ -60,6 +54,7 @@ Correctness factorielle
   end
   { y = (fact x@0) }.
 Proof.
+Split.
 (* decreasing of the variant *)
 Omega.
 (* preservation of the invariant *)
@@ -72,6 +67,3 @@ Rewrite H2 in H1.
 Rewrite <- H1.
 Auto with arith.
 Save.
-
-
-(* $Id$ *)
diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v
index f510fe32b4..c234c5ca3f 100644
--- a/contrib/correctness/examples/fact_int.v
+++ b/contrib/correctness/examples/fact_int.v
@@ -1,20 +1,14 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(* Certification of Imperative Programs                                     *)
-(* Jean-Christophe Filliâtre                                                *)
-(****************************************************************************)
-(*                                fact_int.v                                *)
-(****************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
+
+(* $Id$ *)
 
 (* Proof of an imperative program computing the factorial (over type Z) *)
 
@@ -179,6 +173,7 @@ Correctness factorielle
   end
   { (fact x@0 y) }.
 Proof.
+Split.
 (* decreasing *)
 Unfold Zwf. Unfold Zpred. Omega.
 (* preservation of the invariant *)
@@ -198,6 +193,3 @@ Decompose [and] Inv.
 Rewrite H0 in H2.
 Exact (invariant_0 x y1 H2).
 Save.
-
-
-(* $Id$ *)
diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v
index 730a25fd48..55cafbf8d1 100644
--- a/contrib/correctness/preuves.v
+++ b/contrib/correctness/preuves.v
@@ -37,6 +37,13 @@ Save.
 Global Variable i : Z ref.
 Debug on.
 Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }.
+
+(**********************************************************************)
+
+Global Variable i : Z ref.
+Debug on.
+Correctness assert0 { `0 <= i` } begin assert { `i=2` }; i:=!i-1 end { `i=1` }.
+
 (**********************************************************************)
 
 Correctness echange
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 72f577a7cc..aa60bfb8c5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1007,7 +1007,7 @@ let rec apprec env sigma s =
 let hnf env sigma c = apprec env sigma (c, empty_stack)
 
 (* A reduction function like whd_betaiota but which keeps casts
- * and does not reduce redexes containing meta-variables.
+ * and does not reduce redexes containing existential variables.
  * Used in Correctness.
  * Added by JCF, 29/1/98. *)
 
@@ -1017,7 +1017,7 @@ let whd_programs_stack env sigma =
       | IsApp (f,cl) ->
 	  let n = Array.length cl - 1 in
 	  let c = cl.(n) in
-	  if occur_meta c then 
+	  if occur_existential c then 
 	    s 
 	  else 
 	    whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack)
@@ -1026,7 +1026,7 @@ let whd_programs_stack env sigma =
              | None -> s
              | Some (a,m) -> stacklam whrec [a] c m)
       | IsMutCase (ci,p,d,lf) ->
-	  if occur_meta d then
+	  if occur_existential d then
 	    s
 	  else
             let (c,cargs) = whrec (d, empty_stack) in