diff options
Diffstat (limited to 'contrib/correctness')
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 |