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

5 files changed, 48 insertions, 75 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$ *)