Suppression de la partie ML de la contrib correctness. Les fichiers

n'étaient plus compilés depuis le 14 janvier 2004 (avant la 8.0), Why
ayant pris la suite de correctness.



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

36 files changed, 0 insertions, 6498 deletions

diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
deleted file mode 100644
index faea9bc479..0000000000
--- a/contrib/correctness/past.mli
+++ /dev/null
@@ -1,97 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-(*s Abstract syntax of imperative programs. *)
-
-open Names
-open Ptype
-open Topconstr
-
-type termination = 
-  | RecArg of int 
-  | Wf of constr_expr * constr_expr
-
-type variable = identifier
-
-type pattern =
-  | PatVar of identifier
-  | PatConstruct of identifier * ((kernel_name * int) * int)
-  | PatAlias of pattern * identifier
-  | PatPair of pattern * pattern
-  | PatApp of pattern list
-
-type epattern =
-  | ExnConstant of identifier
-  | ExnBind of identifier * identifier
-
-type ('a, 'b) block_st =
-  | Label of string
-  | Assert of 'b Ptype.assertion
-  | Statement of 'a
-
-type ('a, 'b) block = ('a, 'b) block_st list
-
-type ('a, 'b) t = { 
-  desc : ('a, 'b) t_desc;
-  pre  : 'b Ptype.precondition list;
-  post : 'b Ptype.postcondition option;
-  loc  : Util.loc;
-  info : 'a 
-}
-
-and ('a, 'b) t_desc =
-  | Variable of variable
-  | Acc of variable
-  | Aff of variable * ('a, 'b) t
-  | TabAcc of bool * variable * ('a, 'b) t
-  | TabAff of bool * variable * ('a, 'b) t * ('a, 'b) t
-  | Seq of (('a, 'b) t, 'b) block
-  | While of ('a, 'b) t * 'b Ptype.assertion option * ('b * 'b) *
-               (('a, 'b) t, 'b) block
-  | If of ('a, 'b) t * ('a, 'b) t * ('a, 'b) t
-  | Lam of 'b Ptype.ml_type_v Ptype.binder list * ('a, 'b) t
-  | Apply of ('a, 'b) t * ('a, 'b) arg list
-  | SApp of ('a, 'b) t_desc list * ('a, 'b) t list
-  | LetRef of variable * ('a, 'b) t * ('a, 'b) t
-  | Let of variable * ('a, 'b) t * ('a, 'b) t
-  | LetRec of variable * 'b Ptype.ml_type_v Ptype.binder list *
-                'b Ptype.ml_type_v * ('b * 'b) * ('a, 'b) t
-  | PPoint of string * ('a, 'b) t_desc
-  | Expression of Term.constr
-  | Debug of string * ('a, 'b) t
-
-and ('a, 'b) arg =
-  | Term of ('a, 'b) t
-  | Refarg of variable
-  | Type of 'b Ptype.ml_type_v
-
-type program = (unit, Topconstr.constr_expr) t
-
-(*s Intermediate type for CC terms. *)
-
-type cc_type = Term.constr
-
-type cc_bind_type = 
-  | CC_typed_binder of cc_type 
-  | CC_untyped_binder
-
-type cc_binder = variable * cc_bind_type
-
-type cc_term =
-  | CC_var of variable
-  | CC_letin of bool * cc_type * cc_binder list * cc_term * cc_term
-  | CC_lam of cc_binder list * cc_term
-  | CC_app of cc_term * cc_term list
-  | CC_tuple of bool * cc_type list * cc_term list
-  | CC_case of cc_type * cc_term * cc_term list
-  | CC_expr of Term.constr
-  | CC_hole of cc_type
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
deleted file mode 100644
index 2b64ccbcb6..0000000000
--- a/contrib/correctness/pcic.ml
+++ /dev/null
@@ -1,231 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Util
-open Names
-open Nameops
-open Libnames
-open Term
-open Termops
-open Nametab
-open Declarations
-open Indtypes
-open Sign
-open Rawterm
-open Typeops
-open Entries
-open Topconstr
-
-open Pmisc
-open Past
-
-
-(* Here we translate intermediates terms (cc_term) into CCI terms (constr) *)
-
-let make_hole c = mkCast (isevar, c)
-
-(* Tuples are defined in file Tuples.v 
- * and their constructors are called Build_tuple_n or exists_n,
- * wether they are dependant (last element only) or not. 
- * If necessary, tuples are generated ``on the fly''. *)
-
-let tuple_exists id = 
-  try let _ = Nametab.locate (make_short_qualid id) in true
-  with Not_found -> false
-
-let ast_set = CSort (dummy_loc,RProp Pos)
-
-let tuple_n n =
-  let id = make_ident "tuple_" (Some n) in
-  let l1n = Util.interval 1 n in
-  let params =
-    List.map (fun i ->
-      (LocalRawAssum ([dummy_loc,Name (make_ident "T" (Some i))], ast_set)))
-      l1n in
-  let fields = 
-    List.map
-      (fun i -> 
-	 let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
-	 let id' = make_ident "T" (Some i) in
-	 (false, Vernacexpr.AssumExpr ((dummy_loc,Name id), mkIdentC id')))
-      l1n 
-  in
-  let cons = make_ident "Build_tuple_" (Some n) in
-  Record.definition_structure
-    ((false, (dummy_loc,id)), params, fields, cons, mk_Set)
-
-(*s [(sig_n n)] generates the inductive
-    \begin{verbatim}
-    Inductive sig_n [T1,...,Tn:Set; P:T1->...->Tn->Prop] : Set :=
-      exist_n : (x1:T1)...(xn:Tn)(P x1 ... xn) -> (sig_n T1 ... Tn P).
-    \end{verbatim} *)
-
-let sig_n n =
-  let id = make_ident "sig_" (Some n) in
-  let l1n = Util.interval 1 n in
-  let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in
-  let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in
-  let idp = make_ident "P" None in
-  let params =
-    let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in
-    (idp, LocalAssum typ) :: 
-    (List.rev_map (fun id -> (id, LocalAssum mkSet)) lT)
-  in
-  let lc = 
-    let app_sig = mkApp(mkRel (2*n+3),
-                        Array.init (n+1) (fun i -> mkRel (2*n+2-i))) in
-    let app_p = mkApp(mkRel (n+1),
-                      Array.init n (fun i -> mkRel (n-i))) in
-    let c = mkArrow app_p app_sig in
-    List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c
-  in
-  let cname = make_ident "exist_" (Some n) in
-  Declare.declare_mind 
-    { mind_entry_finite = true;
-      mind_entry_inds = 
-	[ { mind_entry_params = params;
-	    mind_entry_typename = id;
-	    mind_entry_arity = mkSet;
-	    mind_entry_consnames = [ cname ];
-	    mind_entry_lc = [ lc ] } ] }
-
-(*s On the fly generation of needed (possibly dependent) tuples. *)
-
-let check_product_n n =
-  if n > 2 then
-    let s = Printf.sprintf "tuple_%d" n in
-    if not (tuple_exists (id_of_string s)) then tuple_n n
-
-let check_dep_product_n n =
-  if n > 1 then
-    let s = Printf.sprintf "sig_%d" n in
-    if not (tuple_exists (id_of_string s)) then ignore (sig_n n)
-
-(*s Constructors for the tuples. *)
-	
-let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1)
-let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1)
-
-let tuple_ref dep n =
-  if n = 2 & not dep then
-    pair
-  else
-    let n = n - (if dep then 1 else 0) in
-    if dep then
-      if n = 1 then 
-	exist
-      else begin
-	let id = make_ident "exist_" (Some n) in
-	if not (tuple_exists id) then ignore (sig_n n);
-	Nametab.locate (make_short_qualid id)
-      end
-    else begin
-      let id = make_ident "Build_tuple_" (Some n) in
-      if not (tuple_exists id) then tuple_n n;
-      Nametab.locate (make_short_qualid id)
-    end
-
-(* Binders. *)
-
-let trad_binder avoid nenv id = function
-  | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
-  | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty
-
-let rec push_vars avoid nenv = function
-  | [] -> ([],avoid,nenv)
-  | (id,b) :: bl -> 
-      let b' = trad_binder avoid nenv id b in
-      let bl',avoid',nenv' = 
-	push_vars (id :: avoid) (add_name (Name id) nenv) bl 
-      in
-      ((id,b') :: bl', avoid', nenv')
-
-let rec raw_lambda bl v = match bl with
-  | [] -> 
-      v
-  | (id,ty) :: bl' -> 
-      RLambda (dummy_loc, Name id, ty, raw_lambda bl' v)
-
-(* The translation itself is quite easy.
-   letin are translated into Cases constructions *)
-
-let rawconstr_of_prog p =
-  let rec trad avoid nenv = function
-    | CC_var id -> 
-	RVar (dummy_loc, id)
-
-    (*i optimisation : let x = <constr> in e2  =>  e2[x<-constr] 
-    | CC_letin (_,_,[id,_],CC_expr c,e2) ->
-	real_subst_in_constr [id,c] (trad e2)
-    | CC_letin (_,_,([_] as b),CC_expr e1,e2) ->
-	let (b',avoid',nenv') = push_vars avoid nenv b in
-      	let c1 = Detyping.detype avoid nenv e1 
-	and c2 = trad avoid' nenv' e2 in
-	let id = Name (fst (List.hd b')) in
-	RLetIn (dummy_loc, id, c1, c2)
-    i*)
-
-    | CC_letin (_,_,([_] as b),e1,e2) ->
-	let (b',avoid',nenv') = push_vars avoid nenv b in
-      	let c1 = trad avoid nenv e1 
-	and c2 = trad avoid' nenv' e2 in
-	RApp (dummy_loc, raw_lambda b' c2, [c1])
-
-    | CC_letin (dep,ty,bl,e1,e2) ->
-	let (bl',avoid',nenv') = push_vars avoid nenv bl in
-	let c1 = trad avoid nenv e1
-	and c2 = trad avoid' nenv' e2 in
-	ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None)
-
-    | CC_lam (bl,e) ->
-	let bl',avoid',nenv' = push_vars avoid nenv bl in
-	let c = trad avoid' nenv' e in 
-	raw_lambda bl' c
-
-    | CC_app (f,args) ->
-	let c = trad avoid nenv f
-	and cargs = List.map (trad avoid nenv) args in
-	RApp (dummy_loc, c, cargs)
-
-    | CC_tuple (_,_,[e]) -> 
-	trad avoid nenv e
-	
-    | CC_tuple (false,_,[e1;e2]) ->
-	let c1 = trad avoid nenv e1 
-	and c2 = trad avoid nenv e2 in
-	RApp (dummy_loc, RRef (dummy_loc,pair),
-	      [RHole (dummy_loc,ImplicitArg (pair,1));
-	       RHole (dummy_loc,ImplicitArg (pair,2));c1;c2])
-
-    | CC_tuple (dep,tyl,l) ->
-      	let n = List.length l in
-      	let cl = List.map (trad avoid nenv) l in
-      	let tuple = tuple_ref dep n in
-	let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in
-      	let args = tyl @ cl in
-	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
-
-    | CC_case (ty,b,el) ->
-	let c = trad avoid nenv b in
-	let cl = List.map (trad avoid nenv) el in
-	let ty = Detyping.detype (false,Global.env()) avoid nenv ty in
-	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None)
-
-    | CC_expr c -> 
-	Detyping.detype (false,Global.env()) avoid nenv c
-
-    | CC_hole c -> 
-	RCast (dummy_loc, RHole (dummy_loc, QuestionMark),
-               Detyping.detype (false,Global.env()) avoid nenv c)
-
-  in
-  trad [] empty_names_context p
diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli
deleted file mode 100644
index 160217f1dc..0000000000
--- a/contrib/correctness/pcic.mli
+++ /dev/null
@@ -1,24 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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 *)
-
-(*i $Id$ i*)
-
-open Past
-open Rawterm
-
-(* On-the-fly generation of needed (possibly dependent) tuples. *)
-
-val check_product_n : int -> unit
-val check_dep_product_n : int -> unit
-
-(* transforms intermediate functional programs into (raw) CIC terms *)
-
-val rawconstr_of_prog : cc_term -> rawconstr
-
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
deleted file mode 100644
index 4ac4e9704e..0000000000
--- a/contrib/correctness/pcicenv.ml
+++ /dev/null
@@ -1,118 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Term
-open Sign
-
-open Pmisc
-open Putil
-open Ptype
-open Past
-
-(* on redéfinit add_sign pour éviter de construire des environnements
- * avec des doublons (qui font planter la résolution des implicites !) *)
-
-(* VERY UGLY!! find some work around *)
-let modify_sign id t s =
-  fold_named_context
-    (fun ((x,b,ty) as d) sign ->
-      if x=id then add_named_decl (x,b,t) sign else add_named_decl d sign)
-    s ~init:empty_named_context
-
-let add_sign (id,t) s =
-  try 
-    let _ = lookup_named id s in
-    modify_sign id t s
-  with Not_found ->
-    add_named_decl (id,None,t) s
-
-let cast_set c = mkCast (c, mkSet)
-
-let set = mkCast (mkSet, mkType Univ.type1_univ)
-
-(* [cci_sign_of env] construit un environnement pour CIC ne comprenant que
- * les objets fonctionnels de l'environnement de programes [env]
- *)
-
-let cci_sign_of ren env =
-  Penv.fold_all 
-    (fun (id,v) sign ->
-       match v with
-	 | Penv.TypeV (Ref _ | Array _) -> sign
-	 | Penv.TypeV v -> 
-	     let ty = Pmonad.trad_ml_type_v ren env v in
-	     add_sign (id,cast_set ty) sign
-	 | Penv.Set -> add_sign (id,set) sign)
-    env (Global.named_context ())
-
-(* [sign_meta ren env fadd ini]
- * construit un environnement pour CIC qui prend en compte les variables
- * de programme. 
- * pour cela, cette fonction parcours tout l'envrionnement (global puis
- * local [env]) et pour chaque déclaration, ajoute ce qu'il faut avec la
- * fonction [fadd] s'il s'agit d'un mutable et directement sinon,
- * en partant de [ini].
- *)
-
-let sign_meta ren env fast ini =
-   Penv.fold_all 
-    (fun (id,v) sign ->
-       match v with
-	 | Penv.TypeV (Ref _ | Array _ as v) -> 
-	     let ty = Pmonad.trad_imp_type ren env v in
-	     fast sign id ty
-	 | Penv.TypeV v -> 
-	     let ty = Pmonad.trad_ml_type_v ren env v in
-	     add_sign (id,cast_set ty) sign
-	 | Penv.Set -> add_sign (id,set) sign)
-    env ini
-
-let add_sign_d dates (id,c) sign =
-  let sign =
-    List.fold_left (fun sign d -> add_sign (at_id id d,c) sign) sign dates
-  in
-    add_sign (id,c) sign
- 
-let sign_of add ren env =
-  sign_meta ren env
-    (fun sign id c -> let c = cast_set c in add (id,c) sign)
-    (Global.named_context ())
-
-let result_of sign = function
-    None   -> sign
-  | Some (id,c) -> add_sign (id, cast_set c) sign
-	
-let before_after_result_sign_of res ren env =
-  let dates = "" :: Prename.all_dates ren in
-  result_of (sign_of (add_sign_d dates) ren env) res
-
-let before_after_sign_of ren =
-  let dates = "" :: Prename.all_dates ren in
-  sign_of (add_sign_d dates) ren
-
-let before_sign_of ren =
-  let dates = Prename.all_dates ren in
-  sign_of (add_sign_d dates) ren
-
-let now_sign_of =
-  sign_of (add_sign_d [])
-
-
-(* environnement après traduction *)
-
-let trad_sign_of ren =
-  sign_of
-    (fun (id,c) sign -> add_sign (Prename.current_var ren id,c) sign)
-    ren
-
-
diff --git a/contrib/correctness/pcicenv.mli b/contrib/correctness/pcicenv.mli
deleted file mode 100644
index 32bd30daeb..0000000000
--- a/contrib/correctness/pcicenv.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Penv
-open Names
-open Term
-open Sign
-
-(* Translation of local programs environments into Coq signatures.
- * It is mainly used to type the pre/post conditions in the good
- * environment *)
-
-(* cci_sign_of: uniquement les objets purement fonctionnels de l'env. *)
-val cci_sign_of : Prename.t -> local_env -> named_context
-
-(* env. Coq avec seulement les variables X de l'env. *)
-val now_sign_of : Prename.t -> local_env -> named_context
-
-(* + les variables X@d pour toutes les dates de l'env. *)
-val before_sign_of : Prename.t -> local_env -> named_context
-
-(* + les variables `avant' X@ *)
-val before_after_sign_of : Prename.t -> local_env -> named_context
-val before_after_result_sign_of : ((identifier * constr) option)
-                        -> Prename.t -> local_env -> named_context
-
-(* env. des programmes traduits, avec les variables rennomées *)
-val trad_sign_of : Prename.t -> local_env -> named_context
-
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
deleted file mode 100644
index 01b0ef3c23..0000000000
--- a/contrib/correctness/pdb.ml
+++ /dev/null
@@ -1,165 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Term
-open Termops
-open Nametab
-open Constrintern
-
-open Ptype
-open Past
-open Penv
-
-let cci_global id =
-  try
-    global_reference id
-  with
-    _ -> raise Not_found
-
-let lookup_var ids locop id =
-  if List.mem id ids then
-    None
-  else begin
-    try Some (cci_global id)
-    with Not_found -> Perror.unbound_variable id locop
-  end
-
-let check_ref idl loc id =
-  if (not (List.mem id idl)) & (not (Penv.is_global id)) then
-    Perror.unbound_reference id loc
-
-(* db types : only check the references for the moment *)
-
-let rec check_type_v refs = function
-  | Ref v -> 
-      check_type_v refs v
-  | Array (c,v) -> 
-      check_type_v refs v
-  | Arrow (bl,c) -> 
-      check_binder refs c bl
-  | TypePure _ -> 
-      ()
-
-and check_type_c refs ((_,v),e,_,_) =
-  check_type_v refs v;
-  List.iter (check_ref refs None) (Peffect.get_reads e);
-  List.iter (check_ref refs None) (Peffect.get_writes e)
-  (* TODO: check_condition on p and q *)
-
-and check_binder refs c = function
-  | [] -> 
-      check_type_c refs c
-  | (id, BindType (Ref _ | Array _ as v)) :: bl -> 
-      check_type_v refs v;
-      check_binder (id :: refs) c bl
-  | (_, BindType v) :: bl ->
-      check_type_v refs v;
-      check_binder refs c bl
-  | _ :: bl -> 
-      check_binder refs c bl
-
-(* db binders *)
-
-let rec db_binders ((tids,pids,refs) as idl) = function
-  | [] -> 
-      idl, []
-  | (id, BindType (Ref _ | Array _ as v)) as b :: rem ->
-      check_type_v refs v;
-      let idl',rem' = db_binders (tids,pids,id::refs) rem in
-      idl', b :: rem'
-  | (id, BindType v) as b :: rem ->
-      check_type_v refs v;
-      let idl',rem' = db_binders (tids,id::pids,refs) rem in
-      idl', b :: rem'
-  | ((id, BindSet) as t) :: rem ->
-      let idl',rem' = db_binders (id::tids,pids,refs) rem in
-      idl', t :: rem'
-  | a :: rem ->
-      let idl',rem' = db_binders idl rem in idl', a :: rem'
-
-
-(* db programs *)
-  
-let db_prog e =
-  (* tids = type identifiers, ids = variables, refs = references and arrays *)
-  let rec db_desc ((tids,ids,refs) as idl) = function
-    | (Variable x) as t ->
-	(match lookup_var ids (Some e.loc) x with
-	     None -> t
-	   | Some c -> Expression c)
-    | (Acc x) as t ->
-	check_ref refs (Some e.loc) x;
-	t
-    | Aff (x,e1) ->
-	check_ref refs (Some e.loc) x;
-	Aff (x, db idl e1)
-    | TabAcc (b,x,e1) ->
-	check_ref refs (Some e.loc) x;
-	TabAcc(b,x,db idl e1)
-    | TabAff (b,x,e1,e2) ->
-	check_ref refs (Some e.loc) x;
-	TabAff (b,x, db idl e1, db idl e2)
-    | Seq bl ->
-	Seq (List.map (function
-			   Statement p -> Statement (db idl p)
-			 | x -> x) bl)
-    | If (e1,e2,e3) ->
-	If (db idl e1, db idl e2, db idl e3)
-    | While (b,inv,var,bl) ->
-	let bl' = List.map (function
-				Statement p -> Statement (db idl p)
-			      | x -> x) bl in
-	While (db idl b, inv, var, bl')
-	  
-    | Lam (bl,e) ->
-	let idl',bl' = db_binders idl bl in Lam(bl', db idl' e)
-    | Apply (e1,l) ->
-	Apply (db idl e1, List.map (db_arg idl) l)
-    | SApp (dl,l) ->
-	SApp (dl, List.map (db idl) l)
-    | LetRef (x,e1,e2) ->
-	LetRef (x, db idl e1, db (tids,ids,x::refs) e2)
-    | Let (x,e1,e2) ->
-	Let (x, db idl e1, db (tids,x::ids,refs) e2)
-	  
-    | LetRec (f,bl,v,var,e) ->
-	let (tids',ids',refs'),bl' = db_binders idl bl in
-	check_type_v refs' v;
-	LetRec (f, bl, v, var, db (tids',f::ids',refs') e)
-	  
-    | Debug (s,e1) ->
-	Debug (s, db idl e1)
-	  
-    | Expression _ as x -> x
-    | PPoint (s,d) -> PPoint (s, db_desc idl d)
-	  
-  and db_arg ((tids,_,refs) as idl) = function
-    | Term ({ desc = Variable id } as t) -> 
-	if List.mem id refs then Refarg id else Term (db idl t)
-    | Term t -> Term (db idl t)
-    | Type v as ty -> check_type_v refs v; ty
-    | Refarg _ -> assert false
-
-  and db idl e =
-    { desc = db_desc idl e.desc ;
-      pre = e.pre; post = e.post;
-      loc = e.loc; info = e.info }
-
-  in
-  let ids = Termops.ids_of_named_context (Global.named_context ()) in
-            (* TODO: separer X:Set et x:V:Set
-                     virer le reste (axiomes, etc.) *)
-  let vars,refs = all_vars (), all_refs () in
-  db ([],vars@ids,refs) e
-;;
-
diff --git a/contrib/correctness/pdb.mli b/contrib/correctness/pdb.mli
deleted file mode 100644
index 15b9132120..0000000000
--- a/contrib/correctness/pdb.mli
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Ptype
-open Past
-
-
-(* Here we separate local and global variables, we check the use of
- * references and arrays w.r.t the local and global environments, etc.
- * These functions directly raise UserError exceptions on bad programs.
- *)
-
-val check_type_v : Names.identifier list -> 'a ml_type_v -> unit
-
-val db_prog : program -> program
-
diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml
deleted file mode 100644
index dc527a5d41..0000000000
--- a/contrib/correctness/peffect.ml
+++ /dev/null
@@ -1,159 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Nameops
-open Pmisc
-
-(* The type of effects.
- *
- * An effect is composed of two lists (r,w) of variables.
- * The first one is the list of read-only variables
- * and the second one is the list of read-write variables.
- *
- * INVARIANT: 1. each list is sorted in decreasing order for Pervasives.compare
- *            2. there are no duplicate elements in each list
- *            3. the two lists are disjoint
- *)
-
-type t = identifier list * identifier list
-
-
-(* the empty effect *)
-
-let bottom = ([], [])
-
-(* basic operations *)
-
-let push x l =
-  let rec push_rec = function
-      [] -> [x]
-    | (y::rem) as l ->
-	if x = y then l else if x > y then x::l else y :: push_rec rem
-  in
-    push_rec l
-
-let basic_remove x l =
-  let rec rem_rec = function
-      [] -> []
-    | y::l -> if x = y then l else y :: rem_rec l
-  in
-    rem_rec l
-
-let mem x (r,w) = (List.mem x r) or (List.mem x w)
-
-let rec basic_union = function
-    [], s2 -> s2
-  | s1, [] -> s1
-  | ((v1::l1) as s1), ((v2::l2) as s2) ->
-      if v1 > v2 then
-	v1 :: basic_union (l1,s2)
-      else if v1 < v2 then
-	v2 :: basic_union (s1,l2)
-      else
-	v1 :: basic_union (l1,l2)
-
-(* adds reads and writes variables *)
-
-let add_read id ((r,w) as e) =
-  (* if the variable is already a RW it is ok, otherwise adds it as a RO. *)
-  if List.mem id w then
-    e
-  else
-    push id r, w
-
-let add_write id (r,w) =
-  (* if the variable is a RO then removes it from RO. Adds it to RW. *)
-  if List.mem id r then
-    basic_remove id r, push id w
-  else
-    r, push id w
-
-(* access *)
-
-let get_reads = basic_union
-let get_writes = snd
-let get_repr e = (get_reads e, get_writes e)
-
-(* tests *)
-
-let is_read  (r,_) id = List.mem id r
-let is_write (_,w) id = List.mem id w
-
-(* union and disjunction *)
-
-let union (r1,w1) (r2,w2) = basic_union (r1,r2), basic_union (w1,w2)
-
-let rec diff = function
-    [], s2 -> []
-  | s1, [] -> s1
-  | ((v1::l1) as s1), ((v2::l2) as s2) ->
-      if v1 > v2 then
-	v1 :: diff (l1,s2)
-      else if v1 < v2 then
-	diff (s1,l2)
-      else
-	diff (l1,l2)
-
-let disj (r1,w1) (r2,w2) =
-  let w1_w2 = diff (w1,w2) and w2_w1 = diff (w2,w1) in
-  let r = basic_union (basic_union (r1,r2), basic_union (w1_w2,w2_w1))
-  and w = basic_union (w1,w2) in
-  r,w
-
-(* comparison relation *)
-
-let le e1 e2 = failwith "effects: le: not yet implemented"
-
-let inf e1 e2 = failwith "effects: inf: not yet implemented"
-
-(* composition *)
-
-let compose (r1,w1) (r2,w2) =
-  let r = basic_union (r1, diff (r2,w1)) in
-  let w = basic_union (w1,w2) in
-    r,w
-
-(* remove *)
-
-let remove (r,w) name = basic_remove name r, basic_remove name w
-
-(* substitution *)
-
-let subst_list (x,x') l =
-  if List.mem x l then push x' (basic_remove x l) else l
-
-let subst_one (r,w) s = subst_list s r, subst_list s w
-
-let subst s e = List.fold_left subst_one e s
-
-(* pretty-print *)
-
-open Pp
-open Util
-open Himsg
-
-let pp (r,w) =
-  hov 0 (if r<>[] then
-	     (str"reads " ++
-		prlist_with_sep (fun () -> (str"," ++ spc ())) pr_id r)
-	   else (mt ()) ++
-	   spc () ++
-	   if w<>[] then
-	     (str"writes " ++
-		prlist_with_sep (fun ()-> (str"," ++ spc ())) pr_id w)
-	   else (mt ())
-)
-
-let ppr e =
-  Pp.pp (pp e)
-
diff --git a/contrib/correctness/peffect.mli b/contrib/correctness/peffect.mli
deleted file mode 100644
index 6295059a8d..0000000000
--- a/contrib/correctness/peffect.mli
+++ /dev/null
@@ -1,42 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-
-(* The abstract type of effects *)
-
-type t
-
-val bottom : t
-val add_read  : identifier -> t -> t
-val add_write : identifier -> t -> t
-
-val get_reads : t -> identifier list
-val get_writes : t -> identifier list
-val get_repr : t -> (identifier list) * (identifier list)
-
-val is_read  : t -> identifier -> bool    (* read-only *)
-val is_write : t -> identifier -> bool    (* read-write *)
-
-val compose : t -> t -> t
-
-val union : t -> t -> t
-val disj : t -> t -> t
-
-val remove : t -> identifier -> t
-
-val subst : (identifier * identifier) list -> t -> t
-
-
-val pp : t -> Pp.std_ppcmds
-val ppr : t -> unit
-
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
deleted file mode 100644
index b2c94cd6f9..0000000000
--- a/contrib/correctness/penv.ml
+++ /dev/null
@@ -1,240 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pmisc
-open Past
-open Ptype
-open Names
-open Nameops
-open Libobject
-open Library
-open Term
-
-(* Environments for imperative programs.
- *
- * An environment of programs is an association tables
- * from identifiers (Names.identifier) to types of values with effects
- * (ProgAst.ml_type_v), together with a list of these associations, since
- * the order is relevant (we have dependent types e.g. [x:nat; t:(array x T)])
- *)
-
-module Env = struct
-  type 'a t = ('a Idmap.t)
-	    * ((identifier * 'a) list)
-	    * ((identifier * (identifier * variant)) list)
-  let empty = Idmap.empty, [], []
-  let add id v (m,l,r) = (Idmap.add id v m, (id,v)::l, r)
-  let find id (m,_,_) = Idmap.find id m
-  let fold f (_,l,_) x0 = List.fold_right f l x0
-  let add_rec (id,var) (m,l,r) = (m,l,(id,var)::r)
-  let find_rec id (_,_,r) = List.assoc id r
-end
-
-(* Local environments *)
-
-type type_info = Set | TypeV of type_v
-
-type local_env = type_info Env.t
-
-let empty = (Env.empty : local_env)
-
-let add (id,v) = Env.add id (TypeV v)
-
-let add_set id = Env.add id Set
-
-let find id env =
-  match Env.find id env with TypeV v -> v | Set -> raise Not_found
-
-let is_local env id =
-  try
-    match Env.find id env with TypeV _ -> true | Set -> false
-  with
-      Not_found -> false
-
-let is_local_set env id =
-  try
-    match Env.find id env with TypeV _ -> false | Set -> true
-  with
-      Not_found -> false
-
-
-(* typed programs *)
-
-type typing_info = {
-  env : local_env;
-  kappa : constr ml_type_c
-}
-  
-type typed_program = (typing_info, constr) t
-
-
-(* The global environment.
- *
- * We have a global typing environment env
- * We also keep a table of programs for extraction purposes
- * and a table of initializations (still for extraction)
- *)
-
-let (env : type_info Env.t ref) = ref Env.empty
-
-let (pgm_table : (typed_program option) Idmap.t ref) = ref Idmap.empty
-
-let (init_table : constr Idmap.t ref) = ref Idmap.empty
-
-let freeze () = (!env, !pgm_table, !init_table)
-let unfreeze (e,p,i) = env := e; pgm_table := p; init_table := i
-let init () = 
-  env := Env.empty; pgm_table := Idmap.empty; init_table := Idmap.empty
-;;
-
-Summary.declare_summary "programs-environment"
-  { Summary.freeze_function = freeze;
-    Summary.unfreeze_function = unfreeze;
-    Summary.init_function = init;
-    Summary.survive_module = false;
-    Summary.survive_section = false }
-;;
-
-(* Operations on the global environment. *)
-
-let add_pgm id p = pgm_table := Idmap.add id p !pgm_table
-
-let cache_global (_,(id,v,p)) =
-  env := Env.add id v !env; add_pgm id p
-
-let type_info_app f = function Set -> Set | TypeV v -> TypeV (f v)
-
-let subst_global (_,s,(id,v,p)) = (id, type_info_app (type_v_knsubst s) v, p)
-
-let (inProg,outProg) =
-  declare_object { object_name = "programs-objects";
-                   cache_function = cache_global;
-                   load_function = (fun _ -> cache_global);
-                   open_function = (fun _ _ -> ());
-		   classify_function = (fun (_,x) -> Substitute x);
-		   subst_function = subst_global;
-		   export_function = (fun x -> Some x) }
-
-let is_mutable = function Ref _ | Array _ -> true | _ -> false
-
-let add_global id v p =
-  try
-    let _ = Env.find id !env in
-    Perror.clash id None
-  with
-    Not_found -> begin
-      let id' =
-	if is_mutable v then id 
-        else id_of_string ("prog_" ^ (string_of_id id)) 
-      in
-      Lib.add_leaf id' (inProg (id,TypeV v,p))
-    end
-
-let add_global_set id =
-  try
-    let _ = Env.find id !env in
-    Perror.clash id None
-  with
-    Not_found -> Lib.add_leaf id (inProg (id,Set,None))
-
-let is_global id =
-  try
-    match Env.find id !env with TypeV _ -> true | Set -> false
-  with
-    Not_found -> false
-
-let is_global_set id =
-  try
-    match Env.find id !env with TypeV _ -> false | Set -> true
-  with
-    Not_found -> false
-
-
-let lookup_global id =
-  match Env.find id !env with TypeV v -> v | Set -> raise Not_found
-
-let find_pgm id = Idmap.find id !pgm_table
-
-let all_vars () =
-  Env.fold
-    (fun (id,v) l -> match v with TypeV (Arrow _|TypePure _) -> id::l | _ -> l)
-    !env []
-
-let all_refs () =
-  Env.fold
-    (fun (id,v) l -> match v with TypeV (Ref _ | Array _) -> id::l | _ -> l)
-    !env []
-
-(* initializations *)
-
-let cache_init (_,(id,c)) =
-  init_table := Idmap.add id c !init_table
-
-let subst_init (_,s,(id,c)) = (id, subst_mps s c)
-
-let (inInit,outInit) =
-  declare_object { object_name = "programs-objects-init";
-                   cache_function = cache_init;
-                   load_function = (fun _ -> cache_init);
-		   open_function = (fun _ _-> ());
-		   classify_function = (fun (_,x) -> Substitute x);
-		   subst_function = subst_init;
-                   export_function = (fun x -> Some x) }
-
-let initialize id c = Lib.add_anonymous_leaf (inInit (id,c))
-
-let find_init id = Idmap.find id !init_table
-
-
-(* access in env, local then global *)
-
-let type_in_env env id =
-  try find id env with Not_found -> lookup_global id
-
-let is_in_env env id =
-  (is_global id) or (is_local env id)
-
-let fold_all f lenv x0 =
-  let x1 = Env.fold f !env x0 in
-  Env.fold f lenv x1
-
-
-(* recursions *)
-
-let add_recursion = Env.add_rec
-
-let find_recursion = Env.find_rec
-
-
-(* We also maintain a table of the currently edited proofs of programs
- * in order to add them in the environnement when the user does Save *)
-
-open Pp
-open Himsg
-
-let (edited : (type_v * typed_program) Idmap.t ref) = ref Idmap.empty
-
-let new_edited id v =
-  edited := Idmap.add id v !edited
-
-let is_edited id =
-  try let _ = Idmap.find id !edited in true with Not_found -> false
-
-let register id id' =
-  try
-    let (v,p) = Idmap.find id !edited in
-    let _ = add_global id' v (Some p) in
-    Flags.if_verbose 
-      msgnl (hov 0 (str"Program " ++ pr_id id' ++ spc () ++ str"is defined"));
-    edited := Idmap.remove id !edited
-  with Not_found -> ()
-
diff --git a/contrib/correctness/penv.mli b/contrib/correctness/penv.mli
deleted file mode 100644
index 72b4131379..0000000000
--- a/contrib/correctness/penv.mli
+++ /dev/null
@@ -1,87 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Ptype
-open Past
-open Names
-open Libnames
-open Term
-
-(* Environment for imperative programs.
- * 
- * Here we manage the global environment, which is imperative,
- * and we provide a functional local environment. 
- *
- * The most important functions, is_in_env, type_in_env and fold_all
- * first look in the local environment then in the global one.
- *)
-
-(* local environments *)
-
-type local_env
-
-val empty : local_env
-val add : (identifier * type_v) -> local_env -> local_env
-val add_set : identifier -> local_env -> local_env
-val is_local : local_env -> identifier -> bool
-val is_local_set : local_env -> identifier -> bool
-
-(* typed programs *)
-
-type typing_info = {
-  env : local_env;
-  kappa : constr ml_type_c
-}
-  
-type typed_program = (typing_info, constr) t
-
-(* global environment *)
-
-val add_global : identifier -> type_v -> typed_program option -> object_name
-val add_global_set : identifier -> object_name
-val is_global : identifier -> bool
-val is_global_set : identifier -> bool
-val lookup_global : identifier -> type_v
-
-val all_vars : unit -> identifier list
-val all_refs : unit -> identifier list
-
-(* a table keeps the program (for extraction) *)
-
-val find_pgm : identifier -> typed_program option
-
-(* a table keeps the initializations of mutable objects *)
-
-val initialize : identifier -> constr -> unit
-val find_init : identifier -> constr
-
-(* access in env (local then global) *)
-
-val type_in_env : local_env -> identifier -> type_v
-val is_in_env : local_env -> identifier -> bool
-
-type type_info = Set | TypeV of type_v
-val fold_all : (identifier * type_info -> 'a -> 'a) -> local_env -> 'a -> 'a
-
-(* local environnements also contains a list of recursive functions
- * with the associated variant *)
-
-val add_recursion : identifier * (identifier*variant) -> local_env -> local_env
-val find_recursion : identifier -> local_env -> identifier * variant
-
-(* We also maintain a table of the currently edited proofs of programs
- * in order to add them in the environnement when the user does Save *)
-
-val new_edited : identifier -> type_v * typed_program -> unit
-val is_edited : identifier -> bool
-val register : identifier -> identifier -> unit
-
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
deleted file mode 100644
index 9e1ab322f0..0000000000
--- a/contrib/correctness/perror.ml
+++ /dev/null
@@ -1,172 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Term
-open Himsg
-
-open Ptype
-open Past
-
-let is_mutable = function Ref _ | Array _ -> true | _ -> false
-let is_pure = function TypePure _ -> true | _ -> false
-
-let raise_with_loc = function
-  | None -> raise
-  | Some loc -> Stdpp.raise_with_loc loc 
-
-let unbound_variable id loc =
-  raise_with_loc loc
-    (UserError ("Perror.unbound_variable",
-    (hov 0 (str"Unbound variable" ++ spc () ++ pr_id id ++ fnl ()))))
-
-let unbound_reference id loc =
-  raise_with_loc loc
-    (UserError ("Perror.unbound_reference",
-    (hov 0 (str"Unbound reference" ++ spc () ++ pr_id id ++ fnl ()))))
-
-let clash id loc =
-  raise_with_loc loc
-    (UserError ("Perror.clash",
-    (hov 0 (str"Clash with previous constant" ++ spc () ++
-    str(string_of_id id) ++ fnl ()))))
-
-let not_defined id =
-  raise
-    (UserError ("Perror.not_defined",
-	       	(hov 0 (str"The object" ++ spc () ++ pr_id id ++ spc () ++
-			  str"is not defined" ++ fnl ()))))
-
-let check_for_reference loc id = function
-    Ref _ -> ()
-  | _ -> Stdpp.raise_with_loc loc 
-	(UserError ("Perror.check_for_reference",
-		    hov 0 (pr_id id ++ spc () ++ 
-			     str"is not a reference")))
-
-let check_for_array loc id = function
-    Array _ -> ()
-  | _ -> Stdpp.raise_with_loc loc 
-	(UserError ("Perror.check_for_array",
-		    hov 0 (pr_id id ++ spc () ++ 
-			     str"is not an array")))
-
-let is_constant_type s = function
-    TypePure c ->
-      let id = id_of_string s in
-      let c' = Constrintern.global_reference id in
-      Reductionops.is_conv (Global.env()) Evd.empty c c'
-  | _ -> false 
-
-let check_for_index_type loc v =
-  let is_index = is_constant_type "Z" v in
-  if not is_index then
-    Stdpp.raise_with_loc loc 
-      (UserError ("Perror.check_for_index",
-		  hov 0 (str"This expression is an index" ++ spc () ++ 
-			   str"and should have type int (Z)")))
-
-let check_no_effect loc ef =
-  if not (Peffect.get_writes ef = []) then
-    Stdpp.raise_with_loc loc 
-      (UserError ("Perror.check_no_effect",
-		  hov 0 (str"A boolean should not have side effects"
-)))
-
-let should_be_boolean loc =
-  Stdpp.raise_with_loc loc 
-    (UserError ("Perror.should_be_boolean",
-		hov 0 (str"This expression is a test:" ++ spc () ++
-			 str"it should have type bool")))
-
-let test_should_be_annotated loc =
-  Stdpp.raise_with_loc loc 
-    (UserError ("Perror.test_should_be_annotated",
-		hov 0 (str"This test should be annotated")))
-
-let if_branches loc =
-  Stdpp.raise_with_loc loc 
-    (UserError ("Perror.if_branches",
-		hov 0 (str"The two branches of an `if' expression" ++ spc () ++
-			 str"should have the same type")))
-
-let check_for_not_mutable loc v =
-  if is_mutable v then
-    Stdpp.raise_with_loc loc 
-      (UserError ("Perror.check_for_not_mutable",
-		  hov 0 (str"This expression cannot be a mutable")))
-
-let check_for_pure_type loc v =
-  if not (is_pure v) then
-    Stdpp.raise_with_loc loc 
-      (UserError ("Perror.check_for_pure_type",
-		  hov 0 (str"This expression must be pure" ++ spc () ++
-			   str"(neither a mutable nor a function)")))
-
-let check_for_let_ref loc v =
-  if not (is_pure v) then
-    Stdpp.raise_with_loc loc 
-      (UserError ("Perror.check_for_let_ref",
-		  hov 0 (str"References can only be bound in pure terms")))
-
-let informative loc s =
-  Stdpp.raise_with_loc loc 
-  (UserError ("Perror.variant_informative",
-	      hov 0 (str s ++ spc () ++ str"must be informative")))
-
-let variant_informative loc = informative loc "Variant"
-let should_be_informative loc = informative loc "This term"
-
-let app_of_non_function loc =
-  Stdpp.raise_with_loc loc 
-  (UserError ("Perror.app_of_non_function",
-	      hov 0 (str"This term cannot be applied" ++ spc () ++
-		       str"(either it is not a function" ++ spc () ++
-		       str"or it is applied to non pure arguments)")))
-  
-let partial_app loc =
-  Stdpp.raise_with_loc loc 
-  (UserError ("Perror.partial_app",
-	      hov 0 (str"This function does not have" ++
-		       spc () ++ str"the right number of arguments")))
-  
-let expected_type loc s =
-  Stdpp.raise_with_loc loc 
-  (UserError ("Perror.expected_type",
-	      hov 0 (str"Argument is expected to have type" ++ spc () ++ s)))
-
-let expects_a_type id loc =
-  Stdpp.raise_with_loc loc 
-  (UserError ("Perror.expects_a_type",
-	      hov 0 (str"The argument " ++ pr_id id ++ spc () ++
-		       str"in this application is supposed to be a type")))
-
-let expects_a_term id =
-  raise
-  (UserError ("Perror.expects_a_type",
-	      hov 0 (str"The argument " ++ pr_id id ++ spc () ++
-		       str"in this application is supposed to be a term")))
-
-let should_be_a_variable loc =
-  Stdpp.raise_with_loc loc 
-  (UserError ("Perror.should_be_a_variable",
-	      hov 0 (str"Argument should be a variable")))
-   
-let should_be_a_reference loc =
-  Stdpp.raise_with_loc loc 
-  (UserError ("Perror.should_be_a_reference",
-	      hov 0 (str"Argument of function should be a reference")))
-
-   
diff --git a/contrib/correctness/perror.mli b/contrib/correctness/perror.mli
deleted file mode 100644
index 24c77bb5da..0000000000
--- a/contrib/correctness/perror.mli
+++ /dev/null
@@ -1,47 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp
-open Util
-open Names
-open Ptype
-open Past
-
-val unbound_variable : identifier -> loc option -> 'a
-val unbound_reference : identifier -> loc option -> 'a
-
-val clash : identifier -> loc option -> 'a
-val not_defined : identifier -> 'a
-
-val check_for_reference : loc -> identifier -> type_v -> unit
-val check_for_array     : loc -> identifier -> type_v -> unit
-
-val check_for_index_type : loc -> type_v -> unit
-val check_no_effect : loc -> Peffect.t -> unit
-val should_be_boolean : loc -> 'a
-val test_should_be_annotated : loc -> 'a
-val if_branches : loc -> 'a
-
-val check_for_not_mutable : loc -> type_v -> unit
-val check_for_pure_type : loc -> type_v -> unit
-val check_for_let_ref : loc -> type_v -> unit
-
-val variant_informative : loc -> 'a
-val should_be_informative : loc -> 'a
-
-val app_of_non_function : loc -> 'a
-val partial_app : loc -> 'a
-val expected_type : loc -> std_ppcmds -> 'a
-val expects_a_type : identifier -> loc -> 'a
-val expects_a_term : identifier -> 'a
-val should_be_a_variable : loc -> 'a
-val should_be_a_reference : loc -> 'a
diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
deleted file mode 100644
index b1c78480ab..0000000000
--- a/contrib/correctness/pextract.ml
+++ /dev/null
@@ -1,473 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp_control
-open Pp
-open Util
-open System
-open Names
-open Term
-open Himsg
-open Reduction
-
-open Putil
-open Ptype
-open Past
-open Penv
-open Putil
-
-let extraction env c =
-  let ren = initial_renaming env in
-  let sign = Pcicenv.now_sign_of ren env in
-  let fsign = Mach.fsign_of_sign (Evd.mt_evd()) sign in
-  match Mach.infexecute (Evd.mt_evd()) (sign,fsign) c with
-    | (_,Inf j) -> j._VAL
-    | (_,Logic) -> failwith "Prog_extract.pp: should be informative"
-
-(* les tableaux jouent un role particulier, puisqu'ils seront extraits
- * vers des tableaux ML *)
-
-let sp_access = coq_constant ["correctness"; "Arrays"] "access"
-let access = ConstRef sp_access
-
-let has_array = ref false
-
-let pp_conversions () =
-  (str"\
-let rec int_of_pos = function
-    XH -> 1
-  | XI p -> 2 * (int_of_pos p) + 1
-  | XO p -> 2 * (int_of_pos p)
- ++ ++
-
-let int_of_z = function
-    ZERO -> 0
-  | POS p -> int_of_pos p
-  | NEG p -> -(int_of_pos p)
- ++ ++
-") (* '"' *)
-
-(* collect all section-path in a CIC constant *)
-
-let spset_of_cci env c =
-  let spl = Fw_env.collect (extraction env c) in
-  let sps = List.fold_left (fun e x -> SpSet.add x e) SpSet.empty spl in
-  has_array := !has_array or (SpSet.mem sp_access sps) ++
-  SpSet.remove sp_access sps
-
-
-(* collect all Coq constants and all pgms appearing in a given program *)
-
-let add_id env ((sp,ids) as s) id =
-  if is_local env id then
-    s
-  else if is_global id then
-    (sp,IdSet.add id ids)
-  else
-    try (SpSet.add (Nametab.sp_of_id FW id) sp,ids) with Not_found -> s
-
-let collect env =
-  let rec collect_desc env s = function
-    | Var x -> add_id env s x
-    | Acc x -> add_id env s x
-    | Aff (x,e1) -> add_id env (collect_rec env s e1) x
-    | TabAcc (_,x,e1) ->
-	has_array := true ++
-	add_id env (collect_rec env s e1) x
-    | TabAff (_,x,e1,e2) ->
-	has_array := true ++
-	add_id env (collect_rec env (collect_rec env s e1) e2) x
-    | Seq bl ->
-	List.fold_left (fun s st -> match st with
-			    Statement p -> collect_rec env s p
-			  | _ -> s) s bl
-    | If (e1,e2,e3) ->
-    	collect_rec env (collect_rec env (collect_rec env s e1) e2) e3
-    | While (b,_,_,bl) ->
-	let s = List.fold_left (fun s st -> match st with
-				    Statement p -> collect_rec env s p
-				  | _ -> s) s bl in
-	  collect_rec env s b
-    | Lam (bl,e) ->
-	collect_rec (traverse_binders env bl) s e
-    | App (e1,l) ->
-	let s = List.fold_left (fun s a -> match a with
-				    Term t -> collect_rec env s t
-				  | Type _ | Refarg _ -> s) s l in
-	  collect_rec env s e1
-    | SApp (_,l) ->
-	List.fold_left (fun s a -> collect_rec env s a) s l
-    | LetRef (x,e1,e2) ->
-	let (_,v),_,_,_ = e1.info.kappa in
-	  collect_rec (add (x,Ref v) env) (collect_rec env s e1) e2
-    | LetIn (x,e1,e2) ->
-	let (_,v),_,_,_ = e1.info.kappa in
-	  collect_rec (add (x,v) env) (collect_rec env s e1) e2
-    | LetRec (f,bl,_,_,e) ->
-	let env' = traverse_binders env bl in
-	let env'' = add (f,make_arrow bl e.info.kappa) env' in
-	  collect_rec env'' s e
-    | Debug (_,e1) -> collect_rec env s e1
-    | PPoint (_,d) -> collect_desc env s d
-    | Expression c ->
-	let (sp,ids) = s in
-	let sp' = spset_of_cci env c in
-	SpSet.fold 
-	  (fun s (es,ei) ->
-	     let id = basename s in
-	     if is_global id then (*SpSet.add s*)es,IdSet.add id ei
-	     else SpSet.add s es,ei)
-	  sp' (sp,ids)
-
-  and collect_rec env s p = collect_desc env s p.desc
-
-  in
-  collect_rec env (SpSet.empty,IdSet.empty)
-
-
-(* On a besoin de faire du renommage, tout comme pour l'extraction des
- * termes Coq. En ce qui concerne les globaux, on utilise la table de
- * Fwtoml. Pour les objects locaux, on introduit la structure de
- * renommage rename_struct
- *)
-
-module Ocaml_ren = Ocaml.OCaml_renaming
-
-let rename_global id =
-  let id' = Ocaml_ren.rename_global_term !Fwtoml.globals (Name id) in
-  Fwtoml.add_global_renaming (id,id') ++
-  id'
-
-type rename_struct = { rn_map : identifier IdMap.t;
-		       rn_avoid : identifier list }
-
-let rn_empty = { rn_map = IdMap.empty; rn_avoid = [] }
-
-let rename_local rn id =
-  let id' = Ocaml_ren.rename_term (!Fwtoml.globals@rn.rn_avoid) (Name id) in
-  { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid },
-  id'
-
-let get_local_name rn id = IdMap.find id rn.rn_map
-
-let get_name env rn id =
-  if is_local env id then
-    get_local_name rn id
-  else
-    Fwtoml.get_global_name id
-
-let rec rename_binders rn = function
-  | [] -> rn
-  | (id,_) :: bl -> let rn',_ = rename_local rn id in rename_binders rn' bl
-
-(* on a bespoin d'un pretty-printer de constr particulier, qui reconnaisse
- * les acces a des references et dans des tableaux, et qui de plus n'imprime
- * pas de GENTERM lorsque des identificateurs ne sont pas visibles.
- * Il est simplifie dans la mesure ou l'on a ici que des constantes et
- * des applications.
- *)
-
-let putpar par s =
-  if par then (str"(" ++ s ++ str")") else s
-
-let is_ref env id =
-  try
-    (match type_in_env env id with Ref _ -> true | _ -> false)
-  with
-    Not_found -> false
-
-let rec pp_constr env rn = function
-  | VAR id ->
-      if is_ref env id then 
-	(str"!" ++ pID (get_name env rn id)) 
-      else
-	pID (get_name env rn id)
-  | DOPN((Const _|MutInd _|MutConstruct _) as oper, _) ->
-      pID (Fwtoml.name_of_oper oper)
-  | DOPN(AppL,v) ->
-      if Array.length v = 0 then
-	  (mt ())
-      else begin
-	match v.(0) with
-	    DOPN(Const sp,_) when sp = sp_access ->
-	      (pp_constr env rn v.(3) ++ 
-		 str".(int_of_z " ++ pp_constr env rn v.(4) ++ str")")
-	  | _ ->
-	      hov 2 (putpar true (prvect_with_sep (fun () -> (spc ()))
-				    (pp_constr env rn) v))
-      end
-  | DOP2(Cast,c,_) -> pp_constr env rn c
-  | _ -> failwith "Prog_extract.pp_constr: unexpected constr"
-
-
-(* pretty-print of imperative programs *)
-
-let collect_lambda = 
-  let rec collect acc p = match p.desc with
-    | Lam(bl,t) -> collect (bl@acc) t
-    | x         -> acc,p
-  in 
-  collect []
-
-let pr_binding rn = 
-  prlist_with_sep (fun () -> (mt ()))
-    (function 
-       | (id,(Untyped | BindType _)) -> 
-	   (str" " ++ pID (get_local_name rn id))
-       | (id,BindSet) -> (mt ()))
-
-let pp_prog id =
-  let rec pp_d env rn par = function
-    | Var x -> pID (get_name env rn x)
-    | Acc x -> (str"!" ++ pID (get_name env rn x))
-    | Aff (x,e1) -> (pID (get_name env rn x) ++ 
-		       str" := " ++ hov 0 (pp env rn false e1))
-    | TabAcc (_,x,e1) ->
-	(pID (get_name env rn x) ++ 
-	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")")
-    | TabAff (_,x,e1,e2) ->
-	(pID (get_name env rn x) ++
-	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")" ++
-	   str" <-" ++ spc () ++ hov 2 (pp env rn false e2))
-    | Seq bl ->
-	(str"begin" ++ fnl () ++
-	   str"  " ++ hov 0 (pp_block env rn bl) ++ fnl () ++
-	   str"end")
-    | If (e1,e2,e3) ->
-	putpar par (str"if " ++ (pp env rn false e1) ++
-		      str" then" ++ fnl () ++
-		      str"  " ++ hov 0 (pp env rn false e2) ++ fnl () ++
-		      str"else" ++ fnl () ++
-		      str"  " ++ hov 0 (pp env rn false e3))
-	(* optimisations : then begin .... end else begin ... end *)
-    | While (b,inv,_,bl) ->
-	(str"while " ++ (pp env rn false b) ++ str" do" ++ fnl () ++		    
-	   str"  " ++
-	   hov 0 ((match inv with
-			 None -> (mt ()) 
-		       | Some c -> (str"(* invariant: " ++ pTERM c.a_value ++ 
-				      str" *)" ++ fnl ())) ++
-		    pp_block env rn bl) ++ fnl () ++
-	   str"done")
-    | Lam (bl,e) ->
-	let env' = traverse_binders env bl in
-	let rn' = rename_binders rn bl in
-	  putpar par 
-	    (hov 2 (str"fun" ++ pr_binding rn' bl ++ str" ->" ++
-		      spc () ++ pp env' rn' false e))
-    | SApp ((Var id)::_,  [e1; e2])
-	when id = connective_and or id = connective_or ->
-	  let conn = if id = connective_and then "&" else "or" in
-	  putpar par 
-	    (hov 0 (pp env rn true e1 ++ spc () ++ str conn ++ spc () ++
-		      pp env rn true e2))
-    | SApp ((Var id)::_, [e]) when id = connective_not ->
-	putpar par 
-	  (hov 0 (str"not" ++ spc () ++ pp env rn true e))
-    | SApp _ ->
-	invalid_arg "Prog_extract.pp_prog (SApp)"
-    | App(e1,[]) ->
-	hov 0 (pp env rn false e1)
-    | App (e1,l) ->
-	putpar true
-	  (hov 2 (pp env rn true e1 ++
-		    prlist (function 
-				Term p -> (spc () ++ pp env rn true p)
-			      | Refarg x -> (spc () ++ pID (get_name env rn x))
-			      | Type _ -> (mt ())) 
-		      l))
-    | LetRef (x,e1,e2) ->
-	let (_,v),_,_,_ = e1.info.kappa in
-	let env' = add (x,Ref v) env in
-	let rn',x' = rename_local rn x in
-	putpar par 
-	  (hov 0 (str"let " ++ pID x' ++ str" = ref " ++ pp env rn false e1 ++
-		    str" in" ++ fnl () ++ pp env' rn' false e2))
-    | LetIn (x,e1,e2) ->
-	let (_,v),_,_,_ = e1.info.kappa in
-	let env' = add (x,v) env in
-	let rn',x' = rename_local rn x in
-	putpar par 
-	  (hov 0 (str"let " ++ pID x' ++ str" = " ++ pp env rn false e1 ++
-		    str" in" ++ fnl () ++ pp env' rn' false e2))
-    | LetRec (f,bl,_,_,e) ->
-	let env' = traverse_binders env bl in
-	let rn' = rename_binders rn bl in
-	let env'' = add (f,make_arrow bl e.info.kappa) env' in
-	let rn'',f' = rename_local rn' f in
-	putpar par 
-	  (hov 0 (str"let rec " ++ pID f' ++ pr_binding rn' bl ++ str" =" ++ fnl () ++
-		    str"  " ++ hov 0 (pp env'' rn'' false e) ++ fnl () ++
-		    str"in " ++ pID f'))
-    | Debug (_,e1) -> pp env rn par e1
-    | PPoint (_,d) -> pp_d env rn par d
-    | Expression c -> 
-	pp_constr env rn (extraction env c)
-
-  and pp_block env rn bl =
-    let bl =
-      map_succeed (function Statement p -> p | _ -> failwith "caught") bl
-    in
-      prlist_with_sep (fun () -> (str";" ++ fnl ()))
-      	(fun p -> hov 0 (pp env rn false p)) bl
-
-  and pp env rn par p = 
-    (pp_d env rn par p.desc)
-
-  and pp_mut v c = match v with
-    | Ref _ ->
-	(str"ref " ++ pp_constr empty rn_empty (extraction empty c))
-    | Array (n,_) ->
-	(str"Array.create " ++ cut () ++
-	   putpar true 
-	     (str"int_of_z " ++
-		pp_constr empty rn_empty (extraction empty n)) ++
-	   str" " ++ pp_constr empty rn_empty (extraction empty c))
-    | _ -> invalid_arg "pp_mut"
-  in
-  let v = lookup_global id in
-  let id' = rename_global id in
-    if is_mutable v then
-      try
-	let c = find_init id in
-	hov 0 (str"let " ++ pID id' ++ str" = " ++ pp_mut v c)
-      with Not_found -> 
-	errorlabstrm "Prog_extract.pp_prog"
-	  (str"The variable " ++ pID id ++
-	     str" must be initialized first !")
-    else
-      match find_pgm id with
-	| None -> 
-	    errorlabstrm "Prog_extract.pp_prog"
-	      (str"The program " ++ pID id ++
-		 str" must be realized first !")
-      	| Some p ->
-	    let bl,p = collect_lambda p in
-	    let rn = rename_binders rn_empty bl in
-	    let env = traverse_binders empty bl in
-	    hov 0  (str"let " ++ pID id' ++ pr_binding rn bl ++ str" =" ++ fnl () ++ 
-		      str"  " ++ hov 2 (pp env rn false p))
-
-(* extraction des programmes impératifs/fonctionnels vers ocaml *)
-
-(* Il faut parfois importer des modules non ouverts, sinon
- * Ocaml.OCaml_pp_file.pp echoue en disant "machin is not a defined
- * informative object". Cela dit, ce n'est pas tres satisfaisant, vu que
- * la constante existe quand meme: il vaudrait mieux contourner l'echec
- * de ml_import.fwsp_of_id
- *)
-
-let import sp = match repr_path sp with
-  | [m],_,_ ->
-      begin
-	try Library.import_export_module m true
-        with _ -> ()
-      end
-  | _ -> ()
-
-let pp_ocaml file prm =
-  has_array := false ++
-  (* on separe objects Coq et programmes *)
-  let cic,pgms =
-    List.fold_left
-      (fun (sp,ids) id ->
-	 if is_global id then (sp,IdSet.add id ids) else (IdSet.add id sp,ids))
-      (IdSet.empty,IdSet.empty) prm.needed
-  in
-  (* on met les programmes dans l'ordre et pour chacun on recherche les
-   * objects Coq necessaires, que l'on rajoute a l'ensemble cic *)
-  let cic,_,pgms =
-    let o_pgms = fold_all (fun (id,_) l -> id::l) empty [] in
-    List.fold_left
-      (fun (cic,pgms,pl) id -> 
-	 if IdSet.mem id pgms then
-	   let spl,pgms' =
-	     try
-	       (match find_pgm id with
-		  | Some p -> collect empty p
-		  | None ->
-		      (try 
-			 let c = find_init id in
-			 spset_of_cci empty c,IdSet.empty
-		       with Not_found -> 
-			 SpSet.empty,IdSet.empty))
-	     with Not_found -> SpSet.empty,IdSet.empty
-	   in
-	   let cic' = 
-	     SpSet.fold 
-	       (fun sp cic -> import sp ++ IdSet.add (basename sp) cic)
-	       spl cic
-	   in
-	   (cic',IdSet.union pgms pgms',id::pl)
-	 else
-	   (cic,pgms,pl)) 
-      (cic,pgms,[]) o_pgms
-  in
-  let cic = IdSet.elements cic in
-  (* on pretty-print *)
-  let prm' = { needed = cic ++ expand = prm.expand ++ 
-	       expansion = prm.expansion ++ exact = prm.exact } 
-  in
-  let strm = (Ocaml.OCaml_pp_file.pp_recursive prm' ++
-		fnl () ++ fnl () ++
-		if !has_array then pp_conversions() else (mt ()) ++
-		prlist (fun p -> (pp_prog p ++ fnl () ++ str";;" ++ fnl () ++ fnl ()))
-		  pgms
-)
-  in
-  (* puis on ecrit dans le fichier *)
-  let chan = open_trapping_failure open_out file ".ml" in
-  let ft = with_output_to chan in
-  begin
-    try  pP_with ft strm ++ pp_flush_with ft ()
-    with e -> pp_flush_with ft () ++ close_out chan ++ raise e
-  end ++
-  close_out chan
-    
-
-(* Initializations of mutable objects *)
-
-let initialize id com =
-  let loc = Ast.loc com in
-  let c = constr_of_com (Evd.mt_evd()) (initial_sign()) com in
-  let ty = 
-    Reductionops.nf_betaiota (type_of (Evd.mt_evd()) (initial_sign()) c) in
-  try
-    let v = lookup_global id in
-    let ety = match v with 
-      | Ref (TypePure c) -> c | Array (_,TypePure c) -> c
-      | _ -> raise Not_found 
-    in
-    if conv (Evd.mt_evd()) ty ety then
-      initialize id c
-    else
-      errorlabstrm "Prog_extract.initialize"
-	(str"Not the expected type for the mutable " ++ pID id)
-  with Not_found -> 
-    errorlabstrm "Prog_extract.initialize"
-      (pr_id id ++ str" is not a mutable")
-
-(* grammaire *)
-
-open Vernacinterp
-
-let _ = vinterp_add "IMPERATIVEEXTRACTION"
-	  (function 
-	     | VARG_STRING file :: rem ->
-		 let prm = parse_param rem in (fun () -> pp_ocaml file prm)
-	     | _ -> assert false)
-	  
-let _ = vinterp_add "INITIALIZE"
-	  (function 
-	     | [VARG_IDENTIFIER id; VARG_COMMAND com] ->
-		 (fun () -> initialize id com)
-	     | _ -> assert false)
diff --git a/contrib/correctness/pextract.mli b/contrib/correctness/pextract.mli
deleted file mode 100644
index edf6cac8fc..0000000000
--- a/contrib/correctness/pextract.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-
-val pp_ocaml : string -> unit
-
-
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
deleted file mode 100644
index aaa304fe53..0000000000
--- a/contrib/correctness/pmisc.ml
+++ /dev/null
@@ -1,222 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Term
-open Libnames
-open Topconstr
-
-(* debug *)
-
-let deb_mess s =
-  if !Flags.debug then begin
-    msgnl s; pp_flush()
-  end
-
-let deb_print f x =
-  if !Flags.debug then begin
-    msgnl (f x); pp_flush()
-  end
-
-let list_of_some = function
-    None -> []
-  | Some x -> [x]
-
-let difference l1 l2 =
-  let rec diff = function
-      [] -> []
-    | a::rem -> if List.mem a l2 then diff rem else a::(diff rem)
-  in
-    diff l1
-
-(* TODO: these functions should be moved in the code of Coq *)
-
-let reraise_with_loc loc f x =
-  try f x with Util.UserError (_,_) as e -> Stdpp.raise_with_loc loc e
-
-
-(* functions on names *)
-
-let at = if !Flags.v7 then "@" else "'at'"
-
-let at_id id d = id_of_string ((string_of_id id) ^ at ^ d)
-
-let is_at id =
-  try
-    let _ = string_index_from (string_of_id id) 0 at in true
-  with Not_found ->
-    false
-
-let un_at id =
-  let s = string_of_id id in
-    try
-      let n = string_index_from s 0 at in
-    	id_of_string (String.sub s 0 n),
-	String.sub s (n + String.length at)
-          (String.length s - n - String.length at)
-    with Not_found ->
-      invalid_arg "un_at"
-
-let renaming_of_ids avoid ids =
-  let rec rename avoid = function
-      [] -> [], avoid
-    | x::rem ->
-	let al,avoid = rename avoid rem in
-	let x' = next_ident_away x avoid in
-	  (x,x')::al, x'::avoid
-  in
-    rename avoid ids
-
-let result_id = id_of_string "result"
-
-let adr_id id = id_of_string ("adr_" ^ (string_of_id id))
-
-(* hypotheses names *)
-
-let next s r = function
-    Anonymous -> incr r; id_of_string (s ^ string_of_int !r)
-  | Name id -> id
-
-let reset_names,pre_name,post_name,inv_name,
-    test_name,bool_name,var_name,phi_name,for_name,label_name =
-  let pre = ref 0 in
-  let post = ref 0 in
-  let inv = ref 0 in
-  let test = ref 0 in
-  let bool = ref 0 in
-  let var = ref 0 in
-  let phi = ref 0 in
-  let forr = ref 0 in
-  let label = ref 0 in
-    (fun () -> 
-       pre := 0; post := 0; inv := 0; test := 0; 
-       bool := 0; var := 0; phi := 0; label := 0),
-    (next "Pre" pre),
-    (next "Post" post),
-    (next "Inv" inv),
-    (next "Test" test),
-    (fun () -> next "Bool" bool Anonymous),
-    (next "Variant" var),
-    (fun () -> next "rphi" phi Anonymous),
-    (fun () -> next "for" forr Anonymous),
-    (fun () -> string_of_id (next "Label" label Anonymous))
-
-let default = id_of_string "x_"
-let id_of_name = function Name id -> id | Anonymous -> default
-
-
-(* functions on CIC terms *)
-
-let isevar = Evarutil.new_evar_in_sign (Global.env ())
-
-(* Substitutions of variables by others. *)
-let subst_in_constr alist =
-  let alist' = List.map (fun (id,id') -> (id, mkVar id')) alist in
-  replace_vars alist'
-
-(*
-let subst_in_ast alist ast =
-  let rec subst = function
-      Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
-    | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
-    | x -> x
-  in
-    subst ast
-*)
-(*
-let subst_ast_in_ast alist ast =
-  let rec subst = function
-      Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
-    | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
-    | x -> x
-  in
-    subst ast
-*)
-
-let rec subst_in_ast alist = function
-  | CRef (Ident (loc,id)) ->
-      CRef (Ident (loc,(try List.assoc id alist with Not_found -> id)))
-  | x -> map_constr_expr_with_binders subst_in_ast List.remove_assoc alist x
-
-let rec subst_ast_in_ast alist = function
-  | CRef (Ident (_,id)) as x -> (try List.assoc id alist with Not_found -> x)
-  | x ->
-      map_constr_expr_with_binders subst_ast_in_ast List.remove_assoc alist x
-
-(* subst. of variables by constr *)
-let real_subst_in_constr = replace_vars
-
-(* Coq constants *)
-
-let coq_constant d s =
-  Libnames.encode_kn
-    (make_dirpath (List.rev (List.map id_of_string ("Coq"::d))))
-    (id_of_string s)
-
-let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
-let coq_true = mkConstruct ((bool_sp,0),1)
-let coq_false = mkConstruct ((bool_sp,0),2)
-
-let constant s =
-  let id = Constrextern.id_of_v7_string s in
-  Constrintern.global_reference id
-
-let connective_and = id_of_string "prog_bool_and"
-let connective_or  = id_of_string "prog_bool_or"
-let connective_not = id_of_string "prog_bool_not"
-
-let is_connective id =
-  id = connective_and or id = connective_or or id = connective_not
-
-(* [conj i s] constructs the conjunction of two constr *)
-
-let conj i s = Term.applist (constant "and", [i; s])
-
-(* [n_mkNamedProd v [xn,tn;...;x1,t1]] constructs the type 
-   [(x1:t1)...(xn:tn)v] *)
-
-let rec n_mkNamedProd v = function
-  | [] -> v
-  | (id,ty) :: rem -> n_mkNamedProd (Term.mkNamedProd id ty v) rem
-
-(* [n_lambda v [xn,tn;...;x1,t1]] constructs the type [x1:t1]...[xn:tn]v *)
-
-let rec n_lambda v = function
-  | [] -> v
-  | (id,ty) :: rem -> n_lambda (Term.mkNamedLambda id ty v) rem
-
-(* [abstract env idl c] constructs [x1]...[xn]c where idl = [x1;...;xn] *)
-
-let abstract ids c = n_lambda c (List.rev ids)
-
-(* substitutivity (of kernel names, for modules management) *)
-
-open Ptype
-
-let rec type_v_knsubst s = function
-  | Ref v -> Ref (type_v_knsubst s v)
-  | Array (c, v) -> Array (subst_mps s c, type_v_knsubst s v)
-  | Arrow (bl, c) -> Arrow (List.map (binder_knsubst s) bl, type_c_knsubst s c)
-  | TypePure c -> TypePure (subst_mps s c)
-
-and type_c_knsubst s ((id,v),e,pl,q) =
-  ((id, type_v_knsubst s v), e, 
-   List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl,
-   Option.map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
-
-and binder_knsubst s (id,b) = 
-  (id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b)
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
deleted file mode 100644
index 247880e798..0000000000
--- a/contrib/correctness/pmisc.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Term
-open Ptype
-open Topconstr
-
-(* Some misc. functions *)
-
-val reraise_with_loc : Util.loc -> ('a -> 'b) -> 'a -> 'b
-
-val list_of_some : 'a option -> 'a list
-val difference : 'a list -> 'a list -> 'a list
-
-val at_id : identifier -> string -> identifier
-val un_at : identifier -> identifier * string
-val is_at : identifier -> bool
-
-val result_id : identifier
-val adr_id : identifier -> identifier
-
-val renaming_of_ids : identifier list -> identifier list
-                     -> (identifier * identifier) list * identifier list
-
-val reset_names : unit -> unit
-val pre_name    : name -> identifier
-val post_name   : name -> identifier
-val inv_name    : name -> identifier
-val test_name   : name -> identifier
-val bool_name   : unit -> identifier
-val var_name    : name -> identifier
-val phi_name    : unit -> identifier
-val for_name    : unit -> identifier
-val label_name  : unit -> string
-
-val id_of_name : name -> identifier
-
-(* CIC terms *)
-
-val isevar : constr
-
-val subst_in_constr : (identifier * identifier) list -> constr -> constr
-val subst_in_ast : (identifier * identifier) list -> constr_expr -> constr_expr
-val subst_ast_in_ast :
-  (identifier * constr_expr) list -> constr_expr -> constr_expr
-val real_subst_in_constr : (identifier * constr) list -> constr -> constr
-
-val constant : string -> constr
-val coq_constant : string list -> string -> kernel_name
-val conj : constr -> constr -> constr
-
-val coq_true : constr
-val coq_false : constr
-
-val connective_and : identifier
-val connective_or  : identifier
-val connective_not : identifier
-val is_connective : identifier -> bool
-
-val n_mkNamedProd : constr -> (identifier * constr) list -> constr
-val n_lambda  : constr -> (identifier * constr) list -> constr
-val abstract : (identifier * constr) list -> constr -> constr
-
-val type_v_knsubst : substitution -> type_v -> type_v
-val type_c_knsubst : substitution -> type_c -> type_c
-
-(* for debugging purposes *)
-
-val deb_mess : Pp.std_ppcmds -> unit
-val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit
-
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
deleted file mode 100644
index 8df9f20ced..0000000000
--- a/contrib/correctness/pmlize.ml
+++ /dev/null
@@ -1,320 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Term
-open Termast
-open Pattern
-open Matching
-
-open Pmisc
-open Ptype
-open Past
-open Putil
-open Prename
-open Penv
-open Peffect
-open Ptyping
-open Pmonad
-
-
-let has_proof_part ren env c =
-  let sign = Pcicenv.trad_sign_of ren env in
-  let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in
-  Hipattern.is_matching_sigma (Reductionops.nf_betaiota ty)
-
-(* main part: translation of imperative programs into functional ones.
- * 
- * [env] is the environment
- * [ren] is the current renamings of variables
- * [t] is the imperative program to translate, annotated with type+effects
- *
- * we return the translated program in type cc_term
- *)
-
-let rec trad ren t =
-  let env = t.info.env in
-  trad_desc ren env t.info.kappa t.desc
-
-and trad_desc ren env ct d =
-  let (_,tt),eft,pt,qt = ct in
-  match d with
-
-  | Expression c ->
-      let ids = get_reads eft in
-      let al = current_vars ren ids in
-      let c' = subst_in_constr al c in
-      if has_proof_part ren env c' then
-	CC_expr c'
-      else
-      	let ty = trad_ml_type_v ren env tt in
-      	make_tuple [ CC_expr c',ty ] qt ren env (current_date ren)
-      
-  | Variable id ->
-      if is_mutable_in_env env id then
-	invalid_arg "Mlise.trad_desc"
-      else if is_local env id then
-	CC_var id
-      else
-	CC_expr (constant (string_of_id id))
-
-  | Acc _ ->
-      failwith "Mlise.trad: pure terms are supposed to be expressions"
-
-  | TabAcc (check, x, e1) ->
-      let _,ty_elem,_ = array_info ren env x in
-      let te1 = trad ren e1 in
-      let (_,ef1,p1,q1) = e1.info.kappa in
-      let w = get_writes ef1 in
-      let ren' = next ren w in
-      let id = id_of_string "index" in
-      let access = 
-	make_raw_access ren' env (x,current_var ren' x) (mkVar id) 
-      in
-      let t,ty = result_tuple ren' (current_date ren) env
-		   (CC_expr access, ty_elem) (eft,qt) in
-      let t =
-	if check then 
-	  let h = make_pre_access ren env x (mkVar id) in 
-	  let_in_pre ty (anonymous_pre true h) t
-	else
-	  t 
-      in
-      make_let_in ren env te1 p1
-	(current_vars ren' w,q1) (id,constant "Z") (t,ty)
-
-  | Aff (x, e1) ->
-      let tx = trad_type_in_env ren env x in
-      let te1 = trad ren e1 in
-      let (_,ef1,p1,q1) = e1.info.kappa in
-      let w1 = get_writes ef1 in
-      let ren' = next ren (x::w1) in
-      let t_ty = result_tuple ren' (current_date ren) env
-		   (CC_expr (constant "tt"), constant "unit") (eft,qt) 
-      in
-      make_let_in ren env te1 p1
-	(current_vars ren' w1,q1) (current_var ren' x,tx) t_ty
-
-  | TabAff (check, x, e1, e2) ->
-      let _,ty_elem,ty_array = array_info ren env x in
-      let te1 = trad ren e1 in
-      let (_,ef1,p1,q1) = e1.info.kappa in
-      let w1 = get_writes ef1 in
-      let ren' = next ren w1 in
-      let te2 = trad ren' e2 in
-      let (_,ef2,p2,q2) = e2.info.kappa in
-      let w2 = get_writes ef2 in
-      let ren'' = next ren' w2 in
-      let id1 = id_of_string "index" in
-      let id2 = id_of_string "v" in
-      let ren''' = next ren'' [x] in
-      let t,ty = result_tuple ren''' (current_date ren) env
-		   (CC_expr (constant "tt"), constant "unit") (eft,qt) in
-      let store = make_raw_store ren'' env (x,current_var ren'' x) (mkVar id1)
-		   (mkVar id2) in
-      let t = make_let_in ren'' env (CC_expr store) [] ([],None) 
-		(current_var ren''' x,ty_array) (t,ty) in
-      let t = make_let_in ren' env te2 p2
-     	(current_vars ren'' w2,q2) (id2,ty_elem) (t,ty) in
-      let t = 
-	if check then
-	  let h = make_pre_access ren' env x (mkVar id1) in
-	  let_in_pre ty (anonymous_pre true h) t
-	else
-	  t 
-      in
-      make_let_in ren env te1 p1
-	(current_vars ren' w1,q1) (id1,constant "Z") (t,ty)
-
-  | Seq bl ->
-      let before = current_date ren in
-      let finish ren = function
-	  Some (id,ty) -> 
-	    result_tuple ren before env (CC_var id, ty) (eft,qt)
-	| None ->
-	    failwith "a block should contain at least one statement"
-      in
-      let bl = trad_block ren env bl in
-      make_block ren env finish bl
-
-  | If (b, e1, e2) ->
-      let tb = trad ren b in
-      let _,efb,_,_ = b.info.kappa in
-      let ren' = next ren (get_writes efb) in
-      let te1 = trad ren' e1 in
-      let te2 = trad ren' e2 in
-      make_if ren env (tb,b.info.kappa) ren' (te1,e1.info.kappa) 
-	(te2,e2.info.kappa) ct
-
-  (* Translation of the while. *)
-
-  | While (b, inv, var, bl) ->
-      let ren' = next ren (get_writes eft) in
-      let tb = trad ren' b in
-      let tbl = trad_block ren' env bl in
-      let var' = typed_var ren env var in
-      make_while ren env var' (tb,b.info.kappa) tbl (inv,ct)
-
-  | Lam (bl, e) ->
-      let bl' = trad_binders ren env bl in
-      let env' = traverse_binders env bl in
-      let ren' = initial_renaming env' in
-      let te = trans ren' e in
-      CC_lam (bl', te)
-
-  | SApp ([Variable id; Expression q1; Expression q2], [e1; e2])
-      when id = connective_and or id = connective_or ->
-      let c = constant (string_of_id id) in
-      let te1 = trad ren e1
-      and te2 = trad ren e2 in
-      let q1' = apply_post ren env (current_date ren) (anonymous q1)
-      and q2' = apply_post ren env (current_date ren) (anonymous q2) in
-      CC_app (CC_expr c, [CC_expr q1'.a_value; CC_expr q2'.a_value; te1; te2])
-
-  | SApp ([Variable id; Expression q], [e]) when id = connective_not ->
-      let c = constant (string_of_id id) in
-      let te = trad ren e in
-      let q' = apply_post ren env (current_date ren) (anonymous q) in
-      CC_app (CC_expr c, [CC_expr q'.a_value; te])
-
-  | SApp _ ->
-      invalid_arg "mlise.trad (SApp)"
-
-  | Apply (f, args) ->
-      let trad_arg (ren,args) = function
-	| Term a ->
-	    let ((_,tya),efa,_,_) as ca = a.info.kappa in
-	    let ta = trad ren a in
-	    let w = get_writes efa in
-	    let ren' = next ren w in
-	    ren', ta::args
-	| Refarg _ ->
-	    ren, args
-	| Type v -> 
-	    let c = trad_ml_type_v ren env v in
-	    ren, (CC_expr c)::args
-      in
-      let ren',targs = List.fold_left trad_arg (ren,[]) args in
-      let tf = trad ren' f in
-      let cf = f.info.kappa in
-      let c,(s,_,_),capp = effect_app ren env f args in
-      let tc_args =
-	List.combine
-	  (List.rev targs)
-	  (Util.map_succeed
-	     (function
-		| Term x -> x.info.kappa
-		| Refarg _ -> failwith "caught"
-		| Type _ -> 
-		    (result_id,TypePure mkSet),Peffect.bottom,[],None)
-	     args)
-      in
-      make_app env ren tc_args ren' (tf,cf) (c,s,capp) ct
-	
-  | LetRef (x, e1, e2) ->
-      let (_,v1),ef1,p1,q1 = e1.info.kappa in
-      let te1 = trad ren e1 in
-      let tv1 = trad_ml_type_v ren env v1 in
-      let env' = add (x,Ref v1) env in
-      let ren' = next ren [x] in
-      let (_,v2),ef2,p2,q2 = e2.info.kappa in
-      let tv2 = trad_ml_type_v ren' env' v2 in
-      let te2 = trad ren' e2 in
-      let ren'' = next ren' (get_writes ef2) in
-      let t,ty = result_tuple ren'' (current_date ren) env
-		   (CC_var result_id, tv2) (eft,qt) in
-      let t = make_let_in ren' env' te2 p2
-		(current_vars ren'' (get_writes ef2),q2)
-		(result_id,tv2) (t,ty) in
-      let t = make_let_in ren env te1 p1
-     		(current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty) 
-      in
-      t
-
-  | Let (x, e1, e2) ->
-      let (_,v1),ef1,p1,q1 = e1.info.kappa in
-      let te1 = trad ren e1 in
-      let tv1 = trad_ml_type_v ren env v1 in
-      let env' = add (x,v1) env in
-      let ren' = next ren (get_writes ef1) in
-      let (_,v2),ef2,p2,q2 = e2.info.kappa in
-      let tv2 = trad_ml_type_v ren' env' v2 in
-      let te2 = trad ren' e2 in
-      let ren'' = next ren' (get_writes ef2) in
-      let t,ty = result_tuple ren'' (current_date ren) env
-		   (CC_var result_id, tv2) (eft,qt) in
-      let t = make_let_in ren' env' te2 p2
-		(current_vars ren'' (get_writes ef2),q2)
-		(result_id,tv2) (t,ty) in
-      let t = make_let_in ren env te1 p1
-     		(current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty) 
-      in
-      t
-
-  | LetRec (f,bl,v,var,e) ->
-      let (_,ef,_,_) as c = 
-	match tt with Arrow(_,c) -> c | _ -> assert false in
-      let bl' = trad_binders ren env bl in
-      let env' = traverse_binders env bl in
-      let ren' = initial_renaming env' in
-      let (phi0,var') = find_recursion f e.info.env in
-      let te = trad ren' e in
-      let t = make_letrec ren' env' (phi0,var') f bl' (te,e.info.kappa) c in
-      CC_lam (bl', t)
-
-  | PPoint (s,d) ->       
-      let ren' = push_date ren s in
-      trad_desc ren' env ct d
-
-  | Debug _ -> failwith "Mlise.trad: Debug: not implemented"
-
-
-and trad_binders ren env = function
-  | [] -> 
-      []
-  | (_,BindType (Ref _ | Array _))::bl ->
-      trad_binders ren env bl
-  | (id,BindType v)::bl ->
-      let tt = trad_ml_type_v ren env v in
-      (id, CC_typed_binder tt) :: (trad_binders ren env bl)
-  | (id,BindSet)::bl ->
-      (id, CC_typed_binder mkSet) :: (trad_binders ren env bl)
-  | (_,Untyped)::_ -> invalid_arg "trad_binders"
-
-	
-and trad_block ren env = function
-  | [] -> 
-      []
-  | (Assert c)::block ->
-      (Assert c)::(trad_block ren env block)
-  | (Label s)::block ->
-      let ren' = push_date ren s in
-      (Label s)::(trad_block ren' env block)
-  | (Statement e)::block ->
-      let te = trad ren e in
-      let _,efe,_,_ = e.info.kappa in
-      let w = get_writes efe in
-      let ren' = next ren w in
-      (Statement (te,e.info.kappa))::(trad_block ren' env block)
-
-
-and trans ren e =
-  let env = e.info.env in
-  let _,ef,p,_ = e.info.kappa in
-  let ty = trad_ml_type_c ren env e.info.kappa in
-  let ids = get_reads ef in
-  let al = current_vars ren ids in
-  let c = trad ren e in
-  let c = abs_pre ren env (c,ty) p in
-  let bl = binding_of_alist ren env al in
-  make_abs (List.rev bl) c
-
diff --git a/contrib/correctness/pmlize.mli b/contrib/correctness/pmlize.mli
deleted file mode 100644
index 01885418b0..0000000000
--- a/contrib/correctness/pmlize.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Past
-open Penv
-open Names
-
-(* translation of imperative programs into intermediate functional programs *)
-
-val trans : Prename.t -> typed_program -> cc_term
-
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
deleted file mode 100644
index a341ba2ba3..0000000000
--- a/contrib/correctness/pmonad.ml
+++ /dev/null
@@ -1,665 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Util
-open Names
-open Term
-open Termast
-
-open Pmisc
-open Putil
-open Ptype
-open Past
-open Prename
-open Penv
-open Pcic
-open Peffect
-
-
-(* [product ren [y1,z1;...;yk,zk] q] constructs
- * the (possibly dependent) tuple type
- *
- *      z1 x ... x zk                             if no post-condition
- * or   \exists. y1:z1. ... yk:zk. (Q x1 ... xn)  otherwise
- *
- * where the xi are given by the renaming [ren].
- *)
-
-let product_name = function
-  | 2 -> "prod"
-  | n -> check_product_n n; Printf.sprintf "tuple_%d" n
-
-let dep_product_name = function
-  | 1 -> "sig"
-  | n -> check_dep_product_n n; Printf.sprintf "sig_%d" n
-
-let product ren env before lo = function
-  | None -> (* non dependent case *)
-      begin match lo with
-	| [_,v] -> v
-	| _ ->
-	    let s = product_name (List.length lo) in
-      	    Term.applist (constant s, List.map snd lo)
-      end
-  | Some q -> (* dependent case *)
-      let s = dep_product_name (List.length lo) in
-      let a' = apply_post ren env before q in
-      Term.applist (constant s, (List.map snd lo) @ [a'.a_value])
-	
-(* [arrow ren v pl] abstracts the term v over the pre-condition if any
- * i.e. computes
- *
- *     (P1 x1 ... xn) -> ... -> (Pk x1 ... xn) -> v
- * 
- * where the xi are given by the renaming [ren].
- *)
-
-let arrow ren env v pl =
-  List.fold_left 
-    (fun t p -> 
-       if p.p_assert then t else Term.mkArrow (apply_pre ren env p).p_value t) 
-    v pl
-	
-(* [abstract_post ren env (e,q) (res,v)] abstract a post-condition q
- * over the write-variables of e *)
-
-let rec abstract_post ren env (e,q) =
-  let after_id id = id_of_string ((string_of_id id) ^ "'") in
-  let (_,go) = Peffect.get_repr e in
-  let al = List.map (fun id -> (id,after_id id)) go in
-  let q = Option.map (named_app (subst_in_constr al)) q in
-  let tgo = List.map (fun (id,aid) -> (aid, trad_type_in_env ren env id)) al in
-  Option.map (named_app (abstract tgo)) q
-
-(* Translation of effects types in cic types.
- *
- * [trad_ml_type_v] and [trad_ml_type_c] translate types with effects
- * into cic types.
- *)
-
-and prod ren env g = 
-  List.map
-    (fun id -> (current_var ren id, trad_type_in_env ren env id)) 
-    g
-
-and input ren env e  =
-  let i,_ = Peffect.get_repr e in
-  prod ren env i
-
-and output ren env ((id,v),e) =
-  let tv = trad_ml_type_v ren env v in
-  let _,o = Peffect.get_repr e in
-  (prod ren env o) @ [id,tv]
-
-and input_output ren env c =
-  let ((res,v),e,_,_) = c in
-  input ren env e, output ren env ((res,v),e)
-
-(* The function t -> \barre{t} on V and C. *)
-
-and trad_ml_type_c ren env c =
-  let ((res,v),e,p,q) = c in
-  let q = abstract_post ren env (e,q) in
-  let lo = output ren env ((res,v),e) in
-  let ty = product ren env (current_date ren) lo q in
-  let ty = arrow ren env ty p in
-  let li = input ren env e in
-  n_mkNamedProd ty li
-
-and trad_ml_type_v ren env = function
-    
-  | Ref _ | Array _ -> invalid_arg "Monad.trad_ml_type_v"
-	
-  | Arrow (bl, c) ->
-      let bl',ren',env' =
-	List.fold_left
-	  (fun (bl,ren,env) b -> match b with
-	     | (id,BindType ((Ref _ | Array _) as v)) ->
-		 let env' = add (id,v) env in
-		 let ren' = initial_renaming env' in
-		 (bl,ren',env')
-	     | (id,BindType v) -> 
-		 let tt = trad_ml_type_v ren env v in
-		 let env' = add (id,v) env in
-		 let ren' = initial_renaming env' in
-		 (id,tt)::bl,ren',env'
-	     | (id, BindSet) ->
-		 (id,mkSet) :: bl,ren,env
-	     | _ -> failwith "Monad: trad_ml_type_v: not yet implemented"
- 	  )
- 	  ([],ren,env) bl 
-      in
-      n_mkNamedProd (trad_ml_type_c ren' env' c) bl'
-	
-  | TypePure c ->
-      (apply_pre ren env (anonymous_pre false c)).p_value
-
-and trad_imp_type ren env = function
-  | Ref v        -> trad_ml_type_v ren env v
-  | Array (c,v)  -> Term.applist (constant "array", 
-				  [c; trad_ml_type_v ren env v])
-  | _            -> invalid_arg "Monad.trad_imp_type"
-
-and trad_type_in_env ren env id =
-  let v = type_in_env env id in trad_imp_type ren env v
-
-
-
-(* bindings *)
-
-let binding_of_alist ren env al =
-  List.map
-    (fun (id,id') -> (id', CC_typed_binder (trad_type_in_env ren env id)))
-    al
-
-
-(* [make_abs bl t p] abstracts t w.r.t binding list bl., that is
- * [x1:t1]...[xn:tn]t. Returns t if the binding is empty. *)
-
-let make_abs bl t = match bl with
-  | [] -> t
-  | _  -> CC_lam (bl, t)
-
-
-(* [result_tuple ren before env (res,v) (ef,q)] constructs the tuple 
- *
- *    (y1,...,yn,res,?::(q/ren y1 ... yn res))
- *
- * where the yi are the values of the output of ef.
- * if there is no yi and no post-condition, it is simplified in res itself.
- *)
-
-let simple_constr_of_prog = function
-  | CC_expr c -> c
-  | CC_var id -> mkVar id
-  | _ -> assert false
-
-let make_tuple l q ren env before = match l with
-  | [e,_] when q = None -> 
-      e
-  | _ ->
-      let tl = List.map snd l in
-      let dep,h,th = match q with
-	| None -> false,[],[]
-	| Some c ->
-	    let args = List.map (fun (e,_) -> simple_constr_of_prog e) l in
-	    let c = apply_post ren env before c in
-	    true,
-	    [ CC_hole (Term.applist (c.a_value, args)) ], (* hole *)
-	    [ c.a_value ]                     (* type of the hole *)
-      in 
-      CC_tuple (dep, tl @ th, (List.map fst l) @ h)
-
-let result_tuple ren before env (res,v) (ef,q) =
-  let ids = get_writes ef in
-  let lo = 
-    (List.map (fun id -> 
-		 let id' = current_var ren id in
-		 CC_var id', trad_type_in_env ren env id) ids)
-    @ [res,v]
-  in
-  let q = abstract_post ren env (ef,q) in
-  make_tuple lo q ren env before,
-  product ren env before lo q
-
-
-(* [make_let_in ren env fe p (vo,q) (res,v) t] constructs the term
-   
-        [ let h1 = ?:P1 in ... let hn = ?:Pm in ]
-          let y1,y2,...,yn, res [,q] = fe in
-          t
-
-   vo=[_,y1;...;_,ym] are list of renamings.
-   v is the type of res
-   *)
-
-let let_in_pre ty p t =
-  let h = p.p_value in
-  CC_letin (false, ty, [pre_name p.p_name,CC_typed_binder h], CC_hole h, t)
-
-let multiple_let_in_pre ty hl t =
-  List.fold_left (fun t h -> let_in_pre ty h t) t hl
-
-let make_let_in ren env fe p (vo,q) (res,tyres) (t,ty) =
-  let b = [res, CC_typed_binder tyres] in
-  let b',dep = match q with
-    | None -> [],false
-    | Some q -> [post_name q.a_name, CC_untyped_binder],true 
-  in
-  let bl = (binding_of_alist ren env vo) @ b @ b' in
-  let tyapp =
-    let n = succ (List.length vo) in
-    let name = match q with None -> product_name n | _ -> dep_product_name n in
-    constant name 
-  in
-  let t = CC_letin (dep, ty, bl, fe, t) in
-  multiple_let_in_pre ty (List.map (apply_pre ren env) p) t
-
-
-(* [abs_pre ren env (t,ty) pl] abstracts a term t with respect to the 
- * list of pre-conditions [pl]. Some of them are real pre-conditions
- * and others are assertions, according to the boolean field p_assert,
- * so we construct the term
- *   [h1:P1]...[hn:Pn]let h'1 = ?:P'1 in ... let H'm = ?:P'm in t
- *)
-
-let abs_pre ren env (t,ty) pl =
-  List.fold_left
-    (fun t p ->
-       if p.p_assert then
-	 let_in_pre ty (apply_pre ren env p) t
-       else
-	 let h = pre_name p.p_name in 
-	 CC_lam ([h,CC_typed_binder (apply_pre ren env p).p_value],t))
-    t pl
-    
-
-(* [make_block ren env finish bl] builds the translation of a block
- * finish is the function that is applied to the result at the end of the
- * block. *)
-
-let make_block ren env finish bl =
-  let rec rec_block ren result = function
-    | [] ->
-	finish ren result
-    | (Assert c) :: block ->
-	let t,ty = rec_block ren result block in
-	let c = apply_assert ren env c in
-	let p = { p_assert = true; p_name = c.a_name; p_value = c.a_value } in
-	let_in_pre ty p t, ty
-    | (Label s) :: block ->
-	let ren' = push_date ren s in
-	rec_block ren' result block
-    | (Statement (te,info)) :: block ->
-	let (_,tye),efe,pe,qe = info in
-	let w = get_writes efe in
-	let ren' = next ren w in
-	let id = result_id in
-	let tye = trad_ml_type_v ren env tye in
-	let t = rec_block ren' (Some (id,tye)) block in
-	make_let_in ren env te pe (current_vars ren' w,qe) (id,tye) t,
-	snd t
-  in
-  let t,_ = rec_block ren None bl in
-  t
-
-
-(* [make_app env ren args ren' (tf,cf) (cb,s,capp) c]
- * constructs the application of [tf] to [args].
- * capp is the effect of application, after substitution (s) and cb before
- *)
-
-let eq ty e1 e2 =
-  Term.applist (constant "eq", [ty; e1; e2])
-
-let lt r e1 e2 =
-  Term.applist (r, [e1; e2])
-
-let is_recursive env = function
-  | CC_var x -> 
-      (try let _ = find_recursion x env in true with Not_found -> false)
-  | _ -> false
-
-let if_recursion env f = function
-  | CC_var x ->
-      (try let v = find_recursion x env in (f v x) with Not_found -> [])
-  | _ -> []
-
-let dec_phi ren env s svi =
-  if_recursion env
-    (fun (phi0,(cphi,r,_)) f -> 
-       let phi = subst_in_constr svi (subst_in_constr s cphi) in
-       let phi = (apply_pre ren env (anonymous_pre true phi)).p_value in
-       [CC_expr phi; CC_hole (lt r phi (mkVar phi0))])
-
-let eq_phi ren env s svi =
-  if_recursion env
-    (fun (phi0,(cphi,_,a)) f ->
-       let phi = subst_in_constr svi (subst_in_constr s cphi) in
-       let phi = (apply_pre ren env (anonymous_pre true phi)).p_value in
-       [CC_hole (eq a phi phi)])
-
-let is_ref_binder = function 
-  | (_,BindType (Ref _ | Array _)) -> true
-  | _ -> false
-
-let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
-  let ((_,tvf),ef,pf,qf) = cf in
-  let (_,eapp,papp,qapp) = capp in
-  let ((_,v),e,p,q) = c in
-  let bl = List.filter (fun b -> not (is_ref_binder b)) bl in
-  let recur = is_recursive env tf in
-  let before = current_date ren in
-  let ren'' = next ren' (get_writes ef) in
-  let ren''' = next ren'' (get_writes eapp) in
-  let res = result_id in
-  let vi,svi =
-    let ids = List.map fst bl in 
-    let s = fresh (avoid ren ids) ids in
-    List.map snd s, s
-  in
-  let tyres = subst_in_constr svi (trad_ml_type_v ren env v) in
-  let t,ty = result_tuple ren''' before env (CC_var res, tyres) (e,q) in
-  let res_f = id_of_string "vf" in
-  let inf,outf =
-    let i,o = let _,e,_,_ = cb in get_reads e, get_writes e in
-    let apply_s = List.map (fun id -> try List.assoc id s with _ -> id) in
-    apply_s i, apply_s o
-  in
-  let fe =
-    let xi = List.rev (List.map snd (current_vars ren'' inf)) in
-    let holes = List.map (fun x -> (apply_pre ren'' env x).p_value)
-		  (List.map (pre_app (subst_in_constr svi)) papp) in
-    CC_app ((if recur then tf else CC_var res_f),
-	    (dec_phi ren'' env s svi tf) 
-	    @(List.map (fun id -> CC_var id) (vi @ xi))
-	    @(eq_phi ren'' env s svi tf)
-	    @(List.map (fun c -> CC_hole c) holes))
-  in
-  let qapp' = Option.map (named_app (subst_in_constr svi)) qapp in
-  let t = 
-    make_let_in ren'' env fe [] (current_vars ren''' outf,qapp')
-      (res,tyres) (t,ty)
-  in
-  let t =
-    if recur then 
-      t
-    else
-      make_let_in ren' env tf pf
-	(current_vars ren'' (get_writes ef),qf)
-	(res_f,trad_ml_type_v ren env tvf) (t,ty)
-  in
-  let rec eval_args ren = function
-    | [] -> t
-    | (vx,(ta,((_,tva),ea,pa,qa)))::args ->
-	let w = get_writes ea in
-	let ren' = next ren w in
-	let t' = eval_args ren' args in
-	make_let_in ren env ta pa (current_vars ren' (get_writes ea),qa)
-	  (vx,trad_ml_type_v ren env tva) (t',ty)
-  in
-  eval_args ren (List.combine vi args)
-
-
-(* [make_if ren env (tb,cb) ren' (t1,c1) (t2,c2)]
- * constructs the term corresponding to a if expression, i.e
- *
- *       [p] let o1, b [,q1] = m1 [?::p1] in
- *           Cases b of
- *              R => let o2, v2 [,q2] = t1  [?::p2] in 
- *                   (proj (o1,o2)), v2 [,?::q] 
- *            | S => let o2, v2 [,q2] = t2  [?::p2] in 
- *                   (proj (o1,o2)), v2 [,?::q] 
- *)
-
-let make_if_case ren env ty (b,qb) (br1,br2) =
-  let id_b,ty',ty1,ty2 = match qb with
-    | Some q ->  
-  	let q = apply_post ren env (current_date ren) q in
-    	let (name,t1,t2) = Term.destLambda q.a_value in
-	q.a_name,
-    	Term.mkLambda (name, t1, mkArrow t2 ty),
-	Term.mkApp (q.a_value, [| coq_true |]),
-	Term.mkApp (q.a_value, [| coq_false |])
-    | None -> assert false
-  in
-  let n = test_name Anonymous in
-  CC_app (CC_case (ty', b, [CC_lam ([n,CC_typed_binder ty1], br1);
-			    CC_lam ([n,CC_typed_binder ty2], br2)]),
-	  [CC_var (post_name id_b)])
-
-let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c =
-  let ((_,tvb),eb,pb,qb) = cb in
-  let ((_,tv1),e1,p1,q1) = c1 in
-  let ((_,tv2),e2,p2,q2) = c2 in
-  let ((_,t),e,p,q) = c in
-
-  let wb = get_writes eb in
-  let resb = id_of_string "resultb" in
-  let res = result_id in
-  let tyb = trad_ml_type_v ren' env tvb in
-  let tt = trad_ml_type_v ren env t in
-
-  (* une branche de if *)
-  let branch (tv_br,e_br,p_br,q_br) f_br  = 
-    let w_br = get_writes e_br in
-    let ren'' = next ren' w_br in
-    let t,ty = result_tuple ren'' (current_date ren') env
-		 (CC_var res,tt) (e,q) in
-    make_let_in ren' env f_br p_br (current_vars ren'' w_br,q_br)
-      (res,tt) (t,ty),
-    ty
-  in
-  let t1,ty1 = branch c1 t1 in
-  let t2,ty2 = branch c2 t2 in
-  let ty = ty1 in
-  let qb = force_bool_name qb in
-  let t = make_if_case ren env ty (CC_var resb,qb) (t1,t2) in
-  make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty)
-
-
-(* [make_while ren env (cphi,r,a) (tb,cb) (te,ce) c]
- * constructs the term corresponding to the while, i.e.
- * 
- *    [h:(I x)](well_founded_induction
- *              A R ?::(well_founded A R)
- *              [Phi:A] (x) Phi=phi(x)->(I x)-> \exists x'.res.(I x')/\(S x')
- *              [Phi_0:A][w:(Phi:A)(Phi<Phi_0)-> ...]
- *                [x][eq:Phi_0=phi(x)][h:(I x)]
- *                   Cases (b x) of
- *                     (left  HH) => (x,?::(IS x))
- *                   | (right HH) => let x1,_,_ = (e x ?) in
- *                                   (w phi(x1) ? x1 ? ?)
- *              phi(x) x ? ?)
- *)
-
-let id_phi = id_of_string "phi"
-let id_phi0 = id_of_string "phi0"
-
-let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) =
-  let ((_,tvb),eb,pb,qb) = cb in
-  let (_,ef,_,is) = c in
-
-  let ren' = next ren (get_writes ef) in
-  let before = current_date ren in
-  
-  let ty = 
-    let is = abstract_post ren' env (ef,is) in
-    let _,lo = input_output ren env c in
-    product ren env before lo is 
-  in
-  let resb = id_of_string "resultb" in
-  let tyb = trad_ml_type_v ren' env tvb in
-  let wb = get_writes eb in
-
-  (* première branche: le test est vrai => e;w *)
-  let t1 = 
-    make_block ren' env 
-      (fun ren'' result -> match result with
-	 | Some (id,_) ->
-	     let v = List.rev (current_vars ren'' (get_writes ef)) in
-	       CC_app (CC_var id_w,
-		       [CC_expr (phi_of ren'');
-			CC_hole (lt r (phi_of ren'') (mkVar id_phi0))]
-		       @(List.map (fun (_,id) -> CC_var id) v)
-		       @(CC_hole (eq a (phi_of ren'') (phi_of ren'')))
-		       ::(match i with
-			    | None -> [] 
-			    | Some c -> 
-				[CC_hole (apply_assert ren'' env c).a_value])),
-	       ty
-      	 | None -> failwith "a block should contain at least one statement")
-      tbl
-  in
-        
-  (* deuxième branche: le test est faux => on sort de la boucle *)
-  let t2,_ = 
-    result_tuple ren' before env
-      (CC_expr (constant "tt"),constant "unit") (ef,is)
-  in
-
-  let b_al = current_vars ren' (get_reads eb) in
-  let qb = force_bool_name qb in
-  let t = make_if_case ren' env ty (CC_var resb,qb) (t1,t2) in
-  let t = 
-    make_let_in ren' env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) 
-  in
-  let t = 
-    let pl = List.map (pre_of_assert false) (list_of_some i) in
-    abs_pre ren' env (t,ty) pl 
-  in
-  let t = 
-    CC_lam ([var_name Anonymous,
-	     CC_typed_binder (eq a (mkVar id_phi0) (phi_of ren'))],t) 
-  in
-  let bl = binding_of_alist ren env (current_vars ren' (get_writes ef)) in
-  make_abs (List.rev bl) t
-
-
-let make_while ren env (cphi,r,a) (tb,cb) tbl (i,c) =
-  let (_,ef,_,is) = c in
-  let phi_of ren = (apply_pre ren env (anonymous_pre true cphi)).p_value in
-  let wf_a_r = Term.applist (constant "well_founded", [a; r]) in
-
-  let before = current_date ren in
-  let ren' = next ren (get_writes ef) in
-  let al = current_vars ren' (get_writes ef) in
-  let v =   
-    let _,lo = input_output ren env c in
-    let is = abstract_post ren' env (ef,is) in
-    match i with
-      | None -> product ren' env before lo is
-      | Some ci -> 
-	  Term.mkArrow (apply_assert ren' env ci).a_value 
-	    (product ren' env before lo is) 
-  in
-  let v = Term.mkArrow (eq a (mkVar id_phi) (phi_of ren')) v in
-  let v = 
-    n_mkNamedProd v 
-      (List.map (fun (id,id') -> (id',trad_type_in_env ren env id)) al) 
-  in
-  let tw = 
-    Term.mkNamedProd id_phi a
-      (Term.mkArrow (lt r (mkVar id_phi) (mkVar id_phi0)) v) 
-  in
-  let id_w = id_of_string "loop" in
-  let vars = List.rev (current_vars ren (get_writes ef)) in
-  let body =
-    make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) 
-  in
-  CC_app (CC_expr (constant "well_founded_induction"),
-	  [CC_expr a; CC_expr r;
-	   CC_hole wf_a_r;
-	   CC_expr (Term.mkNamedLambda id_phi a v);
-	   CC_lam ([id_phi0, CC_typed_binder a;
-		    id_w, CC_typed_binder tw],
-		   body);
-	   CC_expr (phi_of ren)]
-	  @(List.map (fun (_,id) -> CC_var id) vars)
-          @(CC_hole (eq a (phi_of ren) (phi_of ren)))
-	  ::(match i with
-	       | None -> [] 
-	       | Some c -> [CC_hole (apply_assert ren env c).a_value])) 
-
-
-(* [make_letrec ren env (phi0,(cphi,r,a)) bl (te,ce) c]
- * constructs the term corresponding to the let rec i.e.
- *
- * [x][h:P(x)](well_founded_induction 
- *              A R ?::(well_founded A R)
- *              [Phi:A] (bl) (x) Phi=phi(x)->(P x)-> \exists x'.res.(Q x x')
- *              [Phi_0:A][w:(Phi:A)(Phi<Phi_0)-> ...]
- *                [bl][x][eq:Phi_0=phi(x)][h:(P x)]te
- *              phi(x) bl x ? ?)
- *)
-
-let make_letrec ren env (id_phi0,(cphi,r,a)) idf bl (te,ce) c =
-  let (_,ef,p,q) = c in
-  let phi_of ren = (apply_pre ren env (anonymous_pre true cphi)).p_value in
-  let wf_a_r = Term.applist (constant "well_founded", [a; r]) in
-
-  let before = current_date ren in
-  let al = current_vars ren (get_reads ef) in
-  let v = 
-    let _,lo = input_output ren env c in
-    let q = abstract_post ren env (ef,q) in
-    arrow ren env (product ren env (current_date ren) lo q) p 
-  in
-  let v = Term.mkArrow (eq a (mkVar id_phi) (phi_of ren)) v in
-  let v = 
-    n_mkNamedProd v 
-      (List.map (fun (id,id') -> (id',trad_type_in_env ren env id)) al) 
-  in
-  let v = 
-    n_mkNamedProd v
-      (List.map (function (id,CC_typed_binder c) -> (id,c) 
-		   | _ -> assert false) (List.rev bl)) 
-  in
-  let tw = 
-    Term.mkNamedProd id_phi a
-      (Term.mkArrow (lt r (mkVar id_phi) (mkVar id_phi0)) v) 
-  in
-  let vars = List.rev (current_vars ren (get_reads ef)) in
-  let body =
-    let al = current_vars ren (get_reads ef) in
-    let bod = abs_pre ren env (te,v) p in
-    let bod = CC_lam ([var_name Anonymous,
-		       CC_typed_binder (eq a (mkVar id_phi0) (phi_of ren))],
-		      bod) 
-    in
-    let bl' = binding_of_alist ren env al in
-    make_abs (bl@(List.rev bl')) bod
-  in
-  let t =
-    CC_app (CC_expr (constant "well_founded_induction"),
-	    [CC_expr a; CC_expr r;
-	     CC_hole wf_a_r;
-	     CC_expr (Term.mkNamedLambda id_phi a v);
-	     CC_lam ([id_phi0, CC_typed_binder a;
-		      idf, CC_typed_binder tw],
-		     body);
-	     CC_expr (phi_of ren)]
-	    @(List.map (fun (id,_) -> CC_var id) bl)
-	    @(List.map (fun (_,id) -> CC_var id) vars)
-            @[CC_hole (eq a (phi_of ren) (phi_of ren))]
-	   )
-  in
-  (* on abstrait juste par rapport aux variables de ef *)
-  let al = current_vars ren (get_reads ef) in
-  let bl = binding_of_alist ren env al in
-  make_abs (List.rev bl) t
-
-
-(* [make_access env id c] Access in array id.
- *
- * Constructs [t:(array s T)](access_g s T t c ?::(lt c s)).
- *)
-
-let array_info ren env id =
-  let ty = type_in_env env id in
-  let size,v = dearray_type ty in
-  let ty_elem = trad_ml_type_v ren env v in
-  let ty_array = trad_imp_type ren env ty in
-  size,ty_elem,ty_array
-
-let make_raw_access ren env (id,id') c =
-  let size,ty_elem,_ = array_info ren env id in
-  Term.applist (constant "access", [size; ty_elem; mkVar id'; c])
-
-let make_pre_access ren env id c =
-  let size,_,_ = array_info ren env id in
-  conj (lt (constant "Zle") (constant "ZERO") c)
-       (lt (constant "Zlt") c size)
-      
-let make_raw_store ren env (id,id') c1 c2 =
-  let size,ty_elem,_ = array_info ren env id in
-  Term.applist (constant "store", [size; ty_elem; mkVar id'; c1; c2])
diff --git a/contrib/correctness/pmonad.mli b/contrib/correctness/pmonad.mli
deleted file mode 100644
index 8e7d4b6eb6..0000000000
--- a/contrib/correctness/pmonad.mli
+++ /dev/null
@@ -1,106 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Term
-
-open Ptype
-open Past
-open Penv
-
-(* Main part of the translation of imperative programs into functional ones
- * (with mlise.ml) *)
-
-(* Here we translate the specification into a CIC specification *)
-
-val trad_ml_type_v : Prename.t -> local_env -> type_v -> constr
-val trad_ml_type_c : Prename.t -> local_env -> type_c -> constr
-val trad_imp_type  : Prename.t -> local_env -> type_v -> constr
-val trad_type_in_env : Prename.t -> local_env -> identifier -> constr
-
-val binding_of_alist : Prename.t -> local_env
-                    -> (identifier * identifier) list
-		    -> cc_binder list
-val make_abs : cc_binder list -> cc_term -> cc_term
-val abs_pre : Prename.t -> local_env -> cc_term * constr -> 
-  constr precondition list -> cc_term
-
-(* The following functions translate the main constructions *)
-
-val make_tuple : (cc_term * cc_type) list -> predicate option
-          -> Prename.t -> local_env -> string
-          -> cc_term
-
-val result_tuple : Prename.t -> string -> local_env
-          -> (cc_term * constr) -> (Peffect.t * predicate option)
-          -> cc_term * constr
-
-val let_in_pre : constr -> constr precondition -> cc_term -> cc_term
-
-val make_let_in : Prename.t -> local_env -> cc_term 
-          -> constr precondition list
-          -> ((identifier * identifier) list * predicate option) 
-	  -> identifier * constr
-	  -> cc_term * constr -> cc_term
-
-val make_block : Prename.t -> local_env
-          -> (Prename.t -> (identifier * constr) option -> cc_term * constr)
-	  -> (cc_term * type_c, constr) block
-	  -> cc_term
-
-val make_app : local_env
-          -> Prename.t -> (cc_term * type_c) list
-	  -> Prename.t -> cc_term * type_c
-	  -> ((type_v binder list) * type_c)
-	    * ((identifier*identifier) list)
-	    * type_c
-	  -> type_c
-          -> cc_term
-
-val make_if : Prename.t -> local_env 
-         -> cc_term * type_c
-	 -> Prename.t
-         -> cc_term * type_c
-         -> cc_term * type_c
-         -> type_c
-         -> cc_term
-
-val make_while : Prename.t -> local_env
-         -> (constr * constr * constr) (* typed variant *)
-         -> cc_term * type_c
-         -> (cc_term * type_c, constr) block
-         -> constr assertion option * type_c
-         -> cc_term
-
-val make_letrec : Prename.t -> local_env
-         -> (identifier * (constr * constr * constr)) (* typed variant *)
-	 -> identifier (* the name of the function *)
-         -> (cc_binder list)
-	 -> (cc_term * type_c)
-	 -> type_c
-         -> cc_term
-
-(* Functions to translate array operations *)
-
-val array_info :
-  Prename.t -> local_env -> identifier -> constr * constr * constr
-
-val make_raw_access :
-  Prename.t -> local_env -> identifier * identifier -> constr -> constr
-
-val make_raw_store :
-  Prename.t -> local_env -> identifier * identifier 
-    -> constr -> constr -> constr
-
-val make_pre_access :
-  Prename.t -> local_env -> identifier -> constr -> constr
-
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
deleted file mode 100644
index e378ce814e..0000000000
--- a/contrib/correctness/pred.ml
+++ /dev/null
@@ -1,115 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp
-open Past
-open Pmisc
-
-let rec cc_subst subst = function
-  | CC_var id as c -> 
-      (try CC_expr (List.assoc id subst) with Not_found -> c)
-  | CC_letin (b,ty,bl,c1,c2) ->
-      CC_letin (b, real_subst_in_constr subst ty, cc_subst_binders subst bl,
-		cc_subst subst c1, cc_subst (cc_cross_binders subst bl) c2)
-  | CC_lam (bl, c) ->
-      CC_lam (cc_subst_binders subst bl, 
-	      cc_subst (cc_cross_binders subst bl) c)
-  | CC_app (c, cl) ->
-      CC_app (cc_subst subst c, List.map (cc_subst subst) cl)
-  | CC_tuple (b, tl, cl) ->
-      CC_tuple (b, List.map (real_subst_in_constr subst) tl,
-		List.map (cc_subst subst) cl)
-  | CC_case (ty, c, cl) ->
-      CC_case (real_subst_in_constr subst ty, cc_subst subst c,
-	       List.map (cc_subst subst) cl)
-  | CC_expr c ->
-      CC_expr (real_subst_in_constr subst c)
-  | CC_hole ty ->
-      CC_hole (real_subst_in_constr subst ty)
-
-and cc_subst_binders subst = List.map (cc_subst_binder subst)
-
-and cc_subst_binder subst = function
-  | id,CC_typed_binder c -> id,CC_typed_binder (real_subst_in_constr subst c)
-  | b -> b
-
-and cc_cross_binders subst = function
-  | [] -> subst
-  | (id,_) :: bl -> cc_cross_binders (List.remove_assoc id subst) bl
-
-(* here we only perform eta-reductions on programs to eliminate
- * redexes of the kind
- *
- *   let (x1,...,xn) = e in (x1,...,xn)  -->  e
- *
- *)
-
-let is_eta_redex bl al =
-  try
-    List.for_all2
-      (fun (id,_) t -> match t with CC_var id' -> id=id' | _ -> false)
-      bl al
-  with
-      Invalid_argument("List.for_all2") -> false
-
-let rec red = function
-  | CC_letin (_, _, [id,_], CC_expr c1, e2) ->
-      red (cc_subst [id,c1] e2)
-  | CC_letin (dep, ty, bl, e1, e2) ->
-      begin match red e2 with
-	| CC_tuple (false,tl,al) ->
-	    if is_eta_redex bl al then
-	      red e1
-	    else
-	      CC_letin (dep, ty, bl, red e1,
-			CC_tuple (false,tl,List.map red al))
-	| e -> CC_letin (dep, ty, bl, red e1, e)
-      end
-  | CC_lam (bl, e) ->
-      CC_lam (bl, red e)
-  | CC_app (e, al) ->
-      CC_app (red e, List.map red al)
-  | CC_case (ty, e1, el) ->
-      CC_case (ty, red e1, List.map red el)
-  | CC_tuple (dep, tl, al) ->
-      CC_tuple (dep, tl, List.map red al)
-  | e -> e
-
-
-(* How to reduce uncomplete proof terms when they have become constr *)
-
-open Term
-open Reductionops
-
-(* Il ne faut pas reduire de redexe (beta/iota) qui impliquerait
- * la substitution d'une métavariable.
- * 
- * On commence par rendre toutes les applications binaire (strong bin_app)
- * puis on applique la reduction spéciale programmes définie dans
- * typing/reduction *)
-
-(*i
-let bin_app = function
-  | DOPN(AppL,v) as c ->
-      (match Array.length v with
-	 | 1 -> v.(0)
-	 | 2 -> c
-	 | n ->
-	     let f = DOPN(AppL,Array.sub v 0 (pred n)) in
-	     DOPN(AppL,[|f;v.(pred n)|]))
-  | c -> c
-i*)
-
-let red_cci c = 
-  (*i let c = strong bin_app c in i*) 
-  strong whd_programs (Global.env ()) Evd.empty c
-
diff --git a/contrib/correctness/pred.mli b/contrib/correctness/pred.mli
deleted file mode 100644
index 45d511c507..0000000000
--- a/contrib/correctness/pred.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Term
-open Past
-
-(* reduction on intermediate programs 
- * get rid of redexes of the kind let (x1,...,xn) = e in (x1,...,xn) *)
-
-val red : cc_term -> cc_term
-
-
-(* Ad-hoc reduction on partial proof terms *)
-
-val red_cci : constr -> constr
-
-
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml
deleted file mode 100644
index 6f8e4ae49f..0000000000
--- a/contrib/correctness/prename.ml
+++ /dev/null
@@ -1,139 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Nameops
-open Util
-open Pp
-open Himsg
-open Pmisc
-
-(* Variables names management *)
-
-type date = string
-
-(* The following data structure keeps the successive names of the variables
- * as we traverse the program. A each step a ``date'' and a
- * collection of new names is (possibly) given, and updates the
- * previous renaming.
- * 
- * Then, we can ask for the name of a variable, at current date or
- * at a given date.
- *
- * It is easily represented by a list of date x assoc list, most recent coming 
- * first i.e. as follows:
- *
- *   [ date (= current), [ (x,xi); ... ];
- *     date            , [ (z,zk); ... ];
- *     ...
- *     date (= initial), [ (x,xj); (y,yi); ... ]
- *
- * We also keep a list of all names already introduced, in order to
- * quickly get fresh names.
- *)
-
-type t =
-    { levels : (date * (identifier * identifier) list) list;
-      avoid  : identifier list;
-      cpt    : int }
-    
-
-let empty_ren = { levels = []; avoid = []; cpt = 0 }
-
-let update r d ids =
-  let al,av = renaming_of_ids r.avoid ids in
-  { levels = (d,al) :: r.levels; avoid = av; cpt = r.cpt }
-
-let push_date r d = update r d []
-
-let next r ids =
-  let al,av = renaming_of_ids r.avoid ids in
-  let n = succ r.cpt in
-  let d = string_of_int n in
-  { levels = (d,al) :: r.levels; avoid = av; cpt = n }
-
-
-let find r x =
-  let rec find_in_one = function
-      []         -> raise Not_found
-    | (y,v)::rem -> if y = x then v else find_in_one rem
-  in
-  let rec find_in_all = function
-      []         -> raise Not_found
-    | (_,l)::rem -> try find_in_one l with Not_found -> find_in_all rem
-  in
-    find_in_all r.levels
-
-
-let current_var = find
-
-let current_vars r ids = List.map (fun id -> id,current_var r id) ids
-
-
-let avoid r ids = { levels = r.levels; avoid = r.avoid @ ids; cpt = r.cpt }
-
-let fresh r ids = fst (renaming_of_ids r.avoid ids)
-
-
-let current_date r =
-  match r.levels with
-      [] -> invalid_arg "Renamings.current_date"
-    | (d,_)::_ -> d
-
-let all_dates r = List.map fst r.levels
-
-let rec valid_date da r = 
-  let rec valid = function
-      [] -> false
-    | (d,_)::rem -> (d=da) or (valid rem)
-  in
-    valid r.levels
-
-(* [until d r] selects the part of the renaming [r] starting from date [d] *)
-let rec until da r =
-  let rec cut = function
-      [] -> invalid_arg "Renamings.until"
-    | (d,_)::rem as r -> if d=da then r else cut rem
-  in
-    { avoid = r.avoid; levels = cut r.levels; cpt = r.cpt }
-
-let var_at_date r d id =
-  try
-    find (until d r) id
-  with Not_found ->
-    raise (UserError ("Renamings.var_at_date",
-	      hov 0 (str"Variable " ++ pr_id id ++ str" is unknown" ++ spc () ++
-		       str"at date " ++ str d)))
-
-let vars_at_date r d ids =
-  let r' = until d r in List.map (fun id -> id,find r' id) ids
-
-
-(* pretty-printers *)
-
-open Pp
-open Util
-open Himsg
-
-let pp r = 
-  hov 2 (prlist_with_sep (fun () -> (fnl ()))
-	   (fun (d,l) -> 
-	      (str d ++ str": " ++ 
-		 prlist_with_sep (fun () -> (spc ()))
-		   (fun (id,id') -> 
-		      (str"(" ++ pr_id id ++ str"," ++ pr_id id' ++ str")"))
-		   l))
-	   r.levels)
-
-let ppr e =
-  Pp.pp (pp e)
-
diff --git a/contrib/correctness/prename.mli b/contrib/correctness/prename.mli
deleted file mode 100644
index 6fb563ffcb..0000000000
--- a/contrib/correctness/prename.mli
+++ /dev/null
@@ -1,57 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-
-(* Abstract type for renamings 
- * 
- * Records the names of the mutables objets (ref, arrays) at the different
- * moments of the evaluation, called dates
- *)
-
-type t
-
-type date = string
-
-
-val empty_ren : t
-val update    : t -> date -> identifier list -> t
-    (* assign new names for the given variables, associated to a new date *)
-val next      : t -> identifier list -> t
-    (* assign new names for the given variables, associated to a new
-     * date which is generated from an internal counter *)
-val push_date : t -> date -> t
-    (* put a new date on top of the stack *)
-
-val valid_date   : date -> t -> bool
-val current_date : t -> date
-val all_dates    : t -> date list
-
-val current_var  : t -> identifier      -> identifier
-val current_vars : t -> identifier list -> (identifier * identifier) list
-    (* gives the current names of some variables *)
-
-val avoid : t -> identifier list -> t
-val fresh : t -> identifier list -> (identifier * identifier) list
-    (* introduces new names to avoid and renames some given variables *)
-
-val var_at_date  : t -> date -> identifier -> identifier
-    (* gives the name of a variable at a given date *)
-val vars_at_date : t -> date -> identifier list
-                 -> (identifier * identifier) list
-    (* idem for a list of variables *)  
-
-(* pretty-printers *)
-
-val pp : t -> Pp.std_ppcmds
-val ppr : t -> unit
-
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
deleted file mode 100644
index df1b67fd3f..0000000000
--- a/contrib/correctness/psyntax.ml4
+++ /dev/null
@@ -1,1059 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
-
-open Flags
-open Util
-open Names
-open Nameops
-open Vernacentries
-open Reduction
-open Term
-open Libnames
-open Topconstr
-
-open Prename
-open Pmisc
-open Putil
-open Ptype
-open Past
-open Penv
-open Pmonad
-open Vernacexpr
-
-
-(* We define new entries for programs, with the use of this module
- * Programs. These entries are named Programs.<foo>
- *)
-
-module Gram = Pcoq.Gram
-module Constr = Pcoq.Constr
-module Tactic = Pcoq.Tactic
-
-module Programs =
-  struct
-    let gec s = Gram.Entry.create ("Programs."^s)
-    (* types *)
-    let type_v   = gec "type_v"
-    let type_v0  = gec "type_v0"
-    let type_v1  = gec "type_v1"
-    let type_v2  = gec "type_v2"
-    let type_v3  = gec "type_v3"
-    let type_v_app  = gec "type_v_app"
-    let type_c   = gec "type_c"
-    let effects  = gec "effects"
-    let reads    = gec "reads"
-    let writes   = gec "writes"
-    let pre_condition = gec "pre_condition"
-    let post_condition = gec "post_condition"
-    (* binders *)
-    let binder  = gec "binder"
-    let binder_type = gec "binder_type"
-    let binders  = gec "binders"
-    (* programs *)
-    let program = gec "program"
-    let prog1 = gec "prog1"
-    let prog2 = gec "prog2"
-    let prog3 = gec "prog3"
-    let prog4 = gec "prog4"
-    let prog5 = gec "prog5"
-    let prog6 = gec "prog6"
-    let prog7 = gec "prog7"
-    let ast1 = gec "ast1"
-    let ast2 = gec "ast2"
-    let ast3 = gec "ast3"
-    let ast4 = gec "ast4"
-    let ast5 = gec "ast5"
-    let ast6 = gec "ast6"
-    let ast7 = gec "ast7"
-    let arg = gec "arg"
-    let block = gec "block"
-    let block_statement = gec "block_statement"
-    let relation = gec "relation"
-    let variable = gec "variable"
-    let invariant = gec "invariant"
-    let variant = gec "variant"
-    let assertion = gec "assertion"
-    let precondition = gec "precondition"
-    let postcondition = gec "postcondition"
-    let predicate = gec "predicate"
-    let name = gec "name"
-  end
-
-open Programs
-
-let ast_of_int n = 
-  CDelimiters
-    (dummy_loc, "Z", CNumeral (dummy_loc, Bignat.POS (Bignat.of_string n)))
-
-let constr_of_int n =
-  Constrintern.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
-
-open Util
-open Coqast
-
-let mk_id loc id = mkRefC (Ident (loc, id))
-let mk_ref loc s = mk_id loc (Constrextern.id_of_v7_string s)
-let mk_appl loc1 loc2 f args =
-  CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args)
-
-let conj_assert {a_name=n;a_value=a} {a_value=b} = 
-  let loc1 = constr_loc a in
-  let loc2 = constr_loc a in
-  { a_value = mk_appl loc1 loc2 "and" [a;b]; a_name = n }
-
-let conj = function
-    None,None     -> None
-  | None,b        -> b
-  | a,None        -> a
-  | Some a,Some b -> Some (conj_assert a b)
-
-let without_effect loc d = 
-  { desc = d; pre = []; post = None; loc = loc; info = () }
-
-let isevar = Expression isevar
-
-let bin_op op loc e1 e2 =
-  without_effect loc
-    (Apply (without_effect loc (Expression (constant op)),
-            [ Term e1; Term e2 ]))
-
-let un_op op loc e =
-  without_effect loc
-    (Apply (without_effect loc (Expression (constant op)), [Term e]))
-
-let bool_bin op loc a1 a2 =
-  let w = without_effect loc in
-  let d = SApp ( [Variable op], [a1; a2]) in
-  w d
-
-let bool_or  loc = bool_bin connective_or loc
-let bool_and loc = bool_bin connective_and loc
-
-let bool_not loc a =
-  let w = without_effect loc in
-  let d = SApp ( [Variable connective_not ], [a]) in
-  w d
-
-let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "Z0"]
-
-(* program -> Coq AST *)
-
-let bdize c =
-  let env = 
-    Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty)
-  in
-  Constrextern.extern_constr true env c
-
-let rec coqast_of_program loc = function
-  | Variable id -> mk_id loc id
-  | Acc id -> mk_id loc id
-  | Apply (f,l) -> 
-      let f = coqast_of_program f.loc f.desc in
-      let args = List.map 
-		   (function Term t -> (coqast_of_program t.loc t.desc,None)
-		      | _ -> invalid_arg "coqast_of_program") l
-      in
-      CApp (dummy_loc, (None,f), args)
-  | Expression c -> bdize c
-  | _ -> invalid_arg "coqast_of_program"
-
-(* The construction `for' is syntactic sugar.
- *
- * for i = v1 to v2 do { invariant Inv } block done
- *
- * ==> (let rec f i { variant v2+1-i } = 
- *        { i <= v2+1 /\ Inv(i) }
- *        (if i > v2 then tt else begin block; (f (i+1)) end) 
- *        { Inv(v2+1) }
- *      in (f v1)) { Inv(v2+1) }
- *)
-
-let ast_plus_un loc ast =
-  let un = ast_of_int "1" in
-  mk_appl loc loc "Zplus" [ast;un]
-
-let make_ast_for loc i v1 v2 inv block =
-  let f = for_name() in
-  let id_i = id_of_string i in
-  let var_i = without_effect loc (Variable id_i) in
-  let var_f = without_effect loc (Variable f) in
-  let succ_v2 = 
-    let a_v2 = coqast_of_program v2.loc v2.desc in
-    ast_plus_un loc a_v2 in
-  let post = named_app (subst_ast_in_ast [ id_i, succ_v2 ]) inv in
-  let e1 =
-    let test = bin_op "Z_gt_le_bool" loc var_i v2 in
-    let br_t = without_effect loc (Expression (constant "tt")) in
-    let br_f = 
-      let un = without_effect loc (Expression (constr_of_int "1")) in
-      let succ_i = bin_op "Zplus" loc var_i un in
-      let f_succ_i = without_effect loc (Apply (var_f, [Term succ_i])) in
-      without_effect loc (Seq (block @ [Statement f_succ_i]))
-    in
-    let inv' = 
-      let i_le_sv2 = mk_appl loc loc "Zle" [mk_ref loc i; succ_v2] in
-      conj_assert {a_value=i_le_sv2;a_name=inv.a_name} inv
-    in
-    { desc = If(test,br_t,br_f); loc = loc; 
-      pre = [pre_of_assert false inv']; post = Some post; info = () } 
-  in
-  let bl = 
-    let typez = mk_ref loc "Z" in
-    [(id_of_string i, BindType (TypePure typez))] 
-  in
-  let fv1 = without_effect loc (Apply (var_f, [Term v1])) in
-  let v = TypePure (mk_ref loc "unit") in
-  let var = 
-    let a = mk_appl loc loc "Zminus" [succ_v2;mk_ref loc i] in
-    (a, ast_zwf_zero loc)
-  in
-  Let (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1)
-
-let mk_prog loc p pre post =
-  { desc = p.desc; 
-    pre = p.pre @ pre; 
-    post = conj (p.post,post); 
-    loc = loc; 
-    info = () }
-
-if !Flags.v7 then
-GEXTEND Gram
-
-  (* Types ******************************************************************)
-  type_v:
-    [ [ t = type_v0 -> t ] ]
-  ;
-  type_v0:
-    [ [ t = type_v1 -> t ] ]
-  ;
-  type_v1:
-    [ [ t = type_v2 -> t ] ]
-  ;
-  type_v2:
-    [ LEFTA
-      [ v = type_v2; IDENT "ref" -> Ref v
-      | t = type_v3 -> t ] ]
-  ;
-  type_v3:
-    [ [ IDENT "array"; size = Constr.constr; "of"; v = type_v0 ->
-          Array (size,v)
-      | IDENT "fun"; bl = binders; c = type_c -> make_arrow bl c
-      | c = Constr.constr -> TypePure c	  
-      ] ]
-  ;
-  type_c:
-    [ [ IDENT "returns"; id = IDENT; ":"; v = type_v;
-        e = effects; p = OPT pre_condition; q = OPT post_condition; "end" ->
-        ((id_of_string id, v), e, list_of_some p, q)
-      ] ] 
-  ;
-  effects:
-    [ [ r = OPT reads; w = OPT writes ->
-	let r' = match r with Some l -> l | _ -> [] in
-	let w' = match w with Some l -> l | _ -> [] in
-	List.fold_left (fun e x -> Peffect.add_write x e)
-	  (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r')
-          w'
-      ] ]
-  ;
-  reads:
-    [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ]
-  ;
-  writes:
-    [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ]
-  ;
-  pre_condition:
-    [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ]
-  ;
-  post_condition:
-    [ [ IDENT "post"; c = predicate -> c ] ]
-  ;
-
-  (* Binders (for both types and programs) **********************************)
-  binder:
-    [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" ->
-	  List.map (fun s -> (id_of_string s, t)) sl
-      ] ]
-  ;
-  binder_type:
-    [ [ "Set" -> BindSet
-      | v = type_v -> BindType v
-      ] ]
-  ;
-  binders:
-    [ [ bl = LIST0 binder -> List.flatten bl ] ] 
-  ;
-
-  (* annotations *)
-  predicate:
-    [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ]
-  ;
-  name:
-    [ [ "as"; s = IDENT -> Name (id_of_string s)
-      | -> Anonymous
-      ] ]
-  ;
-
-  (* Programs ***************************************************************)
-  variable:
-    [ [ s = IDENT -> id_of_string s ] ]
-  ;
-  assertion:
-    [ [ "{"; c = predicate; "}" -> c ] ]
-  ;
-  precondition:
-    [ [ "{"; c = predicate; "}" -> pre_of_assert false c ] ]
-  ;
-  postcondition:
-    [ [ "{"; c = predicate; "}" -> c ] ]
-  ;
-  program:
-    [ [ p = prog1 -> p ] ]
-  ;
-  prog1:
-    [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog2:
-    [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog3:
-    [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog4:
-    [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog5:
-    [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog6:
-    [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-
-  ast1:
-    [ [ x = prog2; IDENT "or"; y = prog1  -> bool_or loc x y
-      | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y
-      | x = prog2 -> x
-      ] ]
-  ;
-  ast2:
-    [ [ IDENT "not"; x = prog3 -> bool_not loc x
-      | x = prog3 -> x
-      ] ]
-  ;
-  ast3:
-    [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y
-      | x = prog4 -> x
-      ] ]
-    ;
-  ast4:
-    [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y
-      | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y
-      | x = prog5 -> x
-      ] ]
-    ;
-  ast5:
-    [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y 
-      | x = prog6 -> x
-      ] ]
-    ;
-  ast6:
-    [ [ "-"; x = prog6 -> un_op "Zopp" loc x
-      | x = ast7 -> without_effect loc x
-      ] ]
-    ;
-  ast7:
-    [ [ v = variable -> 
-	  Variable v
-      | n = INT ->
-	  Expression (constr_of_int n)
-      | "!"; v = variable ->
-	  Acc v
-      | "?" ->
-	  isevar
-      | v = variable; ":="; p = program ->
-	  Aff (v,p)
-      | v = variable; "["; e = program; "]" -> TabAcc (true,v,e)
-      | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e)
-      | v = variable; "["; e = program; "]"; ":="; p = program -> 
-	  TabAff (true,v,e,p)
-      | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> 
-	  TabAff (true,v,e,p)
-      | IDENT "if"; e1 = program; IDENT "then"; e2 = program;
-	IDENT "else"; e3 = program ->
-	  If (e1,e2,e3)
-      | IDENT "if"; e1 = program; IDENT "then"; e2 = program ->
-	  If (e1,e2,without_effect loc (Expression (constant "tt")))
-      | IDENT "while"; b = program; IDENT "do"; 
-	"{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}";
-	bl = block; IDENT "done" ->
-	  While (b, inv, wf, bl)
-      | IDENT "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program;
-	IDENT "do"; "{"; inv = invariant; "}"; 
-	bl = block; IDENT "done" -> 
-	  make_ast_for loc i v1 v2 inv bl
-      | IDENT "let"; v = variable; "="; IDENT "ref"; p1 = program;
-	"in"; p2 = program ->
-	  LetRef (v, p1, p2)
-      | IDENT "let"; v = variable; "="; p1 = program; "in"; p2 = program ->
-	  Let (v, p1, p2)
-      | IDENT "begin"; b = block; "end" ->
-	  Seq b
-      | IDENT "fun"; bl = binders; "->"; p = program ->
-	  Lam (bl,p)
-      | IDENT "let"; IDENT "rec"; f = variable; 
-	bl = binders; ":"; v = type_v;
-	"{"; IDENT "variant"; var = variant; "}"; "="; p = program ->
-	  LetRec (f,bl,v,var,p)
-      | IDENT "let"; IDENT "rec"; f = variable; 
-	bl = binders; ":"; v = type_v;
-	"{"; IDENT "variant"; var = variant; "}"; "="; p = program;
- 	"in"; p2 = program ->
-	  Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2)
-
-      | "@"; s = STRING; p = program ->
-	  Debug (s,p)
-
-      | "("; p = program; args = LIST0 arg; ")" ->
-	  match args with 
-	      [] -> 
-		if p.pre<>[] or p.post<>None then
-		  Pp.warning "Some annotations are lost";
-		p.desc
-            | _  -> 
-		Apply(p,args)
-     ] ]
-  ;
-  arg:
-    [ [ "'"; t = type_v -> Type t
-      | p = program -> Term p
-      ] ]
-  ;
-  block:
-    [ [ s = block_statement; ";"; b = block -> s::b
-      | s = block_statement                 -> [s] ] ]
-  ;
-  block_statement:
-    [ [ IDENT "label"; s = IDENT -> Label s
-      | IDENT "assert"; c = assertion -> Assert c 
-      | p = program -> Statement p ] ]
-  ;
-  relation:
-    [ [ "<"  -> "Z_lt_ge_bool"
-      | "<=" -> "Z_le_gt_bool"
-      | ">"  -> "Z_gt_le_bool"
-      | ">=" -> "Z_ge_lt_bool"
-      | "="  -> "Z_eq_bool"
-      | "<>" -> "Z_noteq_bool" ] ] 
-  ;
-
-  (* Other entries (invariants, etc.) ***************************************)
-  invariant:
-    [ [ IDENT "invariant"; c = predicate -> c ] ]
-  ;
-  variant:
-    [ [ c = Constr.constr; IDENT "for"; r = Constr.constr -> (c, r)
-      | c = Constr.constr -> (c, ast_zwf_zero loc) ] ]
-  ;
-  END
-else
-GEXTEND Gram
-  GLOBAL: type_v program;
-
-  (* Types ******************************************************************)
-  type_v:
-    [ [ t = type_v0 -> t ] ]
-  ;
-  type_v0:
-    [ [ t = type_v1 -> t ] ]
-  ;
-  type_v1:
-    [ [ t = type_v2 -> t ] ]
-  ;
-  type_v2:
-    [ LEFTA
-      [ v = type_v2; IDENT "ref" -> Ref v
-      | t = type_v3 -> t ] ]
-  ;
-  type_v3:
-    [ [ IDENT "array"; size = Constr.constr; IDENT "of"; v = type_v0 ->
-          Array (size,v)
-      | "fun"; bl = binders; c = type_c -> make_arrow bl c
-      | c = Constr.constr -> TypePure c	  
-      ] ]
-  ;
-  type_c:
-    [ [ IDENT "returns"; id = IDENT; ":"; v = type_v;
-        e = effects; p = OPT pre_condition; q = OPT post_condition; "end" ->
-        ((id_of_string id, v), e, list_of_some p, q)
-      ] ] 
-  ;
-  effects:
-    [ [ r = OPT reads; w = OPT writes ->
-	let r' = match r with Some l -> l | _ -> [] in
-	let w' = match w with Some l -> l | _ -> [] in
-	List.fold_left (fun e x -> Peffect.add_write x e)
-	  (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r')
-          w'
-      ] ]
-  ;
-  reads:
-    [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ]
-  ;
-  writes:
-    [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ]
-  ;
-  pre_condition:
-    [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ]
-  ;
-  post_condition:
-    [ [ IDENT "post"; c = predicate -> c ] ]
-  ;
-
-  (* Binders (for both types and programs) **********************************)
-  binder:
-    [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" ->
-	  List.map (fun s -> (id_of_string s, t)) sl
-      ] ]
-  ;
-  binder_type:
-    [ [ "Set" -> BindSet
-      | v = type_v -> BindType v
-      ] ]
-  ;
-  binders:
-    [ [ bl = LIST0 binder -> List.flatten bl ] ] 
-  ;
-
-  (* annotations *)
-  predicate:
-    [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ]
-  ;
-  dpredicate:
-    [ [ c = Constr.lconstr; n = name -> { a_name = n; a_value = c } ] ]
-  ;
-  name:
-    [ [ "as"; s = IDENT -> Name (id_of_string s)
-      | -> Anonymous
-      ] ]
-  ;
-
-  (* Programs ***************************************************************)
-  variable:
-    [ [ s = IDENT -> id_of_string s ] ]
-  ;
-  assertion:
-    [ [ "{"; c = dpredicate; "}" -> c ] ]
-  ;
-  precondition:
-    [ [ "{"; c = dpredicate; "}" -> pre_of_assert false c ] ]
-  ;
-  postcondition:
-    [ [ "{"; c = dpredicate; "}" -> c ] ]
-  ;
-  program:
-    [ [ p = prog1 -> p ] ]
-  ;
-  prog1:
-    [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog2:
-    [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog3:
-    [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog4:
-    [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog5:
-    [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-  prog6:
-    [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition ->
-	  mk_prog loc ast pre post ] ]
-  ;
-
-  ast1:
-    [ [ x = prog2; IDENT "or"; y = prog1  -> bool_or loc x y
-      | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y
-      | x = prog2 -> x
-      ] ]
-  ;
-  ast2:
-    [ [ IDENT "not"; x = prog3 -> bool_not loc x
-      | x = prog3 -> x
-      ] ]
-  ;
-  ast3:
-    [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y
-      | x = prog4 -> x
-      ] ]
-    ;
-  ast4:
-    [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y
-      | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y
-      | x = prog5 -> x
-      ] ]
-    ;
-  ast5:
-    [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y 
-      | x = prog6 -> x
-      ] ]
-    ;
-  ast6:
-    [ [ "-"; x = prog6 -> un_op "Zopp" loc x
-      | x = ast7 -> without_effect loc x
-      ] ]
-    ;
-  ast7:
-    [ [ v = variable -> 
-	  Variable v
-      | n = INT ->
-	  Expression (constr_of_int n)
-      | "!"; v = variable ->
-	  Acc v
-      | "?" ->
-	  isevar
-      | v = variable; ":="; p = program ->
-	  Aff (v,p)
-      | v = variable; "["; e = program; "]" -> TabAcc (true,v,e)
-      | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e)
-      | v = variable; "["; e = program; "]"; ":="; p = program -> 
-	  TabAff (true,v,e,p)
-      | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> 
-	  TabAff (true,v,e,p)
-      | "if"; e1 = program; "then"; e2 = program; "else"; e3 = program ->
-	  If (e1,e2,e3)
-      | "if"; e1 = program; "then"; e2 = program ->
-	  If (e1,e2,without_effect loc (Expression (constant "tt")))
-      | IDENT "while"; b = program; IDENT "do"; 
-	"{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}";
-	bl = block; IDENT "done" ->
-	  While (b, inv, wf, bl)
-      | "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program;
-	IDENT "do"; "{"; inv = invariant; "}"; 
-	bl = block; IDENT "done" -> 
-	  make_ast_for loc i v1 v2 inv bl
-      | "let"; v = variable; "="; IDENT "ref"; p1 = program;
-	"in"; p2 = program ->
-	  LetRef (v, p1, p2)
-      | "let"; v = variable; "="; p1 = program; "in"; p2 = program ->
-	  Let (v, p1, p2)
-      | IDENT "begin"; b = block; "end" ->
-	  Seq b
-      | "fun"; bl = binders; "=>"; p = program ->
-	  Lam (bl,p)
-      | "let"; IDENT "rec"; f = variable; 
-	bl = binders; ":"; v = type_v;
-	"{"; IDENT "variant"; var = variant; "}"; "="; p = program ->
-	  LetRec (f,bl,v,var,p)
-      | "let"; IDENT "rec"; f = variable; 
-	bl = binders; ":"; v = type_v;
-	"{"; IDENT "variant"; var = variant; "}"; "="; p = program;
- 	"in"; p2 = program ->
-	  Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2)
-
-      | "@"; s = STRING; p = program ->
-	  Debug (s,p)
-
-      | "("; p = program; args = LIST0 arg; ")" ->
-	  match args with 
-	      [] -> 
-		if p.pre<>[] or p.post<>None then
-		  Pp.warning "Some annotations are lost";
-		p.desc
-            | _  -> 
-		Apply(p,args)
-     ] ]
-  ;
-  arg:
-    [ [ "'"; t = type_v -> Type t
-      | p = program -> Term p
-      ] ]
-  ;
-  block:
-    [ [ s = block_statement; ";"; b = block -> s::b
-      | s = block_statement                 -> [s] ] ]
-  ;
-  block_statement:
-    [ [ IDENT "label"; s = IDENT -> Label s
-      | IDENT "assert"; c = assertion -> Assert c 
-      | p = program -> Statement p ] ]
-  ;
-  relation:
-    [ [ "<"  -> "Z_lt_ge_bool"
-      | "<=" -> "Z_le_gt_bool"
-      | ">"  -> "Z_gt_le_bool"
-      | ">=" -> "Z_ge_lt_bool"
-      | "="  -> "Z_eq_bool"
-      | "<>" -> "Z_noteq_bool" ] ] 
-  ;
-
-  (* Other entries (invariants, etc.) ***************************************)
-  invariant:
-    [ [ IDENT "invariant"; c = predicate -> c ] ]
-  ;
-  variant:
-    [ [ c = Constr.constr; "for"; r = Constr.constr -> (c, r)
-      | c = Constr.constr -> (c, ast_zwf_zero loc) ] ]
-  ;
-  END
-;;
-
-let wit_program, globwit_program, rawwit_program =
-  Genarg.create_arg "program"
-let wit_type_v, globwit_type_v, rawwit_type_v =
-  Genarg.create_arg "type_v"
-
-open Pp
-open Util
-open Himsg
-open Vernacinterp
-open Vernacexpr
-open Declare
-
-let is_assumed global ids =
-  if List.length ids = 1 then
-    msgnl (str (if global then "A global variable " else "") ++ 
-	     pr_id (List.hd ids) ++ str " is assumed")
-  else
-    msgnl (str (if global then "Some global variables " else "") ++
-	     prlist_with_sep (fun () -> (str ", ")) pr_id ids ++
-	     str " are assumed")
-
-open Pcoq
-
-(* Variables *)
-
-let wit_variables, globwit_variables, rawwit_variables =
-  Genarg.create_arg "variables"
-
-let variables = Gram.Entry.create "Variables"
-
-GEXTEND Gram
-  variables: [ [ l = LIST1 Prim.ident SEP "," -> l ] ];
-END
-
-let pr_variables _prc _prtac l = spc() ++ prlist_with_sep pr_coma pr_id l
-
-let _ =
-  Pptactic.declare_extra_genarg_pprule true
-    (rawwit_variables, pr_variables)
-    (globwit_variables, pr_variables)
-    (wit_variables, pr_variables)
-
-(* then_tac *)
-
-open Genarg
-open Tacinterp
-
-let pr_then_tac _ prt = function
-  | None -> mt ()
-  | Some t -> pr_semicolon () ++ prt t
-
-ARGUMENT EXTEND then_tac
-  TYPED AS tactic_opt 
-  PRINTED BY pr_then_tac
-  INTERPRETED BY interp_genarg
-  GLOBALIZED BY intern_genarg
-| [ ";" tactic(t) ] -> [ Some t ]
-| [ ] -> [ None ]
-END
-
-(* Correctness *)
-
-VERNAC COMMAND EXTEND Correctness
-  [ "Correctness" preident(str) program(pgm) then_tac(tac) ]
-   -> [ Ptactic.correctness str pgm (Option.map Tacinterp.interp tac) ]
-END
-
-(* Show Programs *)
-
-let show_programs () =
-  fold_all 
-    (fun (id,v) _ -> 
-      msgnl (pr_id id ++ str " : " ++ 
-      hov 2 (match v with TypeV v -> pp_type_v v
-	| Set -> (str "Set")) ++
-      fnl ()))
-    Penv.empty ()
-
-VERNAC COMMAND EXTEND ShowPrograms
-  [ "Show" "Programs" ] -> [ show_programs () ]
-END
-
-(* Global Variable *)
-
-let global_variable ids v =
-  List.iter
-    (fun id -> if Penv.is_global id then
-      Util.errorlabstrm "PROGVARIABLE"
-	(str"Clash with previous constant " ++ pr_id id))
-    ids;
-  Pdb.check_type_v (all_refs ()) v;
-  let env = empty in
-  let ren = update empty_ren "" [] in
-  let v = Ptyping.cic_type_v env ren v in
-  if not (is_mutable v) then begin
-    let c = 
-      Entries.ParameterEntry (trad_ml_type_v ren env v),
-      Decl_kinds.IsAssumption Decl_kinds.Definitional in
-    List.iter 
-      (fun id -> ignore (Declare.declare_constant id c)) ids;
-    if_verbose (is_assumed false) ids
-  end;
-  if not (is_pure v) then begin
-    List.iter (fun id -> ignore (Penv.add_global id v None)) ids;
-    if_verbose (is_assumed true) ids
-  end
-
-VERNAC COMMAND EXTEND ProgVariable
-  [ "Global" "Variable" variables(ids) ":" type_v(t) ]
-  -> [ global_variable ids t]
-END
-
-let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
-
-(* Type printer *)
-
-let pr_reads = function
-  | [] -> mt ()
-  | l -> spc () ++
-      hov 0 (str "reads" ++ spc () ++ prlist_with_sep pr_coma pr_id l)
-
-let pr_writes = function
-  | [] -> mt ()
-  | l -> spc () ++
-      hov 0 (str "writes" ++ spc () ++ prlist_with_sep pr_coma pr_id l)
-
-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 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 } =
-  pr_predicate b { a_name = x; a_value = v }
-
-let pr_pre_condition_list = function
-  | [] -> mt ()
-  | [pre] -> spc() ++ hov 0 (str "pre" ++ spc () ++ pr_assert false pre)
-  | _ -> assert false
-
-let pr_post_condition_opt = function
-  | None -> mt ()
-  | Some post ->
-      spc() ++ hov 0 (str "post" ++ spc () ++ pr_predicate false post)
-
-let rec pr_type_v_v8 = function
-  | Array (a,v) ->
-      str "array" ++ spc() ++ Ppconstr.pr_constr a ++ spc() ++ str "of " ++
-      pr_type_v_v8 v
-  | v -> pr_type_v3 v
-
-and pr_type_v3 = function
-  | Ref v -> pr_type_v3 v ++ spc () ++ str "ref"
-  | Arrow (bl,((id,v),e,prel,postl)) ->
-      str "fun" ++ spc() ++ hov 0 (prlist_with_sep cut pr_binder bl) ++
-      spc () ++ str "returns" ++ spc () ++ pr_id id ++ str ":" ++ 
-      pr_type_v_v8 v ++ pr_effects e ++ 
-      pr_pre_condition_list prel ++ pr_post_condition_opt postl ++
-      spc () ++ str "end"
-  | TypePure a -> Ppconstr.pr_constr a
-  | v -> str "(" ++ pr_type_v_v8 v ++ str ")"
-
-and pr_binder = function
-  | (id,BindType c) ->
-      str "(" ++ pr_id id ++ str ":" ++ pr_type_v_v8 c ++ str ")"
-  | (id,BindSet) ->
-      str "(" ++ pr_id id ++ str ":" ++ str "Set" ++ str ")"
-  | (id,Untyped) ->
-      str "<<<<< TODO: Untyped binder >>>>"
-
-let _ =
-  Pptactic.declare_extra_genarg_pprule true
-    (rawwit_type_v, fun _ _ -> pr_type_v_v8)
-    (globwit_type_v, fun _ -> raise Not_found)
-    (wit_type_v, fun _ -> raise Not_found)
-
-(* Program printer *)
-
-let pr_precondition pred = str "{" ++ pr_assert true pred ++ str "}" ++ spc ()
-
-let pr_postcondition pred = str "{" ++ pr_predicate true pred ++ str "}"
-
-let pr_invariant = function
-  | None -> mt ()
-  | Some c -> hov 2 (str "invariant" ++ spc ()  ++ pr_predicate false c)
-
-let pr_variant (c1,c2) =
-  Ppconstr.pr_constr c1 ++
-  (try Constrextern.check_same_type c2 (ast_zwf_zero dummy_loc); mt ()
-   with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstr.pr_constr c2))
-
-let rec pr_desc = function
-  | Variable id ->
-      (* Unsafe: should distinguish global names and bound vars *)
-      let vars = (* TODO *) Idset.empty in
-      let id = try 
-        snd (repr_qualid
-          (snd (qualid_of_reference 
-            (Constrextern.extern_reference
-              dummy_loc vars (Nametab.locate (make_short_qualid id))))))
-      with _ -> id in
-      pr_id id
-  | Acc id -> str "!" ++ pr_id id
-  | Aff (id,p) -> pr_id id ++ spc() ++ str ":=" ++ spc() ++ pr_prog p
-  | TabAcc (b,id,p) -> pr_id id ++ str "[" ++ pr_prog p ++ str "]"
-  | TabAff (b,id,p1,p2) ->
-      pr_id id ++ str "[" ++ pr_prog p1 ++ str "]" ++
-      str ":=" ++ pr_prog p2
-  | Seq bll -> 
-      hv 0 (str "begin" ++ spc () ++ pr_block bll ++ spc () ++ str "end")
-  | While (p1,inv,var,bll) ->
-      hv 0 (
-	hov 0 (str "while" ++ spc () ++ pr_prog p1 ++ spc () ++ str "do") ++
-	brk (1,2) ++
-	hv 2 (
-	  str "{ " ++ 
-	  pr_invariant inv ++ spc() ++
-	  hov 0 (str "variant" ++ spc () ++ pr_variant var)
-	  ++ str " }") ++ cut () ++
-	hov 0 (pr_block bll) ++ cut () ++ 
-	str "done")
-  | If (p1,p2,p3) ->
-      hov 1 (str "if " ++ pr_prog p1) ++ spc () ++
-      hov 0 (str "then" ++ spc () ++ pr_prog p2) ++ spc () ++
-      hov 0 (str "else" ++ spc () ++ pr_prog p3)
-  | Lam (bl,p) ->
-      hov 0 
-        (str "fun" ++ spc () ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ 
-	 spc () ++ str "=>") ++
-      pr_prog p
-  | Apply ({desc=Expression e; pre=[]; post=None} as p,args) when isConst e ->
-      begin match
-	string_of_id (snd (repr_path (Nametab.sp_of_global (ConstRef (destConst e))))),
-	args
-      with
-      | "Zmult", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str"*" ++ pr_arg a2 ++ str ")"
-      | "Zplus", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str"+" ++ pr_arg a2 ++ str ")"
-      | "Zminus", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str"-" ++ pr_arg a2 ++ str ")"
-      | "Zopp", [a] ->
-	  str "( -" ++ pr_arg a ++ str ")"
-      | "Z_lt_ge_bool", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str"<" ++ pr_arg a2 ++ str ")"
-      | "Z_le_gt_bool", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str"<=" ++ pr_arg a2 ++ str ")"
-      | "Z_gt_le_bool", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str">" ++ pr_arg a2 ++ str ")"
-      | "Z_ge_lt_bool", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str">=" ++ pr_arg a2 ++ str ")"
-      | "Z_eq_bool", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str"=" ++ pr_arg a2 ++ str ")"
-      | "Z_noteq_bool", [a1;a2] ->
-	  str "(" ++ pr_arg a1 ++ str"<> " ++ pr_arg a2 ++ str ")"
-      | _ -> 
-	  str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++
-	  str ")"
-      end
-  | Apply (p,args) ->
-      str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++
-      str ")"
-  | SApp ([Variable v], args) ->
-      begin match string_of_id v, args with
-	| "prog_bool_and", [a1;a2] -> 
-	    str"(" ++ pr_prog a1 ++ spc() ++ str"and " ++ pr_prog a2 ++str")"
-	| "prog_bool_or", [a1;a2] -> 
-	    str"(" ++ pr_prog a1 ++ spc() ++ str"or " ++ pr_prog a2 ++ str")"
-	| "prog_bool_not", [a] ->
-	    str "(not " ++ pr_prog a ++ str ")"
-	| _ -> failwith "Correctness printer: TODO"
-      end
-  | SApp _ -> failwith "Correctness printer: TODO"
-  | LetRef (v,p1,p2) ->
-      hov 2 (
-	str "let " ++ pr_id v ++ str " =" ++ spc () ++ str "ref" ++ spc () ++
-	pr_prog p1 ++ str " in") ++
-      spc () ++ pr_prog p2
-  | Let (id, {desc=LetRec (f,bl,v,var,p); pre=[]; post=None },p2) when f=id ->
-      hov 2 (
-	str "let rec " ++ pr_id f ++ spc () ++
-	hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++
-	str ":" ++ pr_type_v_v8 v ++ spc () ++
-	hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++ 
-	spc() ++ str "=" ++ spc () ++ pr_prog p ++
- 	str " in") ++
-      spc () ++ pr_prog p2
-  | Let (v,p1,p2) ->
-      hov 2 (
-	str "let " ++ pr_id v ++ str " =" ++ spc () ++ pr_prog p1 ++ str" in")
-      ++ spc () ++ pr_prog p2
-  | LetRec (f,bl,v,var,p) ->
-      str "let rec " ++ pr_id f ++ spc () ++
-      hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++
-      str ":" ++ pr_type_v_v8 v ++ spc () ++
-      hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++
-      spc () ++ str "=" ++ spc () ++ pr_prog p
-  | PPoint _ -> str "TODO: Ppoint" (* Internal use only *)
-  | Expression c ->
-      (* 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 "@" ++ Pptactic.qsnew s ++ pr_prog p
-
-and pr_block_st = function
-  | Label s -> hov 0 (str "label" ++ spc() ++ str s)
-  | Assert pred -> 
-      hov 0 (str "assert" ++ spc() ++ hov 0 (pr_postcondition pred))
-  | Statement p -> pr_prog p
-
-and pr_block bl = prlist_with_sep pr_semicolon pr_block_st bl
-
-and pr_arg = function
-  | Past.Term p -> pr_prog p
-  | Past.Type t -> str "'" ++ pr_type_v_v8 t
-  | Refarg _ -> str "TODO: Refarg" (* Internal use only *)
-
-and pr_prog0 b { desc = desc; pre = pre; post = post } =
-  hv 0 (
-    prlist pr_precondition pre ++
-    hov 0
-      (if b & post<>None then str"(" ++ pr_desc desc ++ str")"
-       else pr_desc desc)
-    ++ Ppconstr.pr_opt pr_postcondition post)
-
-and pr_prog x = pr_prog0 true x
-
-let _ =
-  Pptactic.declare_extra_genarg_pprule true
-    (rawwit_program, fun _ _ a -> spc () ++ pr_prog0 false a)
-    (globwit_program, fun _ -> raise Not_found)
-    (wit_program, fun _ -> raise Not_found)
-
diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli
deleted file mode 100644
index ba3ba5449a..0000000000
--- a/contrib/correctness/psyntax.mli
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pcoq
-open Ptype
-open Past
-open Topconstr
-
-(* Grammar for the programs and the tactic Correctness *)
-
-module Programs :
-  sig
-    val program : program Gram.Entry.e
-    val type_v  : constr_expr ml_type_v Gram.Entry.e
-    val type_c  : constr_expr ml_type_c Gram.Entry.e
-  end
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
deleted file mode 100644
index 76ba04c514..0000000000
--- a/contrib/correctness/ptactic.ml
+++ /dev/null
@@ -1,257 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp
-open Flags
-open Names
-open Libnames
-open Term
-open Pretyping
-open Pfedit
-open Decl_kinds
-open Vernacentries
-
-open Pmisc
-open Putil
-open Past
-open Penv
-open Prename
-open Peffect
-open Pmonad
-
-(* [coqast_of_prog: program -> constr * constr]
- * Traduction d'un programme impératif en un but (second constr)
- * et un terme de preuve partiel pour ce but (premier constr)
- *)
-
-let coqast_of_prog p =
-  (* 1. db : séparation dB/var/const *)
-  let p = Pdb.db_prog p in
-
-  (* 2. typage avec effets *)
-  deb_mess (str"Ptyping.states: Typing with effects..." ++ fnl ());
-  let env = Penv.empty in
-  let ren = initial_renaming env in
-  let p = Ptyping.states ren env p in
-  let ((_,v),_,_,_) as c = p.info.kappa in
-  Perror.check_for_not_mutable p.loc v;
-  deb_print pp_type_c c;
-
-  (* 3. propagation annotations *)
-  let p = Pwp.propagate ren p in
-
-  (* 4a. traduction type *)
-  let ty = Pmonad.trad_ml_type_c ren env c in
-  deb_print (Printer.pr_lconstr_env (Global.env())) ty;
-
-  (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
-  deb_mess 
-    (fnl () ++ str"Mlize.trad: Translation program -> cc_term..." ++ fnl ());
-  let cc = Pmlize.trans ren p in
-  let cc = Pred.red cc in
-  deb_print Putil.pp_cc_term cc;
-
-  (* 5. traduction en constr *)
-  deb_mess 
-    (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ 
-       fnl ());
-  let r = Pcic.rawconstr_of_prog cc in
-  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.pr_lconstr_env (Global.env())) (snd oc);
-
-  p,oc,ty,v
-
-(* [automatic : tactic]
- * 
- * Certains buts engendrés par "correctness" (ci-dessous)
- * sont réellement triviaux. On peut les résoudre aisément, sans pour autant
- * tomber dans la solution trop lourde qui consiste à faire "; Auto."
- *
- * Cette tactique fait les choses suivantes :
- *   o  elle élimine les hypothèses de nom loop<i>
- *   o  sur  G |- (well_founded nat lt) ==> Exact lt_wf.  
- *   o  sur  G |- (well_founded Z (Zwf c)) ==> Exact (Zwf_well_founded c)
- *   o  sur  G |- e = e' ==> Reflexivity.  (arg. de decr. des boucles)
- *                           sinon Try Assumption.
- *   o  sur  G |- P /\ Q ==> Try (Split; Assumption). (sortie de boucle)
- *   o  sinon, Try AssumptionBis (= Assumption + décomposition /\ dans hyp.)
- *             (pour entrée dans corps de boucle par ex.)
- *)
-
-open Pattern
-open Tacmach
-open Tactics
-open Tacticals
-open Equality
-open Nametab
-
-let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0)
-let lt = ConstRef (coq_constant ["Init";"Peano"] "lt")
-let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded")
-let z = IndRef (coq_constant ["ZArith";"BinInt"] "Z", 0)
-let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0)
-let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0)
-
-let mkmeta n = Nameops.make_ident "X" (Some n)
-let mkPMeta n = PMeta (Some (mkmeta n))
-
-(* ["(well_founded nat lt)"] *)
-let wf_nat_pattern = 
-  PApp (PRef well_founded, [| PRef nat; PRef lt |])
-(* ["((well_founded Z (Zwf ?1))"] *)
-let wf_z_pattern = 
-  let zwf = ConstRef (coq_constant ["ZArith";"Zwf"] "Zwf") in
-  PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| mkPMeta 1 |]) |])
-(* ["(and ?1 ?2)"] *)
-let and_pattern = 
-  PApp (PRef and_, [| mkPMeta 1; mkPMeta 2 |])
-(* ["(eq ?1 ?2 ?3)"] *)
-let eq_pattern = 
-  PApp (PRef eq, [| mkPMeta 1; mkPMeta 2; mkPMeta 3 |])
-
-(* loop_ids: remove loop<i> hypotheses from the context, and rewrite
- * using Variant<i> hypotheses when needed. *)
- 
-let (loop_ids : tactic) = fun gl ->
-  let rec arec hyps gl =
-    let env = pf_env gl in
-    let concl = pf_concl gl in 
-    match hyps with
-      | [] -> tclIDTAC gl
-      | (id,a) :: al ->
-	  let s = string_of_id id in
-	  let n = String.length s in
-	  if n >= 4 & (let su = String.sub s 0 4 in su="loop" or su="Bool")
-	  then
-	    tclTHEN (clear [id]) (arec al) gl
-	  else if n >= 7 & String.sub s 0 7 = "Variant" then begin
-	    match pf_matches gl eq_pattern a with
-	      | [_; _,varphi; _] when isVar varphi ->
-		  let phi = destVar varphi in
-		  if Termops.occur_var env phi concl then
-		    tclTHEN (rewriteLR (mkVar id)) (arec al) gl
-		  else
-		    arec al gl
-	      | _ -> assert false end
-	  else
-	    arec al gl
-  in 
-  arec (pf_hyps_types gl) gl
-
-(* assumption_bis: like assumption, but also solves ... h:A/\B ... |- A 
- * (resp. B) *)
-
-let (assumption_bis : tactic) = fun gl ->
-  let concl = pf_concl gl in 
-  let rec arec = function
-    | [] -> Util.error "No such assumption"
-    | (s,a) :: al ->
-	if pf_conv_x_leq gl a concl then 
-          refine (mkVar s) gl
-	else if pf_is_matching gl and_pattern a then
-	  match pf_matches gl and_pattern a with
-	    | [_,c1; _,c2] -> 
-		if pf_conv_x_leq gl c1 concl then
-		  exact_check (applistc (constant "proj1") [c1;c2;mkVar s]) gl
-		else if pf_conv_x_leq gl c2 concl then
-		  exact_check (applistc (constant "proj2") [c1;c2;mkVar s]) gl
-		else
-		  arec al
-	    | _ -> assert false
-	else
-	  arec al
-  in 
-  arec (pf_hyps_types gl)
-
-(* automatic: see above *)
-
-let (automatic : tactic) =
-  tclTHEN
-    loop_ids
-    (fun gl ->
-       let c = pf_concl gl in
-	 if pf_is_matching gl wf_nat_pattern c then
-	   exact_check (constant "lt_wf") gl
-	 else if pf_is_matching gl wf_z_pattern c then
-	   let (_,z) = List.hd (pf_matches gl wf_z_pattern c) in
-	   exact_check (Term.applist (constant "Zwf_well_founded",[z])) gl
-	 else if pf_is_matching gl and_pattern c then
-	   (tclORELSE assumption_bis
-	      (tclTRY (tclTHEN simplest_split assumption))) gl
-	 else if pf_is_matching gl eq_pattern c then
-	   (tclORELSE reflexivity (tclTRY assumption_bis)) gl
-	 else
-	   tclTRY assumption_bis gl)
-      
-(* [correctness s p] : string -> program -> tactic option -> unit
- *
- * Vernac: Correctness <string> <program> [; <tactic>].
- *)
-
-let reduce_open_constr (em0,c) =
-  let existential_map_of_constr = 
-    let rec collect em c = match kind_of_term c with
-      | Cast (c',t) -> 
-	  (match kind_of_term c' with
-	     | Evar (ev,_) ->
-                 if not (Evd.mem em ev) then
-                   Evd.add em ev (Evd.find em0 ev)
-                 else
-                   em
-	     | _ -> fold_constr collect em c)
-      | Evar _ -> 
-	  assert false (* all existentials should be casted *)
-      | _ -> 
-	  fold_constr collect em c
-    in
-    collect Evd.empty
-  in
-  let c = Pred.red_cci c in
-  let em = existential_map_of_constr c in
-  (em,c)
-
-let register id n =
-  let id' = match n with None -> id | Some id' -> id' in
-  Penv.register id id'
-
-  (* On dit à la commande "Save" d'enregistrer les nouveaux programmes *)
-let correctness_hook _ ref = 
-  let pf_id = Nametab.id_of_global ref in
-  register pf_id None
-
-let correctness s p opttac =
-  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
-  let sign = Global.named_context () in
-  let sigma = Evd.empty in
-  let cty = Reduction.nf_betaiota cty in
-  let id = id_of_string s in 
-  start_proof id (IsGlobal (Proof Lemma)) sign cty correctness_hook;
-  Penv.new_edited id (v,p);
-  if !debug then msg (Pfedit.pr_open_subgoals());
-  deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
-  let oc = reduce_open_constr oc in
-  deb_mess (str"AFTER REDUCTION:" ++ fnl ());
-  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
-    | Some t -> tclTHEN tac t
-  in
-  solve_nth 1 tac;
-  if_verbose msg (pr_open_subgoals ())
diff --git a/contrib/correctness/ptactic.mli b/contrib/correctness/ptactic.mli
deleted file mode 100644
index 3c3d134234..0000000000
--- a/contrib/correctness/ptactic.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-(* 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
- * tactic with the partial proof term obtained by the translation of
- * P into a functional program.
- *
- * Then an ad-hoc automatic tactic is applied on each subgoal to solve the
- * trivial proof obligations *)
-
-val correctness : string -> Past.program -> Tacmach.tactic option -> unit
-
diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli
deleted file mode 100644
index e0e24f9aad..0000000000
--- a/contrib/correctness/ptype.mli
+++ /dev/null
@@ -1,73 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Term
-
-(* Types des valeurs (V) et des calculs (C).
- *
- * On a C = r:V,E,P,Q 
- *
- *   et V = (x1:V1)...(xn:Vn)C | V ref | V array | <type pur>
- *
- * INVARIANT: l'effet E contient toutes les variables apparaissant dans
- *            le programme ET les annotations P et Q
- *            Si E = { x1,...,xn | y1,...,ym }, les variables x sont les
- *            variables en lecture seule et y1 les variables modifiées
- *            les xi sont libres dans P et Q, et les yi,result liées dans Q
- *            i.e.  P = p(x)
- *               et Q = [y1]...[yn][res]q(x,y,res)
- *)
-
-(* pre and post conditions *)
-
-type 'a precondition = { p_assert : bool; p_name : Names.name; p_value : 'a }
-
-type 'a assertion  = { a_name : Names.name; a_value : 'a }
-
-type 'a postcondition = 'a assertion
-
-type predicate = constr assertion
-
-(* binders *)
-
-type 'a binder_type =
-    BindType  of 'a
-  | BindSet
-  | Untyped
-
-type 'a binder = Names.identifier * 'a binder_type
-
-(* variant *)
-
-type variant = constr * constr * constr (* phi, R, A *)
-
-(* types des valeurs *)
-
-type 'a ml_type_v =
-    Ref       of 'a ml_type_v
-  | Array     of 'a * 'a ml_type_v   (* size x type *)
-  | Arrow     of 'a ml_type_v binder list * 'a ml_type_c
-
-  | TypePure  of 'a
-
-(* et type des calculs *)
-
-and 'a ml_type_c =
-    (Names.identifier * 'a ml_type_v) 
-  * Peffect.t
-  * ('a precondition list) * ('a postcondition option)
-
-(* at beginning they contain Coq AST but they become constr after typing *)
-type type_v = constr ml_type_v
-type type_c = constr ml_type_c
-
-
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
deleted file mode 100644
index 58c2e33576..0000000000
--- a/contrib/correctness/ptyping.ml
+++ /dev/null
@@ -1,600 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Termops
-open Environ
-open Constrintern
-open Himsg
-open Proof_trees
-open Topconstr
-
-open Pmisc
-open Putil
-open Prename
-open Ptype
-open Past
-open Penv 
-open Peffect
-open Pcicenv
-
-(* Ce module implante le jugement  Gamma |-a e : kappa  de la thèse.
- * Les annotations passent du type CoqAst.t au type Term.constr ici. 
- * Les post-conditions sont abstraites par rapport au résultat. *)
-
-let simplify_type_of env sigma t =
-  Reductionops.nf_betaiota (Typing.type_of env sigma t)
-
-let just_reads e =
-  difference (get_reads e) (get_writes e)
-
-let type_v_sup loc t1 t2 =
-  if t1 = t2 then
-    t1
-  else
-    Perror.if_branches loc
-
-let typed_var ren env (phi,r) =
-  let sign = Pcicenv.before_after_sign_of ren env in
-  let a = simplify_type_of (Global.env_of_context sign) Evd.empty phi in
-  (phi,r,a)
-
-(* Application de fonction *)
-
-let rec convert = function
-  | (TypePure c1, TypePure c2) -> 
-      Reductionops.is_conv (Global.env ()) Evd.empty c1 c2
-  | (Ref v1, Ref v2) -> 
-      convert (v1,v2)
-  | (Array (s1,v1), Array (s2,v2)) -> 
-      (Reductionops.is_conv (Global.env ()) Evd.empty s1 s2) && (convert (v1,v2))
-  | (v1,v2) -> v1 = v2
-      
-let effect_app ren env f args =
-  let n = List.length args in
-  let tf = 
-    let ((_,v),_,_,_) = f.info.kappa in
-    match v with TypePure c -> v_of_constr c | _ -> v
-  in
-  let bl,c = 
-    match tf with
-	Arrow (bl, c) ->
-	  if List.length bl <> n then Perror.partial_app f.loc;
-	  bl,c
-      | _ -> Perror.app_of_non_function f.loc
-  in
-  let check_type loc v t so =
-    let v' = type_v_rsubst so v in
-    if not (convert (v',t)) then Perror.expected_type loc (pp_type_v v')
-  in
-  let s,so,ok = 
-    (* s est la substitution des références, so celle des autres arg. 
-     * ok nous dit si les arguments sont sans effet i.e. des expressions *)
-    List.fold_left
-    (fun (s,so,ok) (b,a) ->
-       match b,a with
-	   (id,BindType (Ref _ | Array _ as v)), Refarg id' ->
-	     let ta = type_in_env env id' in
-	     check_type f.loc v ta so;
-	     (id,id')::s, so, ok
-	 | _, Refarg _ -> Perror.should_be_a_variable f.loc
-	 | (id,BindType v), Term t ->
-	     let ((_,ta),_,_,_) = t.info.kappa in
-	     check_type t.loc v ta so;
-	     (match t.desc with
-		  Expression c -> s, (id,c)::so, ok
-		| _ -> s,so,false)
-	 | (id,BindSet), Type v ->
-	     let c = Pmonad.trad_ml_type_v ren env v in
-	     s, (id,c)::so, ok
-	 | (id,BindSet), Term t -> Perror.expects_a_type id t.loc
-	 | (id,BindType _), Type _ -> Perror.expects_a_term id
-	 | (_,Untyped), _ -> invalid_arg "effects_app")
-    ([],[],true)
-    (List.combine bl args)
-  in
-  let (id,v),ef,pre,post = type_c_subst s c in
-  (bl,c), (s,so,ok), ((id,type_v_rsubst so v),ef,pre,post)
-
-(* Execution of a Coq AST. Returns value and type.
- * Also returns its variables *)
-
-let state_coq_ast sign a =
-  let env = Global.env_of_context sign in
-  let j =
-    reraise_with_loc (constr_loc a) (judgment_of_rawconstr Evd.empty env) a in
-  let ids = global_vars env j.uj_val in
-  j.uj_val, j.uj_type, ids
-
-(* [is_pure p] tests wether the program p is an expression or not. *)
-
-let type_of_expression ren env c =
-  let sign = now_sign_of ren env in
-  simplify_type_of (Global.env_of_context sign) Evd.empty c
-
-let rec is_pure_type_v = function
-    TypePure _ -> true
-  | Arrow (bl,c) -> List.for_all is_pure_arg bl & is_pure_type_c c
-  | Ref _ | Array _ -> false
-and is_pure_arg = function
-    (_,BindType v) -> is_pure_type_v v
-  | (_,BindSet) -> true
-  | (_,Untyped) -> false
-and is_pure_type_c = function
-    (_,v),_,[],None -> is_pure_type_v v
-  | _ -> false
-
-let rec is_pure_desc ren env = function
-    Variable id ->
-      not (is_in_env env id) or (is_pure_type_v (type_in_env env id))
-  | Expression c -> 
-      (c = isevar) or (is_pure_cci (type_of_expression ren env c))
-  | Acc _ -> true
-  | TabAcc (_,_,p) -> is_pure ren env p
-  | Apply (p,args) -> 
-      is_pure ren env p & List.for_all (is_pure_arg ren env) args
-  | SApp _ | Aff _ | TabAff _ | Seq _ | While _ | If _ 
-  | Lam _ | LetRef _ | Let _ | LetRec _ -> false
-  | Debug (_,p) -> is_pure ren env p
-  | PPoint (_,d) -> is_pure_desc ren env d
-and is_pure ren env p =
-  p.pre = [] & p.post = None & is_pure_desc ren env p.desc
-and is_pure_arg ren env = function
-    Term p -> is_pure ren env p
-  | Type _ -> true
-  | Refarg _ -> false
-
-(* [state_var ren env (phi,r)] returns a tuple (e,(phi',r')) 
- * where e is the effect of the variant phi and phi',r' the corresponding 
- * constr of phi and r.
- *)
-
-let state_var ren env (phi,r) = 
-  let sign = Pcicenv.before_after_sign_of ren env in
-  let phi',_,ids = state_coq_ast sign phi in
-  let ef = List.fold_left
-	     (fun e id ->
-		if is_mutable_in_env env id then Peffect.add_read id e else e)
-	     Peffect.bottom ids in
-  let r',_,_ = state_coq_ast (Global.named_context ()) r in
-  ef,(phi',r')
-	
-(* [state_pre ren env pl] returns a pair (e,c) where e is the effect of the
- * pre-conditions list pl and cl the corresponding constrs not yet abstracted
- * over the variables xi (i.e. c NOT [x1]...[xn]c !)
- *)
-
-let state_pre ren env pl =
-  let state e p =
-    let sign = Pcicenv.before_sign_of ren env in
-    let cc,_,ids = state_coq_ast sign p.p_value in
-    let ef = List.fold_left
-	       (fun e id ->
-		  if is_mutable_in_env env id then
-		    Peffect.add_read id e
-		  else if is_at id then
-		    let uid,_ = un_at id in
-		    if is_mutable_in_env env uid then
-		      Peffect.add_read uid e
-		    else
-		      e
-	     	  else
-		    e)
-	       e ids 
-    in
-    ef,{ p_assert = p.p_assert; p_name = p.p_name; p_value = cc }
-  in
-  List.fold_left 
-    (fun (e,cl) p -> let ef,c = state e p in (ef,c::cl)) 
-    (Peffect.bottom,[]) pl
-
-let state_assert ren env a =
-  let p = pre_of_assert true a in
-  let e,l = state_pre ren env [p] in
-  e,assert_of_pre (List.hd l)
-
-let state_inv ren env = function
-    None -> Peffect.bottom, None
-  | Some i -> let e,p = state_assert ren env i in e,Some p
-	  
-(* [state_post ren env (id,v,ef) q] returns a pair (e,c)
- * where e is the effect of the
- * post-condition q and c the corresponding constr not yet abstracted
- * over the variables xi, yi and result.
- * Moreover the RW variables not appearing in ef have been replaced by
- * RO variables, and (id,v) is the result
- *)
-
-let state_post ren env (id,v,ef) = function
-    None -> Peffect.bottom, None
-  | Some q ->
-      let v' = Pmonad.trad_ml_type_v ren env v in
-      let sign = Pcicenv.before_after_result_sign_of (Some (id,v')) ren env in
-      let cc,_,ids = state_coq_ast sign q.a_value in
-      let ef,c = 
-	List.fold_left
-	  (fun (e,c) id ->
-	     if is_mutable_in_env env id then
-	       if is_write ef id then
-		 Peffect.add_write id e, c
-	       else
-		 Peffect.add_read id e,
-		 subst_in_constr [id,at_id id ""] c
-	     else if is_at id then
-	       let uid,_ = un_at id in
-	       if is_mutable_in_env env uid then
-		 Peffect.add_read uid e, c
-	       else
-		 e,c
-	     else
-	       e,c)
-	  (Peffect.bottom,cc) ids 
-      in
-      let c = abstract [id,v'] c in
-      ef, Some { a_name = q.a_name; a_value = c }
-
-(* transformation of AST into constr in types V and C *)
-
-let rec cic_type_v env ren = function
-  | Ref v -> Ref (cic_type_v env ren v)
-  | Array (com,v) ->
-      let sign = Pcicenv.now_sign_of ren env in
-      let c = interp_constr Evd.empty (Global.env_of_context sign) com in
-      Array (c, cic_type_v env ren v)
-  | Arrow (bl,c) ->
-      let bl',ren',env' =
-	List.fold_left
-	(fun (bl,ren,env) b ->
-	   let b' = cic_binder env ren b in
-	   let env' = traverse_binders env [b'] in
-	   let ren' = initial_renaming env' in
-	     b'::bl,ren',env')
-	([],ren,env) bl
-      in
-      let c' = cic_type_c env' ren' c in
-      Arrow (List.rev bl',c')
-  | TypePure com ->
-      let sign = Pcicenv.cci_sign_of ren env in
-      let c = interp_constr Evd.empty (Global.env_of_context sign) com in
-      TypePure c
-
-and cic_type_c env ren ((id,v),e,p,q) =
-  let v' = cic_type_v env ren v in
-  let cv = Pmonad.trad_ml_type_v ren env v' in
-  let efp,p' = state_pre ren env p in
-  let efq,q' = state_post ren env (id,v',e) q in
-  let ef = Peffect.union e (Peffect.union efp efq) in
-  ((id,v'),ef,p',q')
-
-and cic_binder env ren = function
-  | (id,BindType v) ->
-      let v' = cic_type_v env ren v in
-      let env' = add (id,v') env in
-      let ren' = initial_renaming env' in
-      (id, BindType v')
-  | (id,BindSet) -> (id,BindSet)
-  | (id,Untyped) -> (id,Untyped)
-
-and cic_binders env ren = function
-    [] -> []
-  | b::bl ->
-      let b' = cic_binder env ren b in
-      let env' = traverse_binders env [b'] in
-      let ren' = initial_renaming env' in
-      b' :: (cic_binders env' ren' bl)
-
-
-(* The case of expressions.
- * 
- * Expressions are programs without neither effects nor pre/post conditions.
- * But access to variables are allowed.
- *
- * Here we transform an expression into the corresponding constr,
- * the variables still appearing as VAR (they will be abstracted in
- * Mlise.trad)
- * We collect the pre-conditions (e<N for t[e]) as we traverse the term.
- * We also return the effect, which does contain only *read* variables.
- *)
-
-let states_expression ren env expr =
-  let rec effect pl = function
-    | Variable id -> 
-	(if is_global id then constant (string_of_id id) else mkVar id),
-	pl, Peffect.bottom
-    | Expression c -> c, pl, Peffect.bottom
-    | Acc id -> mkVar id, pl, Peffect.add_read id Peffect.bottom
-    | TabAcc (_,id,p) ->
-	let c,pl,ef = effect pl p.desc in
-	let pre = Pmonad.make_pre_access ren env id c in
-	Pmonad.make_raw_access ren env (id,id) c, 
-	(anonymous_pre true pre)::pl, Peffect.add_read id ef
-    | Apply (p,args) ->
-	let a,pl,e = effect pl p.desc in
-	let args,pl,e =
-	  List.fold_right
-	    (fun arg (l,pl,e) -> 
-	       match arg with
-		   Term p ->
-		     let carg,pl,earg = effect pl p.desc in
-		     carg::l,pl,Peffect.union e earg
-		 | Type v ->
-		     let v' = cic_type_v env ren v in
-		     (Pmonad.trad_ml_type_v ren env v')::l,pl,e
-		 | Refarg _ -> assert false) 
-	    args ([],pl,e) 
-	in
-	Term.applist (a,args),pl,e
-    | _ -> invalid_arg "Ptyping.states_expression"
-  in
-  let e0,pl0 = state_pre ren env expr.pre in
-  let c,pl,e = effect [] expr.desc in
-  let sign = Pcicenv.before_sign_of ren env in
-  (*i WAS
-  let c = (Trad.ise_resolve true empty_evd [] (gLOB sign) c)._VAL in
-  i*)
-  let ty = simplify_type_of (Global.env_of_context sign) Evd.empty c in
-  let v = TypePure ty in
-  let ef = Peffect.union e0 e in
-  Expression c, (v,ef), pl0@pl
-
-
-(* We infer here the type with effects.
- * The type of types with effects (ml_type_c) is defined in the module ProgAst.
- * 
- * A program of the shape {P} e {Q} has a type 
- *   
- *        V, E, {None|Some P}, {None|Some Q}
- *
- * where - V is the type of e
- *       - E = (I,O) is the effect; the input I contains
- *         all the input variables appearing in P,e and Q;
- *         the output O contains variables possibly modified in e
- *       - P is NOT abstracted
- *       - Q = [y'1]...[y'k][result]Q where O = {y'j}
- *         i.e. Q is only abstracted over the output and the result
- *         the other variables now refer to value BEFORE
- *)
-
-let verbose_fix = ref false
-
-let rec states_desc ren env loc = function
-	
-    Expression c ->
-      let ty = type_of_expression ren env c in
-      let v = v_of_constr ty in
-      Expression c, (v,Peffect.bottom)
-
-  | Acc _ ->
-      failwith "Ptyping.states: term is supposed not to be pure"
-
-  | Variable id ->
-      let v = type_in_env env id in
-      let ef = Peffect.bottom in
-      Variable id, (v,ef)
-
-  | Aff (x, e1) ->
-      Perror.check_for_reference loc x (type_in_env env x);
-      let s_e1 = states ren env e1 in
-      let _,e,_,_ = s_e1.info.kappa in
-      let ef = add_write x e in
-      let v = constant_unit () in
-      Aff (x, s_e1), (v, ef)
-
-  | TabAcc (check, x, e) ->
-      let s_e = states ren env e in
-      let _,efe,_,_ = s_e.info.kappa in
-      let ef = Peffect.add_read x efe in
-      let _,ty = dearray_type (type_in_env env x) in
-      TabAcc (check, x, s_e), (ty, ef)
-
-  | TabAff (check, x, e1, e2) ->
-      let s_e1 = states ren env e1 in
-      let s_e2 = states ren env e2 in 
-      let _,ef1,_,_ = s_e1.info.kappa in
-      let _,ef2,_,_ = s_e2.info.kappa in
-      let ef = Peffect.add_write x (Peffect.union ef1 ef2) in
-      let v = constant_unit () in
-      TabAff (check, x, s_e1, s_e2), (v,ef)
-
-  | Seq bl ->
-      let bl,v,ef,_ = states_block ren env bl in
-      Seq bl, (v,ef)
-	      
-  | While(b, invopt, var, bl) ->
-      let efphi,(cvar,r') = state_var ren env var in
-      let ren' = next ren [] in
-      let s_b = states ren' env b in
-      let s_bl,_,ef_bl,_ = states_block ren' env bl in
-      let cb = s_b.info.kappa in
-      let efinv,inv = state_inv ren env invopt in
-      let _,efb,_,_ = s_b.info.kappa in
-      let ef = 
-	Peffect.union (Peffect.union ef_bl efb) (Peffect.union efinv efphi)
-      in
-      let v = constant_unit () in
-      let cvar = 
-	let al = List.map (fun id -> (id,at_id id "")) (just_reads ef) in
-	subst_in_constr al cvar 
-      in
-      While (s_b,inv,(cvar,r'),s_bl), (v,ef)
-      
-  | Lam ([],_) ->
-      failwith "Ptyping.states: abs. should have almost one binder"
-
-  | Lam (bl, e) ->
-      let bl' = cic_binders env ren bl in
-      let env' = traverse_binders env bl' in
-      let ren' = initial_renaming env' in
-      let s_e = states ren' env' e in
-      let v = make_arrow bl' s_e.info.kappa in
-      let ef = Peffect.bottom in
-      Lam(bl',s_e), (v,ef)
-	 
-  (* Connectives AND and OR *)
-  | SApp ([Variable id], [e1;e2]) ->
-      let s_e1 = states ren env e1
-      and s_e2 = states ren env e2 in
-      let (_,ef1,_,_) = s_e1.info.kappa
-      and (_,ef2,_,_) = s_e2.info.kappa in
-      let ef = Peffect.union ef1 ef2 in
-      SApp ([Variable id], [s_e1; s_e2]), 
-      (TypePure (constant "bool"), ef)
-
-  (* Connective NOT *)
-  | SApp ([Variable id], [e]) ->
-      let s_e = states ren env e in
-      let (_,ef,_,_) = s_e.info.kappa in
-      SApp ([Variable id], [s_e]), 
-      (TypePure (constant "bool"), ef)
-      
-  | SApp _ -> invalid_arg "Ptyping.states (SApp)"
-
-  (* ATTENTION:
-     Si un argument réel de type ref. correspond à une ref. globale
-     modifiée par la fonction alors la traduction ne sera pas correcte.
-     Exemple:
-            f=[x:ref Int]( r := !r+1 ; x := !x+1) modifie r et son argument x
-            donc si on l'applique à r justement, elle ne modifiera que r
-            mais le séquencement ne sera pas correct. *)
-
-  | Apply (f, args) ->
-      let s_f = states ren env f in
-      let _,eff,_,_ = s_f.info.kappa in
-      let s_args = List.map (states_arg ren env) args in
-      let ef_args = 
-	List.map 
-	  (function Term t -> let (_,e,_,_) = t.info.kappa in e
-	          | _ -> Peffect.bottom) 
-	  s_args 
-      in
-      let _,_,((_,tapp),efapp,_,_) = effect_app ren env s_f s_args in
-      let ef = 
-	Peffect.compose (List.fold_left Peffect.compose eff ef_args) efapp
-      in
-      Apply (s_f, s_args), (tapp, ef)
-      
-  | LetRef (x, e1, e2) ->
-      let s_e1 = states ren env e1 in
-      let (_,v1),ef1,_,_ = s_e1.info.kappa in
-      let env' = add (x,Ref v1) env in
-      let ren' = next ren [x] in
-      let s_e2 = states ren' env' e2 in
-      let (_,v2),ef2,_,_ = s_e2.info.kappa in
-      Perror.check_for_let_ref loc v2;
-      let ef = Peffect.compose ef1 (Peffect.remove ef2 x) in
-      LetRef (x, s_e1, s_e2), (v2,ef)
-	
-  | Let (x, e1, e2) ->
-      let s_e1 = states ren env e1 in
-      let (_,v1),ef1,_,_ = s_e1.info.kappa in
-      Perror.check_for_not_mutable e1.loc v1;
-      let env' = add (x,v1) env in
-      let s_e2 = states ren env' e2 in
-      let (_,v2),ef2,_,_ = s_e2.info.kappa in
-      let ef = Peffect.compose ef1 ef2 in
-      Let (x, s_e1, s_e2), (v2,ef)
-	    
-  | If (b, e1, e2) ->
-      let s_b = states ren env b in
-      let s_e1 = states ren env e1
-      and s_e2 = states ren env e2 in
-      let (_,tb),efb,_,_ = s_b.info.kappa in
-      let (_,t1),ef1,_,_ = s_e1.info.kappa in
-      let (_,t2),ef2,_,_ = s_e2.info.kappa in
-      let ef = Peffect.compose efb (disj ef1 ef2) in
-      let v = type_v_sup loc t1 t2 in
-      If (s_b, s_e1, s_e2), (v,ef)
-
-  | LetRec (f,bl,v,var,e) ->
-      let bl' = cic_binders env ren bl in
-      let env' = traverse_binders env bl' in
-      let ren' = initial_renaming env' in
-      let v' = cic_type_v env' ren' v in
-      let efvar,var' = state_var ren' env' var in
-      let phi0 = phi_name () in
-      let tvar = typed_var ren env' var' in
-      (* effect for a let/rec construct is computed as a fixpoint *)
-      let rec state_rec c =
-	let tf = make_arrow bl' c in
-	let env'' = add_recursion (f,(phi0,tvar)) (add (f,tf) env') in
-	let s_e = states ren' env'' e in
-	if s_e.info.kappa = c then
-	  s_e
-      	else begin
-	  if !verbose_fix then begin msgnl (pp_type_c s_e.info.kappa) end ;
-	  state_rec s_e.info.kappa
-      	end
-      in 
-      let s_e = state_rec ((result_id,v'),efvar,[],None) in
-      let tf = make_arrow bl' s_e.info.kappa in
-      LetRec (f,bl',v',var',s_e), (tf,Peffect.bottom)
-
-  | PPoint (s,d) -> 
-      let ren' = push_date ren s in
-      states_desc ren' env loc d
-	
-  | Debug _ -> failwith "Ptyping.states: Debug: TODO"
-
-
-and states_arg ren env = function
-    Term a    -> let s_a = states ren env a in Term s_a
-  | Refarg id -> Refarg id
-  | Type v    -> let v' = cic_type_v env ren v in Type v'
-	
-
-and states ren env expr =
-  (* Here we deal with the pre- and post- conditions:
-   * we add their effects to the effects of the program *)
-  let (d,(v,e),p1) = 
-    if is_pure_desc ren env expr.desc then
-      states_expression ren env expr
-    else
-      let (d,ve) = states_desc ren env expr.loc expr.desc in (d,ve,[])
-  in
-  let (ep,p) = state_pre ren env expr.pre in
-  let (eq,q) = state_post ren env (result_id,v,e) expr.post in
-  let e' = Peffect.union e (Peffect.union ep eq) in
-  let p' = p1 @ p in
-  let tinfo = { env = env; kappa = ((result_id,v),e',p',q) } in
-  { desc = d;
-    loc = expr.loc;
-    pre = p'; post = q; (* on les conserve aussi ici pour prog_wp *)
-    info = tinfo }
-
-
-and states_block ren env bl =
-  let rec ef_block ren tyres = function
-      [] ->
-	begin match tyres with
-	    Some ty -> [],ty,Peffect.bottom,ren
-	  | None -> failwith "a block should contain at least one statement"
-	end
-    | (Assert p)::block -> 
-	let ep,c = state_assert ren env p in
-	let bl,t,ef,ren' = ef_block ren tyres block in
-	(Assert c)::bl,t,Peffect.union ep ef,ren'
-    | (Label s)::block ->
-	let ren' = push_date ren s in
-	let bl,t,ef,ren'' = ef_block ren' tyres block in
-	(Label s)::bl,t,ef,ren''
-    | (Statement e)::block ->
-	let s_e = states ren env e in
-	let (_,t),efe,_,_ = s_e.info.kappa in
-	let ren' = next ren (get_writes efe) in
-	let bl,t,ef,ren'' = ef_block ren' (Some t) block in
-	(Statement s_e)::bl,t,Peffect.compose efe ef,ren''
-  in
-  ef_block ren None bl
-
diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli
deleted file mode 100644
index 396a4aae4b..0000000000
--- a/contrib/correctness/ptyping.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Names
-open Term
-open Topconstr
-
-open Ptype
-open Past
-open Penv
-
-(* This module realizes type and effect inference *)
-
-val cic_type_v : local_env -> Prename.t -> constr_expr ml_type_v -> type_v
-
-val effect_app : Prename.t -> local_env
-            -> (typing_info,'b) Past.t
-            -> (typing_info,constr) arg list
-            -> (type_v binder list * type_c) 
-             * ((identifier*identifier) list * (identifier*constr) list * bool)
-             * type_c
-
-val typed_var : Prename.t -> local_env -> constr * constr -> variant
-
-val type_of_expression : Prename.t -> local_env -> constr -> constr
-
-val states : Prename.t -> local_env -> program -> typed_program
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
deleted file mode 100644
index e4bac65f4b..0000000000
--- a/contrib/correctness/putil.ml
+++ /dev/null
@@ -1,303 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Pattern
-open Matching
-open Hipattern
-open Environ
-
-open Pmisc
-open Ptype
-open Past
-open Penv
-open Prename
-
-let is_mutable = function Ref _ | Array _ -> true | _ -> false
-let is_pure = function TypePure _ -> true | _ -> false
-
-let named_app f x = { a_name = x.a_name; a_value = (f x.a_value) }
-
-let pre_app f x = 
-  { p_assert = x.p_assert; p_name = x.p_name; p_value = f x.p_value }
-
-let post_app = named_app
-
-let anonymous x = { a_name = Anonymous; a_value = x }
-
-let anonymous_pre b x = { p_assert = b; p_name = Anonymous; p_value = x }
-
-let force_name f x =
-  Option.map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x
-
-let force_post_name x = force_name post_name x
-
-let force_bool_name x = 
-  force_name (function Name id -> id | Anonymous -> bool_name()) x
-
-let out_post = function
-    Some { a_value = x } -> x
-  | None -> invalid_arg "out_post"
-
-let pre_of_assert b x =
-  { p_assert = b; p_name = x.a_name; p_value = x.a_value }
-
-let assert_of_pre x =
-  { a_name = x.p_name; a_value = x.p_value }
-
-(* Some generic functions on programs *)
-
-let is_mutable_in_env env id =
-  (is_in_env env id) & (is_mutable (type_in_env env id))
-
-let now_vars env c =
-  Util.map_succeed 
-    (function id -> if is_mutable_in_env env id then id else failwith "caught")
-    (global_vars (Global.env()) c)
-
-let make_before_after c =
-  let ids = global_vars (Global.env()) c in
-  let al = 
-    Util.map_succeed
-      (function id -> 
-	 if is_at id then 
-	   match un_at id with (uid,"") -> (id,uid) | _ -> failwith "caught"
-	 else failwith "caught")
-      ids
-  in
-  subst_in_constr al c
-
-(* [apply_pre] and [apply_post] instantiate pre- and post- conditions
- * according to a given renaming of variables (and a date that means
- * `before' in the case of the post-condition).
- *)
-
-let make_assoc_list ren env on_prime ids =
-  List.fold_left
-    (fun al id ->
-       if is_mutable_in_env env id then
-	 (id,current_var ren id)::al
-       else if is_at id then
-	 let uid,d = un_at id in
-	   if is_mutable_in_env env uid then
-	     (match d with
-		  "" -> (id,on_prime ren uid)
-		| _  -> (id,var_at_date ren d uid))::al
-	   else
-	     al
-       else
-	 al) 
-    [] ids
-
-let apply_pre ren env c =
-  let ids = global_vars (Global.env()) c.p_value in
-  let al = make_assoc_list ren env current_var ids in
-  { p_assert = c.p_assert; p_name = c.p_name; 
-    p_value = subst_in_constr al c.p_value }
-
-let apply_assert ren env c =
-  let ids = global_vars (Global.env()) c.a_value in
-  let al = make_assoc_list ren env current_var ids in
-  { a_name = c.a_name; a_value = subst_in_constr al c.a_value }
- 
-let apply_post ren env before c =
-  let ids = global_vars (Global.env()) c.a_value in
-  let al = 
-    make_assoc_list ren env (fun r uid -> var_at_date r before uid) ids in
-  { a_name = c.a_name; a_value = subst_in_constr al c.a_value }
-
-(* [traverse_binder ren env bl] updates renaming [ren] and environment [env]
- * as we cross the binders [bl]
- *)
-
-let rec traverse_binders env = function
-    [] -> env
-  | (id,BindType v)::rem ->
-      traverse_binders (add (id,v) env) rem
-  | (id,BindSet)::rem ->
-      traverse_binders (add_set id env) rem
-  | (_,Untyped)::_ ->
-      invalid_arg "traverse_binders"
-	  
-let initial_renaming env =
-  let ids = Penv.fold_all (fun (id,_) l -> id::l) env [] in
-    update empty_ren "0" ids
-
-
-(* Substitutions *)
-
-let rec type_c_subst s ((id,t),e,p,q) =
-  let s' = s @ List.map (fun (x,x') -> (at_id x "", at_id x' "")) s in
-  (id, type_v_subst s t), Peffect.subst s e,
-  List.map (pre_app (subst_in_constr s)) p,
-  Option.map (post_app (subst_in_constr s')) q
-
-and type_v_subst s = function
-    Ref v -> Ref (type_v_subst s v)
-  | Array (n,v) -> Array (n,type_v_subst s v)
-  | Arrow (bl,c) -> Arrow(List.map (binder_subst s) bl, type_c_subst s c)
-  | (TypePure _) as v -> v
-
-and binder_subst s = function
-    (n, BindType v) -> (n, BindType (type_v_subst s v))
-  | b -> b
-
-(* substitution of constr by others *)
-
-let rec type_c_rsubst s ((id,t),e,p,q) =
-  (id, type_v_rsubst s t), e,
-    List.map (pre_app (real_subst_in_constr s)) p,
-    Option.map (post_app (real_subst_in_constr s)) q
-
-and type_v_rsubst s = function
-    Ref v -> Ref (type_v_rsubst s v)
-  | Array (n,v) -> Array (real_subst_in_constr s n,type_v_rsubst s v)
-  | Arrow (bl,c) -> Arrow(List.map (binder_rsubst s) bl, type_c_rsubst s c)
-  | TypePure c -> TypePure (real_subst_in_constr s c)
-
-and binder_rsubst s = function
-  | (n, BindType v) -> (n, BindType (type_v_rsubst s v))
-  | b -> b
-
-(* make_arrow bl c = (x1:V1)...(xn:Vn)c *)
-
-let make_arrow bl c = match bl with
-  | [] -> invalid_arg "make_arrow: no binder"
-  | _ -> Arrow (bl,c)
-
-(* misc. functions *)
-
-let deref_type = function
-  | Ref v -> v
-  | _ -> invalid_arg "deref_type"
-
-let dearray_type = function
-  | Array (size,v) -> size,v
-  | _ -> invalid_arg "dearray_type"
-
-let constant_unit () = TypePure (constant "unit")
-
-let id_from_name = function Name id -> id | Anonymous -> (id_of_string "X")
-
-(* v_of_constr : traduit un type CCI en un type ML *)
-
-(* TODO: faire un test plus serieux sur le type des objets Coq *)
-let rec is_pure_cci c = match kind_of_term c with
-  | Cast (c,_) -> is_pure_cci c
-  | Prod(_,_,c') -> is_pure_cci c'
-  | Rel _ | Ind _ | Const _ -> true (* heu... *)
-  | App _ -> not (is_matching_sigma c)
-  | _ -> Util.error "CCI term not acceptable in programs"
-
-let rec v_of_constr c = match kind_of_term c with
-  | Cast (c,_) -> v_of_constr c
-  | Prod _ ->
-      let revbl,t2 = Term.decompose_prod c in
-      let bl =
-	List.map
-	  (fun (name,t1) -> (id_from_name name, BindType (v_of_constr t1)))
-	  (List.rev revbl)
-      in
-      let vars = List.rev (List.map (fun (id,_) -> mkVar id) bl) in
-      Arrow (bl, c_of_constr (substl vars t2))
-  | Ind _ | Const _ | App _ ->
-      TypePure c
-  | _ -> 
-      failwith "v_of_constr: TODO"
-
-and c_of_constr c =
-  if is_matching_sigma c then
-    let (a,q) = match_sigma c in
-    (result_id, v_of_constr a), Peffect.bottom, [], Some (anonymous q)
-  else
-    (result_id, v_of_constr c), Peffect.bottom, [], None
-
-
-(* pretty printers (for debugging purposes) *)
-
-open Pp
-open Util
-
-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 -> pr_lconstr x.p_value) l)
-
-let pp_post = function
-    None -> (mt ())
-  | 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 " ++ 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 -> 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 () ++ 
-	   Peffect.pp e ++ spc () ++ pp_pre p ++ spc () ++ pp_post q ++
-	   spc () ++ str"end")
-
-and pp_binder = function
-    id,BindType v -> (str"(" ++ pr_id id ++ str":" ++ pp_type_v v ++ str")")
-  | id,BindSet -> (str"(" ++ pr_id id ++ str":Set)")
-  | id,Untyped -> (str"(" ++ pr_id id ++ str")")
-
-(* pretty-print of cc-terms (intermediate terms) *)
-
-let rec pp_cc_term = function
-    CC_var id -> pr_id id
-  | CC_letin (_,_,bl,c,c1) ->
-      hov 0 (hov 2 (str"let " ++
-		  	prlist_with_sep (fun () -> (str","))
-			  (fun (id,_) -> pr_id id) bl ++
-		  	str" =" ++ spc () ++
-		  	pp_cc_term c ++
-		  	str " in") ++
-	       fnl () ++
-	       pp_cc_term c1)
-  | CC_lam (bl,c) ->
-      hov 2 (prlist (fun (id,_) -> (str"[" ++ pr_id id ++ str"]")) bl ++
-	       cut () ++
-	       pp_cc_term c)
-  | CC_app (f,args) ->
-      hov 2 (str"(" ++ 
-	       pp_cc_term f ++ spc () ++
-	       prlist_with_sep (fun () -> (spc ())) pp_cc_term args ++
-	       str")")
-  | CC_tuple (_,_,cl) ->
-      hov 2 (str"(" ++
-	       prlist_with_sep (fun () -> (str"," ++ cut ()))
-		 pp_cc_term cl ++
-	       str")")
-  | CC_case (_,b,[e1;e2]) ->
-      hov 0 (str"if " ++ pp_cc_term b ++ str" then" ++ fnl () ++
-	       str"  " ++ hov 0 (pp_cc_term e1) ++ fnl () ++
-	       str"else" ++ fnl () ++
-	       str"  " ++ hov 0 (pp_cc_term e2))
-  | CC_case _ ->
-      hov 0 (str"<Case: not yet implemented>")
-  | CC_expr c ->
-      hov 0 (pr_lconstr c)
-  | CC_hole c ->
-      (str"(?::" ++ pr_lconstr c ++ str")")
-
diff --git a/contrib/correctness/putil.mli b/contrib/correctness/putil.mli
deleted file mode 100644
index 02092c7806..0000000000
--- a/contrib/correctness/putil.mli
+++ /dev/null
@@ -1,72 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Pp
-open Names
-open Term
-open Pmisc
-open Ptype
-open Past
-open Penv
-
-val is_mutable : 'a ml_type_v -> bool
-val is_pure : 'a ml_type_v -> bool
-
-val named_app : ('a -> 'b) -> 'a assertion -> 'b assertion
-val pre_app : ('a -> 'b) -> 'a precondition -> 'b precondition
-val post_app : ('a -> 'b) -> 'a postcondition -> 'b postcondition
-
-val anonymous : 'a -> 'a assertion
-val anonymous_pre : bool -> 'a -> 'a precondition
-val out_post : 'a postcondition option -> 'a
-val pre_of_assert : bool -> 'a assertion -> 'a precondition
-val assert_of_pre : 'a precondition -> 'a assertion
-
-val force_post_name : 'a postcondition option -> 'a postcondition option
-val force_bool_name : 'a postcondition option -> 'a postcondition option
-
-val make_before_after : constr -> constr
-
-val traverse_binders : local_env -> (type_v binder) list -> local_env
-val initial_renaming : local_env -> Prename.t
-
-val apply_pre : Prename.t -> local_env -> constr precondition ->
-  constr precondition
-val apply_post : Prename.t -> local_env -> string -> constr postcondition ->
-  constr postcondition
-val apply_assert : Prename.t -> local_env -> constr assertion ->
-  constr assertion
-
-val type_v_subst : (identifier * identifier) list -> type_v -> type_v
-val type_c_subst : (identifier * identifier) list -> type_c -> type_c
-
-val type_v_rsubst : (identifier * constr) list -> type_v -> type_v
-val type_c_rsubst : (identifier * constr) list -> type_c -> type_c
-
-val make_arrow : ('a ml_type_v binder) list -> 'a ml_type_c -> 'a ml_type_v
-
-val is_mutable_in_env : local_env -> identifier -> bool
-val now_vars : local_env -> constr -> identifier list
-
-val deref_type : 'a ml_type_v -> 'a ml_type_v
-val dearray_type : 'a ml_type_v -> 'a * 'a ml_type_v
-val constant_unit : unit -> constr ml_type_v
-val v_of_constr : constr -> constr ml_type_v
-val c_of_constr : constr -> constr ml_type_c
-val is_pure_cci : constr -> bool
-
-(* pretty printers *)
-
-val pp_type_v : type_v -> std_ppcmds
-val pp_type_c : type_c -> std_ppcmds
-val pp_cc_term : cc_term -> std_ppcmds
-
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
deleted file mode 100644
index 258a461501..0000000000
--- a/contrib/correctness/pwp.ml
+++ /dev/null
@@ -1,347 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Util
-open Names
-open Libnames
-open Term
-open Termops
-open Environ
-open Nametab
-
-open Pmisc
-open Ptype
-open Past
-open Putil
-open Penv
-open Peffect
-open Ptyping
-open Prename
-
-(* In this module:
- *  - we try to insert more annotations to achieve a greater completeness;
- *  - we recursively propagate annotations inside programs;
- *  - we normalize boolean expressions.
- *
- * The propagation schemas are the following:
- * 
- *  1. (f a1 ... an)  ->  (f a1 ... an) {Qf} if the ai are functional
- *
- *  2. (if e1 then e2 else e3) {Q}  ->  (if e1 then e2 {Q} else e3 {Q}) {Q}
- * 
- *  3. (let x = e1 in e2) {Q}  ->  (let x = e1 in e2 {Q}) {Q}
- *)
-
-(* force a post-condition *)
-let update_post env top ef c =
-  let i,o = Peffect.get_repr ef in
-  let al = 
-    List.fold_left 
-      (fun l id -> 
-	 if is_mutable_in_env env id then
-	   if is_write ef id then l else (id,at_id id "")::l
-	 else if is_at id then
-	   let (uid,d) = un_at id in
-	   if is_mutable_in_env env uid & d="" then 
-	     (id,at_id uid top)::l 
-	   else 
-	     l
-	 else
-	   l) 
-      [] (global_vars (Global.env()) c)
-  in
-  subst_in_constr al c
-  
-let force_post up env top q e =
-  let (res,ef,p,_) = e.info.kappa in
-  let q' = 
-    if up then Option.map (named_app (update_post env top ef)) q else q 
-  in
-  let i = { env = e.info.env; kappa = (res,ef,p,q') } in
-  { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i }
-
-(* put a post-condition if none is present *)
-let post_if_none_up env top q = function
-  | { post = None } as p -> force_post true env top q p 
-  | p -> p
-
-let post_if_none env q = function
-  | { post = None } as p -> force_post false env "" q p 
-  | p -> p
-
-(* [annotation_candidate p] determines if p is a candidate for a 
- * post-condition *)
-
-let annotation_candidate = function
-  | { desc = If _ | Let _ | LetRef _ ; post = None } -> true
-  | _ -> false
-
-(* [extract_pre p] erase the pre-condition of p and returns it *)
-let extract_pre pr =
-  let (v,e,p,q) = pr.info.kappa in
-  { desc = pr.desc; pre = []; post = pr.post; loc = pr.loc;
-    info = { env = pr.info.env; kappa = (v,e,[],q) } },
-  p
-
-(* adds some pre-conditions *)
-let add_pre p1 pr =
-  let (v,e,p,q) = pr.info.kappa in
-  let p' = p1 @ p in
-  { desc = pr.desc; pre = p'; post = pr.post; loc = pr.loc;
-    info = { env = pr.info.env; kappa = (v,e,p',q) } }
-  
-(* change the statement *)
-let change_desc p d =
-  { desc = d; pre = p.pre; post = p.post; loc = p.loc; info = p.info }
-
-let create_bool_post c =
-  Some { a_value = c; a_name = Name (bool_name()) }
-
-(* [normalize_boolean b] checks if the boolean expression b (of type bool) is 
- * annotated, and if it is not the case tries to add the annotation
- * (if result then c=true else c=false) if b is an expression c.
- *)
-
-let is_bool = function
-  | TypePure c ->
-      (match kind_of_term (strip_outer_cast c) with
-	 | Ind op ->
-             string_of_id (id_of_global (IndRef op)) = "bool"
-	 | _ -> false)
-  | _ -> false
-
-let normalize_boolean ren env b =
-  let ((res,v),ef,p,q) = b.info.kappa in
-  Perror.check_no_effect b.loc ef;
-  if is_bool v then
-    match q with
-      | Some _ ->
-	  (* il y a une annotation : on se contente de lui forcer un nom *)
-	  let q = force_bool_name q in
-	  { desc = b.desc; pre = b.pre; post = q; loc = b.loc;
-	    info = { env = b.info.env; kappa = ((res,v),ef,p,q) } }
-      | None -> begin
-	  (* il n'y a pas d'annotation : on cherche à en mettre une *)
-	  match b.desc with
-	      Expression c ->
-	    	let c' = Term.applist (constant "annot_bool",[c]) in
-		let ty = type_of_expression ren env c' in
-		let (_,q') = Hipattern.match_sigma ty in
-		let q' = Some { a_value = q'; a_name = Name (bool_name()) } in
-		{ desc = Expression c'; 
-		  pre = b.pre; post = q'; loc = b.loc;
-		  info = { env = b.info.env; kappa = ((res, v),ef,p,q') } }
-	    | _ -> b
-	end
-  else
-    Perror.should_be_boolean b.loc
-
-(* [decomp_boolean c] returns the specs R and S of a boolean expression *)
-
-let decomp_boolean = function
-  | Some { a_value = q } ->
-      Reductionops.whd_betaiota (Term.applist (q, [constant "true"])),
-      Reductionops.whd_betaiota (Term.applist (q, [constant "false"]))
-  | _ -> invalid_arg "Ptyping.decomp_boolean"
-
-(* top point of a program *)
-
-let top_point = function
-  | PPoint (s,_) as p -> s,p
-  | p -> let s = label_name() in s,PPoint(s,p)
-
-let top_point_block = function
-  | (Label s :: _) as b -> s,b
-  | b -> let s = label_name() in s,(Label s)::b
-
-let abstract_unit q = abstract [result_id,constant "unit"] q
-
-(* [add_decreasing env ren ren' phi r bl] adds the decreasing condition
- *    phi(ren') r phi(ren)
- * to the last assertion of the block [bl], which is created if needed
- *)
-
-let add_decreasing env inv (var,r) lab bl =
-  let ids = now_vars env var in
-  let al = List.map (fun id -> (id,at_id id lab)) ids in
-  let var_lab = subst_in_constr al var in
-  let dec = Term.applist (r, [var;var_lab]) in
-  let post = match inv with
-      None -> anonymous dec
-    | Some i -> { a_value = conj dec i.a_value; a_name = i.a_name }
-  in
-  bl @ [ Assert post ]
-
-(* [post_last_statement env top q bl] annotates the last statement of the
- * sequence bl with q if necessary *)
-
-let post_last_statement env top q bl =
-  match List.rev bl with
-    | Statement e :: rem when annotation_candidate e -> 
-	List.rev ((Statement (post_if_none_up env top q e)) :: rem)
-    | _ -> bl
-
-(* [propagate_desc] moves the annotations inside the program 
- * info is the typing information coming from the outside annotations *)
-let rec propagate_desc ren info d = 
-  let env = info.env in
-  let (_,_,p,q) = info.kappa in
-  match d with
-    | If (e1,e2,e3) ->
-      (* propagation number 2 *)
-	let e1' = normalize_boolean ren env (propagate ren e1) in
-	if e2.post = None or e3.post = None then
-	  let top = label_name() in
-	  let ren' = push_date ren top in
-	  PPoint (top, If (e1', 
-			   propagate ren' (post_if_none_up env top q e2),
-			   propagate ren' (post_if_none_up env top q e3)))
-	else
-	  If (e1', propagate ren e2, propagate ren e3)
-    | Aff (x,e) ->
-      	Aff (x, propagate ren e)
-    | TabAcc (ch,x,e) ->
-      	TabAcc (ch, x, propagate ren e)
-    | TabAff (ch,x,({desc=Expression c} as e1),e2) ->
-	let p = Pmonad.make_pre_access ren env x c in
-	let e1' = add_pre [(anonymous_pre true p)] e1 in
-      	TabAff (false, x, propagate ren e1', propagate ren e2)
-    | TabAff (ch,x,e1,e2) ->
-      	TabAff (ch, x, propagate ren e1, propagate ren e2)
-    | Apply (f,l) ->
-      	Apply (propagate ren f, List.map (propagate_arg ren) l)
-    | SApp (f,l) ->
-	let l = 
-	  List.map (fun e -> normalize_boolean ren env (propagate ren e)) l
-	in
-      	SApp (f, l)
-    | Lam (bl,e) ->
-      	Lam (bl, propagate ren e)
-    | Seq bl ->
-	let top,bl = top_point_block bl in
-	let bl = post_last_statement env top q bl in
-      	Seq (propagate_block ren env bl)
-    | While (b,inv,var,bl) ->
-	let b = normalize_boolean ren env (propagate ren b) in
-	let lab,bl = top_point_block bl in
-	let bl = add_decreasing env inv var lab bl in
-      	While (b,inv,var,propagate_block ren env bl)
-    | LetRef (x,e1,e2) ->
-	let top = label_name() in
-	let ren' = push_date ren top in
-	PPoint (top, LetRef (x, propagate ren' e1, 
-	      		     propagate ren' (post_if_none_up env top q e2)))
-    | Let (x,e1,e2) ->
-	let top = label_name() in
-	let ren' = push_date ren top in
-      	PPoint (top, Let (x, propagate ren' e1, 
-			    propagate ren' (post_if_none_up env top q e2)))
-    | LetRec (f,bl,v,var,e) ->
-      	LetRec (f, bl, v, var, propagate ren e)
-    | PPoint (s,d) -> 
-      	PPoint (s, propagate_desc ren info d)
-    | Debug _ | Variable _ 
-    | Acc _ | Expression _ as d -> d
-	  
-
-(* [propagate] adds new annotations if possible *)
-and propagate ren p =
-  let env = p.info.env in
-  let p = match p.desc with
-    | Apply (f,l) ->
-	let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in
-	if ok then
-	  let q = Option.map (named_app (real_subst_in_constr so)) qapp in
-	  post_if_none env q p
-	else
-	  p
-    | _ -> p
-  in
-  let d = propagate_desc ren p.info p.desc in
-  let p = change_desc p d in
-  match d with
-    | Aff (x,e) ->
-	let e1,p1 = extract_pre e in
-	change_desc (add_pre p1 p) (Aff (x,e1))
-
-    | TabAff (check, x, ({ desc = Expression _ } as e1), e2) ->
-	let e1',p1 = extract_pre e1 in
-	let e2',p2 = extract_pre e2 in
-	change_desc (add_pre (p1@p2) p) (TabAff (check,x,e1',e2'))
-
-    | While (b,inv,_,_) ->
-	let _,s = decomp_boolean b.post in
-	let s = make_before_after s in
-	let q = match inv with
-	    None -> Some (anonymous s)
-	  | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name }
-	in
-	let q = Option.map (named_app abstract_unit) q in
-	post_if_none env q p
-
-    | SApp ([Variable id], [e1;e2]) 
-      when id = connective_and or id = connective_or ->
-	let (_,_,_,q1) = e1.info.kappa
-	and (_,_,_,q2) = e2.info.kappa in
-	let (r1,s1) = decomp_boolean q1
-	and (r2,s2) = decomp_boolean q2 in
-	let q =
-	  let conn = if id = connective_and then "spec_and" else "spec_or" in
-	  let c = Term.applist (constant conn, [r1; s1; r2; s2]) in
-	  let c = Reduction.whd_betadeltaiota (Global.env()) c in
-	  create_bool_post c
-	in
-	let d = 
-	  SApp ([Variable id;
-                 Expression (out_post q1);
-                 Expression (out_post q2)], 
-		[e1; e2] ) 
-	in
-	post_if_none env q (change_desc p d)
-
-    | SApp ([Variable id], [e1]) when id = connective_not ->
-	let (_,_,_,q1) = e1.info.kappa in
-	let (r1,s1) = decomp_boolean q1 in
-	let q = 
-	  let c = Term.applist (constant "spec_not", [r1; s1]) in
-	  let c = Reduction.whd_betadeltaiota (Global.env ()) c in
-	  create_bool_post c 
-	in
-	let d = SApp ([Variable id; Expression (out_post q1)], [ e1 ]) in
-	post_if_none env q (change_desc p d)
-
-    | _ -> p
-
-and propagate_arg ren = function
-  | Type _ | Refarg _ as a -> a
-  | Term e -> Term (propagate ren e)
-
-
-and propagate_block ren env = function 
-  | [] -> 
-      []
-  | (Statement p) :: (Assert q) :: rem when annotation_candidate p ->
-      (* TODO: plutot p.post = None ? *)
-      let q' =
-	let ((id,v),_,_,_) = p.info.kappa in
-	let tv = Pmonad.trad_ml_type_v ren env v in
-	named_app (abstract [id,tv]) q
-      in
-      let p' = post_if_none env (Some q') p in
-      (Statement (propagate ren p')) :: (Assert q) 
-      :: (propagate_block ren env rem)
-  | (Statement p) :: rem ->
-      (Statement (propagate ren p)) :: (propagate_block ren env rem)
-  | (Label s as x) :: rem ->
-      x :: propagate_block (push_date ren s) env rem
-  | x :: rem ->
-      x :: propagate_block ren env rem
diff --git a/contrib/correctness/pwp.mli b/contrib/correctness/pwp.mli
deleted file mode 100644
index 7b6440c63e..0000000000
--- a/contrib/correctness/pwp.mli
+++ /dev/null
@@ -1,18 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \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$ *)
-
-open Term
-open Penv
-
-val update_post : local_env -> string -> Peffect.t -> constr -> constr
-
-val propagate : Prename.t -> typed_program -> typed_program