summaryrefslogtreecommitdiff
path: root/contrib/correctness
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/correctness
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'contrib/correctness')
-rw-r--r--contrib/correctness/ArrayPermut.v2
-rw-r--r--contrib/correctness/Arrays.v2
-rw-r--r--contrib/correctness/Arrays_stuff.v2
-rw-r--r--contrib/correctness/Correctness.v2
-rw-r--r--contrib/correctness/Exchange.v2
-rw-r--r--contrib/correctness/ProgBool.v2
-rw-r--r--contrib/correctness/ProgInt.v2
-rw-r--r--contrib/correctness/ProgramsExtraction.v2
-rw-r--r--contrib/correctness/Programs_stuff.v2
-rw-r--r--contrib/correctness/Sorted.v2
-rw-r--r--contrib/correctness/Tuples.v2
-rw-r--r--contrib/correctness/examples/Handbook.v2
-rw-r--r--contrib/correctness/examples/exp.v2
-rw-r--r--contrib/correctness/examples/exp_int.v2
-rw-r--r--contrib/correctness/examples/fact.v2
-rw-r--r--contrib/correctness/examples/fact_int.v2
-rw-r--r--contrib/correctness/past.mli2
-rw-r--r--contrib/correctness/pcic.ml2
-rw-r--r--contrib/correctness/pcic.mli2
-rw-r--r--contrib/correctness/pcicenv.ml2
-rw-r--r--contrib/correctness/pcicenv.mli2
-rw-r--r--contrib/correctness/pdb.ml2
-rw-r--r--contrib/correctness/pdb.mli2
-rw-r--r--contrib/correctness/peffect.ml2
-rw-r--r--contrib/correctness/peffect.mli2
-rw-r--r--contrib/correctness/penv.ml2
-rw-r--r--contrib/correctness/penv.mli2
-rw-r--r--contrib/correctness/perror.ml2
-rw-r--r--contrib/correctness/perror.mli2
-rw-r--r--contrib/correctness/pextract.ml2
-rw-r--r--contrib/correctness/pextract.mli2
-rw-r--r--contrib/correctness/pmisc.ml2
-rw-r--r--contrib/correctness/pmisc.mli2
-rw-r--r--contrib/correctness/pmlize.ml2
-rw-r--r--contrib/correctness/pmlize.mli2
-rw-r--r--contrib/correctness/pmonad.ml2
-rw-r--r--contrib/correctness/pmonad.mli2
-rw-r--r--contrib/correctness/pred.ml2
-rw-r--r--contrib/correctness/pred.mli2
-rw-r--r--contrib/correctness/prename.ml2
-rw-r--r--contrib/correctness/prename.mli2
-rw-r--r--contrib/correctness/psyntax.ml418
-rw-r--r--contrib/correctness/psyntax.mli2
-rw-r--r--contrib/correctness/ptactic.ml12
-rw-r--r--contrib/correctness/ptactic.mli2
-rw-r--r--contrib/correctness/ptype.mli2
-rw-r--r--contrib/correctness/ptyping.ml2
-rw-r--r--contrib/correctness/ptyping.mli2
-rw-r--r--contrib/correctness/putil.ml16
-rw-r--r--contrib/correctness/putil.mli2
-rw-r--r--contrib/correctness/pwp.ml2
-rw-r--r--contrib/correctness/pwp.mli2
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