Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

52 files changed, 72 insertions, 72 deletions

diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v
index b352045a..30f5ac8f 100644
--- a/contrib/correctness/ArrayPermut.v
+++ b/contrib/correctness/ArrayPermut.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ArrayPermut.v,v 1.3.2.1 2004/07/16 19:29:59 herbelin Exp $ *)
+(* $Id: ArrayPermut.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (****************************************************************************)
 (*                    Permutations of elements in arrays                    *)
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v
index 1659917a..3a6aaaf8 100644
--- a/contrib/correctness/Arrays.v
+++ b/contrib/correctness/Arrays.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: Arrays.v,v 1.9.2.1 2004/07/16 19:29:59 herbelin Exp $ *)
+(* $Id: Arrays.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (**********************************************)
 (* Functional arrays, for use in Correctness. *)
diff --git a/contrib/correctness/Arrays_stuff.v b/contrib/correctness/Arrays_stuff.v
index 899d7007..a8a2858f 100644
--- a/contrib/correctness/Arrays_stuff.v
+++ b/contrib/correctness/Arrays_stuff.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: Arrays_stuff.v,v 1.2.16.1 2004/07/16 19:29:59 herbelin Exp $ *)
+(* $Id: Arrays_stuff.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Exchange.
 Require Export ArrayPermut.
diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index a2ad2f50..b7513d09 100644
--- a/contrib/correctness/Correctness.v
+++ b/contrib/correctness/Correctness.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: Correctness.v,v 1.6.2.1 2004/07/16 19:29:59 herbelin Exp $ *)
+(* $Id: Correctness.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* Correctness is base on the tactic Refine (developped on purpose) *)
 
diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v
index 7dc5218e..035a98f2 100644
--- a/contrib/correctness/Exchange.v
+++ b/contrib/correctness/Exchange.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: Exchange.v,v 1.4.2.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: Exchange.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (****************************************************************************)
 (*                   Exchange of two elements in an array                   *)
diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v
index bce19870..38448efc 100644
--- a/contrib/correctness/ProgBool.v
+++ b/contrib/correctness/ProgBool.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ProgBool.v,v 1.4.2.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: ProgBool.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Import ZArith.
 Require Export Bool_nat.
diff --git a/contrib/correctness/ProgInt.v b/contrib/correctness/ProgInt.v
index c26e3553..b1eaaea7 100644
--- a/contrib/correctness/ProgInt.v
+++ b/contrib/correctness/ProgInt.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ProgInt.v,v 1.2.2.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: ProgInt.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export ZArith.
 Require Export ZArith_dec.
diff --git a/contrib/correctness/ProgramsExtraction.v b/contrib/correctness/ProgramsExtraction.v
index 40253f33..5f7dfdbf 100644
--- a/contrib/correctness/ProgramsExtraction.v
+++ b/contrib/correctness/ProgramsExtraction.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ProgramsExtraction.v,v 1.2.16.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: ProgramsExtraction.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Extraction.
 
diff --git a/contrib/correctness/Programs_stuff.v b/contrib/correctness/Programs_stuff.v
index 1ca4b63e..6489de81 100644
--- a/contrib/correctness/Programs_stuff.v
+++ b/contrib/correctness/Programs_stuff.v
@@ -8,6 +8,6 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: Programs_stuff.v,v 1.1.16.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: Programs_stuff.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Arrays_stuff.
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v
index 2efe54a4..ca4ed880 100644
--- a/contrib/correctness/Sorted.v
+++ b/contrib/correctness/Sorted.v
@@ -8,7 +8,7 @@
 
 (*  Library about sorted (sub-)arrays / Nicolas Magaud, July 1998 *)
 
-(* $Id: Sorted.v,v 1.7.2.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: Sorted.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Arrays.
 Require Import ArrayPermut.
diff --git a/contrib/correctness/Tuples.v b/contrib/correctness/Tuples.v
index e3fff08d..c7071f32 100644
--- a/contrib/correctness/Tuples.v
+++ b/contrib/correctness/Tuples.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: Tuples.v,v 1.2.2.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: Tuples.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* Tuples *)
 
diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v
index 8c983a72..abb1cc76 100644
--- a/contrib/correctness/examples/Handbook.v
+++ b/contrib/correctness/examples/Handbook.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: Handbook.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *)
+(* $Id: Handbook.v 1577 2001-04-11 07:56:19Z filliatr $ *)
 
 (* 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 dcfcec87..3142e906 100644
--- a/contrib/correctness/examples/exp.v
+++ b/contrib/correctness/examples/exp.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(*i $Id: exp.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ i*)
+(*i $Id: exp.v 1577 2001-04-11 07:56:19Z filliatr $ i*)
 
 (* Efficient computation of X^n using
  * 
diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v
index accd60c2..044263ca 100644
--- a/contrib/correctness/examples/exp_int.v
+++ b/contrib/correctness/examples/exp_int.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: exp_int.v,v 1.4 2001/04/11 07:56:19 filliatr Exp $ *)
+(* $Id: exp_int.v 1577 2001-04-11 07:56:19Z filliatr $ *)
 
 (* Efficient computation of X^n using
  * 
diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v
index e480c806..07e77140 100644
--- a/contrib/correctness/examples/fact.v
+++ b/contrib/correctness/examples/fact.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: fact.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *)
+(* $Id: fact.v 1577 2001-04-11 07:56:19Z filliatr $ *)
 
 (* Proof of an imperative program computing the factorial (over type nat) *)
 
diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v
index cb2b0460..f463ca80 100644
--- a/contrib/correctness/examples/fact_int.v
+++ b/contrib/correctness/examples/fact_int.v
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: fact_int.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *)
+(* $Id: fact_int.v 1577 2001-04-11 07:56:19Z filliatr $ *)
 
 (* Proof of an imperative program computing the factorial (over type Z) *)
 
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 1cc7164e..70328704 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: past.mli,v 1.7.6.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: past.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (*s Abstract syntax of imperative programs. *)
 
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index e87ba70c..041cd81f 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pcic.ml,v 1.23.2.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: pcic.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Util
 open Names
diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli
index 89731472..67b152f3 100644
--- a/contrib/correctness/pcic.mli
+++ b/contrib/correctness/pcic.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(*i $Id: pcic.mli,v 1.3.16.1 2004/07/16 19:30:00 herbelin Exp $ i*)
+(*i $Id: pcic.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 open Past
 open Rawterm
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
index cc15c8f3..368d0281 100644
--- a/contrib/correctness/pcicenv.ml
+++ b/contrib/correctness/pcicenv.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pcicenv.ml,v 1.5.14.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: pcicenv.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Term
diff --git a/contrib/correctness/pcicenv.mli b/contrib/correctness/pcicenv.mli
index fc4fa0b9..365fa960 100644
--- a/contrib/correctness/pcicenv.mli
+++ b/contrib/correctness/pcicenv.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pcicenv.mli,v 1.2.16.1 2004/07/16 19:30:00 herbelin Exp $ *)
+(* $Id: pcicenv.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Penv
 open Names
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 302db871..759e9133 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pdb.ml,v 1.8.2.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pdb.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Term
diff --git a/contrib/correctness/pdb.mli b/contrib/correctness/pdb.mli
index a0df29bd..d6e647b7 100644
--- a/contrib/correctness/pdb.mli
+++ b/contrib/correctness/pdb.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pdb.mli,v 1.2.16.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pdb.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Ptype
 open Past
diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml
index 08d6b002..faf5f3d3 100644
--- a/contrib/correctness/peffect.ml
+++ b/contrib/correctness/peffect.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: peffect.ml,v 1.3.14.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: peffect.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Nameops
diff --git a/contrib/correctness/peffect.mli b/contrib/correctness/peffect.mli
index d6d0ce22..9a10dea4 100644
--- a/contrib/correctness/peffect.mli
+++ b/contrib/correctness/peffect.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: peffect.mli,v 1.1.16.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: peffect.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 820d1cf0..7f89b1e1 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: penv.ml,v 1.10.2.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: penv.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pmisc
 open Past
diff --git a/contrib/correctness/penv.mli b/contrib/correctness/penv.mli
index ef2e4c6e..6743b465 100644
--- a/contrib/correctness/penv.mli
+++ b/contrib/correctness/penv.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: penv.mli,v 1.3.8.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: penv.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Ptype
 open Past
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 40fe4c98..8415e96d 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: perror.ml,v 1.9.2.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: perror.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/contrib/correctness/perror.mli b/contrib/correctness/perror.mli
index 40b2d25c..45b2acdc 100644
--- a/contrib/correctness/perror.mli
+++ b/contrib/correctness/perror.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: perror.mli,v 1.2.6.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: perror.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
index 2a35d471..407567ad 100644
--- a/contrib/correctness/pextract.ml
+++ b/contrib/correctness/pextract.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pextract.ml,v 1.5.6.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pextract.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp_control
 open Pp
diff --git a/contrib/correctness/pextract.mli b/contrib/correctness/pextract.mli
index dc5b4124..3492729c 100644
--- a/contrib/correctness/pextract.mli
+++ b/contrib/correctness/pextract.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pextract.mli,v 1.2.16.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pextract.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index aed8c5cb..29d8fdcf 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pmisc.ml,v 1.18.2.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pmisc.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index ec7521cc..9d96467f 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pmisc.mli,v 1.9.6.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pmisc.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Term
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
index f899366d..e812fa57 100644
--- a/contrib/correctness/pmlize.ml
+++ b/contrib/correctness/pmlize.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pmlize.ml,v 1.7.2.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pmlize.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Term
diff --git a/contrib/correctness/pmlize.mli b/contrib/correctness/pmlize.mli
index 95f74ef9..1f8936f0 100644
--- a/contrib/correctness/pmlize.mli
+++ b/contrib/correctness/pmlize.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pmlize.mli,v 1.2.16.1 2004/07/16 19:30:01 herbelin Exp $ *)
+(* $Id: pmlize.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Past
 open Penv
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index b8b39353..31effc1b 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pmonad.ml,v 1.6.16.1 2004/07/16 19:30:02 herbelin Exp $ *)
+(* $Id: pmonad.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Util
 open Names
diff --git a/contrib/correctness/pmonad.mli b/contrib/correctness/pmonad.mli
index e1400fcb..a46a040e 100644
--- a/contrib/correctness/pmonad.mli
+++ b/contrib/correctness/pmonad.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pmonad.mli,v 1.1.16.1 2004/07/16 19:30:02 herbelin Exp $ *)
+(* $Id: pmonad.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Term
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index 732dcf08..669727fc 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pred.ml,v 1.6.14.1 2004/07/16 19:30:05 herbelin Exp $ *)
+(* $Id: pred.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Past
diff --git a/contrib/correctness/pred.mli b/contrib/correctness/pred.mli
index 2f43f4ad..a5a9549b 100644
--- a/contrib/correctness/pred.mli
+++ b/contrib/correctness/pred.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pred.mli,v 1.1.16.1 2004/07/16 19:30:05 herbelin Exp $ *)
+(* $Id: pred.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Term
 open Past
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml
index 864f6abd..4ef1982d 100644
--- a/contrib/correctness/prename.ml
+++ b/contrib/correctness/prename.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: prename.ml,v 1.3.14.1 2004/07/16 19:30:05 herbelin Exp $ *)
+(* $Id: prename.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Nameops
diff --git a/contrib/correctness/prename.mli b/contrib/correctness/prename.mli
index 88b49d2c..1d3ab669 100644
--- a/contrib/correctness/prename.mli
+++ b/contrib/correctness/prename.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: prename.mli,v 1.1.16.1 2004/07/16 19:30:05 herbelin Exp $ *)
+(* $Id: prename.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index c1f00a3d..eeec28a5 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: psyntax.ml4,v 1.29.2.1 2004/07/16 19:30:05 herbelin Exp $ *)
+(* $Id: psyntax.ml4 7740 2005-12-26 20:07:21Z herbelin $ *)
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
@@ -145,7 +145,7 @@ let bool_not loc a =
   let d = SApp ( [Variable connective_not ], [a]) in
   w d
 
-let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "ZERO"]
+let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "Z0"]
 
 (* program -> Coq AST *)
 
@@ -852,7 +852,7 @@ let pr_effects x =
   let (ro,rw) = Peffect.get_repr x in pr_reads ro ++ pr_writes rw
 
 let pr_predicate delimited { a_name = n; a_value = c } =
-  (if delimited then Ppconstrnew.pr_lconstr else Ppconstrnew.pr_constr) c ++
+  (if delimited then Ppconstr.pr_lconstr else Ppconstr.pr_constr) c ++
   (match n with Name id -> spc () ++ str "as " ++ pr_id id | Anonymous -> mt())
 
 let pr_assert b { p_name = x; p_value = v } =
@@ -870,7 +870,7 @@ let pr_post_condition_opt = function
 
 let rec pr_type_v_v8 = function
   | Array (a,v) ->
-      str "array" ++ spc() ++ Ppconstrnew.pr_constr a ++ spc() ++ str "of " ++
+      str "array" ++ spc() ++ Ppconstr.pr_constr a ++ spc() ++ str "of " ++
       pr_type_v_v8 v
   | v -> pr_type_v3 v
 
@@ -882,7 +882,7 @@ and pr_type_v3 = function
       pr_type_v_v8 v ++ pr_effects e ++ 
       pr_pre_condition_list prel ++ pr_post_condition_opt postl ++
       spc () ++ str "end"
-  | TypePure a -> Ppconstrnew.pr_constr a
+  | TypePure a -> Ppconstr.pr_constr a
   | v -> str "(" ++ pr_type_v_v8 v ++ str ")"
 
 and pr_binder = function
@@ -910,9 +910,9 @@ let pr_invariant = function
   | Some c -> hov 2 (str "invariant" ++ spc ()  ++ pr_predicate false c)
 
 let pr_variant (c1,c2) =
-  Ppconstrnew.pr_constr c1 ++
+  Ppconstr.pr_constr c1 ++
   (try Constrextern.check_same_type c2 (ast_zwf_zero dummy_loc); mt ()
-   with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstrnew.pr_constr c2))
+   with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstr.pr_constr c2))
 
 let rec pr_desc = function
   | Variable id ->
@@ -1025,7 +1025,7 @@ let rec pr_desc = function
       (* Numeral or "tt": use a printer which doesn't globalize *)
       Ppconstr.pr_constr
         (Constrextern.extern_constr_in_scope false "Z_scope" (Global.env()) c)
-  | Debug (s,p) -> str "@" ++ Pptacticnew.qsnew s ++ pr_prog p
+  | Debug (s,p) -> str "@" ++ Pptactic.qsnew s ++ pr_prog p
 
 and pr_block_st = function
   | Label s -> hov 0 (str "label" ++ spc() ++ str s)
@@ -1046,7 +1046,7 @@ and pr_prog0 b { desc = desc; pre = pre; post = post } =
     hov 0
       (if b & post<>None then str"(" ++ pr_desc desc ++ str")"
        else pr_desc desc)
-    ++ Ppconstrnew.pr_opt pr_postcondition post)
+    ++ Ppconstr.pr_opt pr_postcondition post)
 
 and pr_prog x = pr_prog0 true x
 
diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli
index 18912548..c0f0990b 100644
--- a/contrib/correctness/psyntax.mli
+++ b/contrib/correctness/psyntax.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: psyntax.mli,v 1.3.2.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: psyntax.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pcoq
 open Ptype
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 4b22954e..e5347670 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ptactic.ml,v 1.30.2.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: ptactic.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
 
 open Pp
 open Options
@@ -51,7 +51,7 @@ let coqast_of_prog p =
 
   (* 4a. traduction type *)
   let ty = Pmonad.trad_ml_type_c ren env c in
-  deb_print (Printer.prterm_env (Global.env())) ty;
+  deb_print (Printer.pr_lconstr_env (Global.env())) ty;
 
   (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
   deb_mess 
@@ -65,12 +65,12 @@ let coqast_of_prog p =
     (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ 
        fnl ());
   let r = Pcic.rawconstr_of_prog cc in
-  deb_print Printer.pr_rawterm r;
+  deb_print Printer.pr_lrawconstr r;
 
   (* 6. résolution implicites *)
   deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ());
   let oc = understand_gen_tcc Evd.empty (Global.env()) [] None r in
-  deb_print (Printer.prterm_env (Global.env())) (snd oc);
+  deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc);
 
   p,oc,ty,v
 
@@ -234,7 +234,7 @@ let correctness_hook _ ref =
   register pf_id None
 
 let correctness s p opttac =
-  Library.check_required_library ["Coq";"correctness";"Correctness"];
+  Coqlib.check_required_library ["Coq";"correctness";"Correctness"];
   Pmisc.reset_names();
   let p,oc,cty,v = coqast_of_prog p in
   let env = Global.env () in
@@ -248,7 +248,7 @@ let correctness s p opttac =
   deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
   let oc = reduce_open_constr oc in
   deb_mess (str"AFTER REDUCTION:" ++ fnl ());
-  deb_print (Printer.prterm_env (Global.env())) (snd oc);
+  deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc);
   let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in
   let tac = match opttac with 
     | None -> tac
diff --git a/contrib/correctness/ptactic.mli b/contrib/correctness/ptactic.mli
index 875e0780..87378cff 100644
--- a/contrib/correctness/ptactic.mli
+++ b/contrib/correctness/ptactic.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ptactic.mli,v 1.2.16.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: ptactic.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* The main tactic: takes a name N, a program P, creates a goal
  * of name N with the functional specification of P, then apply the Refine
diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli
index f2dc85e3..be181bcc 100644
--- a/contrib/correctness/ptype.mli
+++ b/contrib/correctness/ptype.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ptype.mli,v 1.2.16.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: ptype.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Term
 
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index 9047a925..91c1f293 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ptyping.ml,v 1.7.6.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: ptyping.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli
index 0c0d5905..eaf548b1 100644
--- a/contrib/correctness/ptyping.mli
+++ b/contrib/correctness/ptyping.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: ptyping.mli,v 1.3.6.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: ptyping.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Names
 open Term
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 48f0781a..0eb8806c 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: putil.ml,v 1.10.2.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: putil.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
 
 open Util
 open Names
@@ -231,26 +231,26 @@ and c_of_constr c =
 open Pp
 open Util
 
-let prterm x = Printer.prterm_env (Global.env()) x
+let pr_lconstr x = Printer.pr_lconstr_env (Global.env()) x
 
 let pp_pre = function
     [] -> (mt ())
   | l  ->
       hov 0 (str"pre " ++ 
 	       prlist_with_sep (fun () -> (spc ())) 
-		 (fun x -> prterm x.p_value) l)
+		 (fun x -> pr_lconstr x.p_value) l)
 
 let pp_post = function
     None -> (mt ())
-  | Some c -> hov 0 (str"post " ++ prterm c.a_value)
+  | Some c -> hov 0 (str"post " ++ pr_lconstr c.a_value)
 
 let rec pp_type_v = function
     Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref")
-  | Array (cc,v) -> hov 0 (str"array " ++ prterm cc ++ str" of " ++ pp_type_v v)
+  | Array (cc,v) -> hov 0 (str"array " ++ pr_lconstr cc ++ str" of " ++ pp_type_v v)
   | Arrow (b,c) -> 
       hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++ 
 	       pp_type_c c)
-  | TypePure c -> prterm c
+  | TypePure c -> pr_lconstr c
 
 and pp_type_c ((id,v),e,p,q) =
   hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++ 
@@ -297,7 +297,7 @@ let rec pp_cc_term = function
   | CC_case _ ->
       hov 0 (str"<Case: not yet implemented>")
   | CC_expr c ->
-      hov 0 (prterm c)
+      hov 0 (pr_lconstr c)
   | CC_hole c ->
-      (str"(?::" ++ prterm c ++ str")")
+      (str"(?::" ++ pr_lconstr c ++ str")")
 
diff --git a/contrib/correctness/putil.mli b/contrib/correctness/putil.mli
index b44774ae..6c487f3f 100644
--- a/contrib/correctness/putil.mli
+++ b/contrib/correctness/putil.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: putil.mli,v 1.3.2.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: putil.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Names
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index 58bef673..1e485180 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pwp.ml,v 1.8.2.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: pwp.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Util
 open Names
diff --git a/contrib/correctness/pwp.mli b/contrib/correctness/pwp.mli
index 015031a0..4027a623 100644
--- a/contrib/correctness/pwp.mli
+++ b/contrib/correctness/pwp.mli
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pwp.mli,v 1.2.16.1 2004/07/16 19:30:06 herbelin Exp $ *)
+(* $Id: pwp.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Term
 open Penv