branchement extraction (bytecode seulement)

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

20 files changed, 421 insertions, 404 deletions

diff --git a/contrib/correctness/Programs.v b/contrib/correctness/Correctness.v
index 34d843908..7dc283f7a 100644
--- a/contrib/correctness/Programs.v
+++ b/contrib/correctness/Correctness.v
@@ -23,11 +23,9 @@ Require Export ProgWf.
 Require Export Arrays.
 
 Declare ML Module
-    "misc_utils" "effects" "renamings" "progTypes" "progAst"
-    "prog_errors" "prog_env" "prog_utils"
-    "prog_db" "prog_cci" "monad" "tradEnv"
-    "prog_red" "prog_typing" "prog_wp" "mlise" "prog_tactic"
-    "pprog".
+    "pmisc" "peffect" "prename" "ptype" "past"
+    "perror" "penv" "putil" "pdb" "pcic" "pmonad" "pcicenv"
+    "pred" "ptyping" "pwp" "pmlize" "ptactic" "psyntax".
 
 Token "'".
 
diff --git a/contrib/correctness/past.ml b/contrib/correctness/past.ml
index 5dd0301eb..612097612 100644
--- a/contrib/correctness/past.ml
+++ b/contrib/correctness/past.ml
@@ -100,18 +100,18 @@ type cc_binder = variable * cc_bind_type
 
 type cc_term =
     CC_var   of variable
-  | CC_letin of bool                (* dep. or not *)
-              * cc_type             (* type of result *)
+  | CC_letin of bool                   (* dep. or not *)
+              * cc_type                (* type of result *)
 	      * cc_binder list
-	      * (cc_term * constr)  (* the matched term and its ind. type *)
+	      * (cc_term * case_info)  (* the matched term and its ind. type *)
 	      * cc_term
   | CC_lam   of cc_binder list * cc_term
   | CC_app   of cc_term * cc_term list
-  | CC_tuple of bool                (* dep. or not *)
+  | CC_tuple of bool                   (* dep. or not *)
               * cc_type list * cc_term list
-  | CC_case  of cc_type             (* type of result *)
-              * (cc_term * constr)  (* the test and its inductive type *)
-	      * cc_term list        (* branches *)
+  | CC_case  of cc_type                (* type of result *)
+              * (cc_term * case_info)  (* the test and its inductive type *)
+	      * cc_term list           (* branches *)
   | CC_expr  of constr
   | CC_hole  of cc_type
 
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 36022f208..d674f7d10 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -64,11 +64,11 @@ 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 * Term.constr) *
-                  cc_term
+  | CC_letin of 
+      bool * cc_type * cc_binder list * (cc_term * Term.case_info) * 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 * Term.constr) * cc_term list
+  | CC_case of cc_type * (cc_term * Term.case_info) * 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
index 4c0d08732..49871b23a 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -12,6 +12,7 @@
 
 open Names
 open Term
+open Declarations
 
 open Pmisc
 open Past
@@ -51,42 +52,41 @@ let tuple_n n =
   let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
   Record.definition_structure (false, 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 name = "sig_" ^ string_of_int n in
   let id = id_of_string name in
   let l1n = Util.interval 1 n in
-  let lT = 
-    List.map (fun i -> id_of_string ("T" ^ string_of_int i)) l1n in
-  let lx = 
-    List.map (fun i -> id_of_string ("x" ^ string_of_int i)) l1n in
-  let ty_p = List.fold_right (fun ti c -> mkArrow (mkVar ti) c) lT mkProp in
-  let arity = 
-    let ar = 
-      List.fold_right (fun ti c -> mkNamedProd ti mkSet c) lT
-	(mkArrow ty_p mkSet) in
-    mkCast (ar, mkType Univ.prop_univ) 
-  in
+  let lT = List.map (fun i -> id_of_string ("T" ^ string_of_int i)) l1n in
+  let lx = List.map (fun i -> id_of_string ("x" ^ string_of_int i)) l1n in
   let idp = id_of_string "P" 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 = 
-      let l = 
-	(mkRel (2*n+3)) :: (List.map (fun id -> (mkVar id)) lT) @ [mkVar idp] 
-      in
-      mkAppA (Array.of_list l) in
-    let app_p = 
-      let l = (mkVar idp) :: (List.map (fun id -> mkVar id) lx) in
-      mkAppA (Array.of_list l) in
+    let app_sig = mkAppA (Array.init (n+2) (fun i -> mkRel (2*n+3-i))) in
+    let app_p = mkAppA (Array.init (n+1) (fun i -> mkRel (n+1-i))) in
     let c = mkArrow app_p app_sig in
-    let c = List.fold_right (fun (x,tx) c -> mkNamedProd x (mkVar tx) c)
-	      (List.combine lx lT) c in
-    let c = mkNamedProd idp ty_p c in
-    let c = List.fold_right (fun ti c -> mkNamedProd ti mkSet c) lT c in
-    DLAMV (Name id, [| c |])
+    List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c
   in
   let cname = id_of_string ("exist_" ^ string_of_int n) in
-  Declare.machine_minductive (Termenv.initial_assumptions()) (succ n)
-    [| id, Anonymous, arity, lc, [| cname |] |] true
-
+  Declare.declare_mind 
+    { mind_entry_finite = true;
+      mind_entry_inds = 
+	[ { mind_entry_nparams = succ n;
+	    mind_entry_params = params;
+	    mind_entry_typename = id;
+	    mind_entry_arity = mkSet;
+	    mind_entry_consnames = [ cname ];
+	    mind_entry_lc = [ lc ] } ] }
+	
 let tuple_name dep n =
   if n = 2 & not dep then
     "pair"
@@ -97,7 +97,7 @@ let tuple_name dep n =
 	"exist" 
       else begin
 	let name = Printf.sprintf "exist_%d" n in
-	if not (tuple_exists (id_of_string name)) then sig_n n;
+	if not (tuple_exists (id_of_string name)) then ignore (sig_n n);
 	name
       end
     else begin
@@ -121,7 +121,7 @@ let lambda_of_bl bl c =
 
 let constr_of_prog p =
   let rec trad = function
-      CC_var id -> VAR id
+    | CC_var id -> mkVar id
 
     (* optimisation : let x = <constr> in e2  =>  e2[x<-constr] *)
     | CC_letin (_,_,[id,_],(CC_expr c,_),e2) ->
@@ -129,13 +129,13 @@ let constr_of_prog p =
 
     | CC_letin (_,_,([_] as b),(e1,_),e2) ->
       	let c = trad e1 and c2 = trad e2 in
-	  Term.applist (lambda_of_bl b c2, [c])
+	Term.applist (lambda_of_bl b c2, [c])
 
     | CC_letin (dep,ty,bl,(e,info),e1) ->
-      let c1 = trad e1
-      and c = trad e in
-      let l = [ lambda_of_bl bl c1 ] in
-	Term.mkMutCase (Term.ci_of_mind info) ty c l
+	let c1 = trad e1
+	and c = trad e in
+	let l = [| lambda_of_bl bl c1 |] in
+	Term.mkMutCase (info, ty, c, l)
 
     | CC_lam (bl,e) ->
 	let c = trad e in lambda_of_bl bl c
@@ -143,31 +143,30 @@ let constr_of_prog p =
     | CC_app (f,args) ->
 	let c = trad f
 	and cargs = List.map trad args in
-	  Term.applist (c,cargs)
+	Term.applist (c,cargs)
 
     | CC_tuple (_,_,[e]) -> trad e
 	
     | CC_tuple (false,_,[e1;e2]) ->
 	let c1 = trad e1 
 	and c2 = trad e2 in
-	  Term.applist (constant "pair", [isevar;isevar;c1;c2])
+	Term.applist (constant "pair", [isevar;isevar;c1;c2])
 
     | CC_tuple (dep,tyl,l) ->
       	let n = List.length l in
       	let cl = List.map trad l in
       	let name = tuple_name dep n in
       	let args = tyl @ cl in
-	  Term.applist (constant name,args)
+	Term.applist (constant name,args)
 
     | CC_case (ty,(b,info),el) ->
-      let c = trad b in
-      let cl = List.map trad el in
-	mkMutCase (Term.ci_of_mind info) ty c cl
+	let c = trad b in
+	let cl = List.map trad el in
+	mkMutCase (info, ty, c, Array.of_list cl)
 
     | CC_expr c -> c
 
     | CC_hole c -> make_hole c
 
   in
-    trad p
-  
+  trad p
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
index 046fa7f72..eecc5eb2f 100644
--- a/contrib/correctness/pcicenv.ml
+++ b/contrib/correctness/pcicenv.ml
@@ -12,6 +12,7 @@
 
 open Names
 open Term
+open Sign
 
 open Pmisc
 open Putil
@@ -21,30 +22,35 @@ 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 =
+  let t' = lookup_id_type id s in
+  map_named_context (fun t'' -> if t'' == t' then t else t'') s
+
 let add_sign (id,t) s =
-  if mem_sign s id then
+  if mem_named_context id s then
     modify_sign id t s
   else
-    add_sign (id,t) s
+    add_named_assum (id,t) s
 
-let cast_set c = make_type c mk_Set
+let cast_set c = mkCast (c, mkSet)
 
-let set = make_type Term.mkSet (Term.Type Impuniv.prop_univ)
+let set = mkCast (mkSet, mkType Univ.prop_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 =
-   Prog_env.fold_all 
+   Penv.fold_all 
     (fun (id,v) sign ->
        match v with
-	   Prog_env.TypeV (Ref _ | Array _) -> sign
-	 | Prog_env.TypeV v -> 
-	     let ty = Monad.trad_ml_type_v ren env v in
-	       add_sign (id,cast_set ty) sign
-	 | Prog_env.Set -> add_sign (id,set) sign)
-    env (initial_sign())
+	 | 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
@@ -56,16 +62,16 @@ let cci_sign_of ren env =
  *)
 
 let sign_meta ren env fast ini =
-   Prog_env.fold_all 
+   Penv.fold_all 
     (fun (id,v) sign ->
        match v with
-	   Prog_env.TypeV (Ref _ | Array _ as v) -> 
-	     let ty = Monad.trad_imp_type ren env v in
-	       fast sign id ty
-	 | Prog_env.TypeV v -> 
-	     let ty = Monad.trad_ml_type_v ren env v in
-	       add_sign (id,cast_set ty) sign
-	 | Prog_env.Set -> add_sign (id,set) sign)
+	 | 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 =
@@ -77,22 +83,22 @@ let add_sign_d dates (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)
-    (initial_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 = "" :: Renamings.all_dates ren in
+  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 = "" :: Renamings.all_dates ren in
+  let dates = "" :: Prename.all_dates ren in
   sign_of (add_sign_d dates) ren
 
 let before_sign_of ren =
-  let dates = Renamings.all_dates ren in
+  let dates = Prename.all_dates ren in
   sign_of (add_sign_d dates) ren
 
 let now_sign_of =
@@ -103,7 +109,7 @@ let now_sign_of =
 
 let trad_sign_of ren =
   sign_of
-    (fun (id,c) sign -> add_sign (Renamings.current_var ren id,c) sign)
+    (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
index e0bfd386b..682bc6d40 100644
--- a/contrib/correctness/pcicenv.mli
+++ b/contrib/correctness/pcicenv.mli
@@ -13,25 +13,26 @@
 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 : Renamings.t -> local_env -> context
+val cci_sign_of : Prename.t -> local_env -> named_context
 
 (* env. Coq avec seulement les variables X de l'env. *)
-val now_sign_of : Renamings.t -> local_env -> context
+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 : Renamings.t -> local_env -> context
+val before_sign_of : Prename.t -> local_env -> named_context
 
 (* + les variables `avant' X@ *)
-val before_after_sign_of : Renamings.t -> local_env -> context
+val before_after_sign_of : Prename.t -> local_env -> named_context
 val before_after_result_sign_of : ((identifier * constr) option)
-                        -> Renamings.t -> local_env -> context
+                        -> Prename.t -> local_env -> named_context
 
 (* env. des programmes traduits, avec les variables rennomées *)
-val trad_sign_of : Renamings.t -> local_env -> context
+val trad_sign_of : Prename.t -> local_env -> named_context
 
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 125924fb2..06090fb07 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -11,15 +11,15 @@
 (* $Id$ *)
 
 open Names
+open Term
 
 open Ptype
 open Past
 open Penv
 
-
 let cci_global id =
   try
-    Machops.global (gLOB(initial_sign())) id
+    Declare.global_reference CCI id
   with
     _ -> raise Not_found
 
@@ -28,12 +28,12 @@ let lookup_var ids locop id =
     None
   else begin
     try Some (cci_global id)
-    with Not_found -> Prog_errors.unbound_variable id locop
+    with Not_found -> Perror.unbound_variable id locop
   end
 
 let check_ref idl loc id =
-  if (not (List.mem id idl)) & (not (Prog_env.is_global id)) then
-    Prog_errors.unbound_reference id (Some loc)
+  if (not (List.mem id idl)) & (not (Penv.is_global id)) then
+    Perror.unbound_reference id (Some loc)
 
 (* db types  : just do nothing for the moment ! *)
 
@@ -69,12 +69,11 @@ let rec db_binders ((tids,pids,refs) as idl) = function
 (* db patterns *)
 
 let rec db_pattern = function
-    (PatVar id) as t ->
+  | (PatVar id) as t ->
       (try 
-	 let sp = Nametab.fw_sp_of_id id in
-	 (match Environ.global_operator sp id with
-	      Term.MutConstruct (x,y),_ -> [], PatConstruct (id,(x,y))
-	    | _                         -> [id],t)
+	 (match Nametab.sp_of_id CCI id with
+	    | ConstructRef (x,y) -> [], PatConstruct (id,(x,y))
+	    | _                  -> [id],t)
        with Not_found -> [id],t)
   | PatAlias (p,id) ->
       let ids,p' = db_pattern p in ids,PatAlias (p',id)
@@ -159,7 +158,7 @@ let db_prog e =
       loc = e.loc; info = e.info }
 
   in
-  let ids = Names.ids_of_sign (Vartab.initial_sign()) in
+  let ids = Sign.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
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index fe37f8308..31a2bad38 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -115,7 +115,6 @@ let (inProg,outProg) =
                     cache_function = cache_global;
                     open_function = (fun _ -> ());
 		    export_function = (fun x -> Some x) })
-;;
 
 let add_global id v p =
   try
@@ -125,16 +124,17 @@ let add_global id v p =
     Not_found -> begin
       let id' =
 	if is_mutable v then id 
-        else id_of_string ("prog_" ^ (string_of_id id)) in
-	add_named_object (id',OBJ) (inProg (id,TypeV v,p))
+        else id_of_string ("prog_" ^ (string_of_id id)) 
+      in
+      Lib.add_leaf id' OBJ (inProg (id,TypeV v,p))
     end
 
 let add_global_set id =
   try
     let _ = Env.find id !env in
-    Prog_errors.clash id None
+    Perror.clash id None
   with
-    Not_found -> add_named_object (id,OBJ) (inProg (id,Set,None))
+    Not_found -> Lib.add_leaf id OBJ (inProg (id,Set,None))
 
 let is_global id =
   try
@@ -152,7 +152,7 @@ let is_global_set id =
 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 find_pgm id = Idmap.find id !pgm_table
 
 let all_vars () =
   Env.fold
@@ -167,17 +167,18 @@ let all_refs () =
 (* initializations *)
 
 let cache_init (_,(id,c)) =
-  init_table := IdMap.add id c !init_table
+  init_table := Idmap.add id c !init_table
 
 let (inInit,outInit) =
   declare_object ("programs-objects-init",
-                  { load_function = (fun _ -> ());
+                  { load_function = cache_init;
+		    open_function = (fun _ -> ());
                     cache_function = cache_init;
-                    specification_function = fun x -> x})
+                    export_function = fun x -> Some x })
 
-let initialize id c = add_anonymous_object (inInit (id,c))
+let initialize id c = Lib.add_anonymous_leaf (inInit (id,c))
 
-let find_init id = IdMap.find id !init_table
+let find_init id = Idmap.find id !init_table
 
 
 (* access in env, local then global *)
@@ -206,19 +207,19 @@ let find_recursion = Env.find_rec
 open Pp
 open Himsg
 
-let (edited : (type_v * typed_program) IdMap.t ref) = ref IdMap.empty
+let (edited : (type_v * typed_program) Idmap.t ref) = ref Idmap.empty
 
 let new_edited id v =
-  edited := IdMap.add id v !edited
+  edited := Idmap.add id v !edited
 
 let is_edited id =
-  try let _ = IdMap.find id !edited in true with Not_found -> false
+  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
-      add_global id' v (Some p);
-      mSGNL (hOV 0 [< 'sTR"Program "; pID id'; 'sPC; 'sTR"is defined" >]);
-      edited := IdMap.remove id !edited
+    let (v,p) = Idmap.find id !edited in
+    let _ = add_global id' v (Some p) in
+    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
index c6962b5f4..83ac2d91a 100644
--- a/contrib/correctness/penv.mli
+++ b/contrib/correctness/penv.mli
@@ -45,8 +45,8 @@ type typed_program = (typing_info, constr) t
 
 (* global environment *)
 
-val add_global : identifier -> type_v -> typed_program option -> unit
-val add_global_set : identifier -> unit
+val add_global : identifier -> type_v -> typed_program option -> section_path
+val add_global_set : identifier -> section_path
 val is_global : identifier -> bool
 val is_global_set : identifier -> bool
 val lookup_global : identifier -> type_v
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 251471082..0435095fa 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -22,42 +22,42 @@ open Past
 
 
 let raise_with_loc = function
-    None -> raise
+  | None -> raise
   | Some loc -> Stdpp.raise_with_loc loc 
 
 let unbound_variable id loc =
   raise_with_loc loc
-    (UserError ("Prog_errors.unbound_variable",
+    (UserError ("Perror.unbound_variable",
     (hOV 0 [<'sTR"Unbound variable"; 'sPC; pr_id id; 'fNL >])))
 
 let unbound_reference id loc =
   raise_with_loc loc
-    (UserError ("Prog_errors.unbound_reference",
+    (UserError ("Perror.unbound_reference",
     (hOV 0 [<'sTR"Unbound reference"; 'sPC; pr_id id; 'fNL >])))
 
 let clash id loc =
   raise_with_loc loc
-    (UserError ("Prog_errors.clash",
+    (UserError ("Perror.clash",
     (hOV 0 [< 'sTR"Clash with previous constant"; 'sPC;
     'sTR(string_of_id id); 'fNL >])))
 
 let not_defined id =
   raise
-    (UserError ("Prog_errors.not_defined",
+    (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 ("Prog_errors.check_for_reference",
+	(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 ("Prog_errors.check_for_array",
+	(UserError ("Perror.check_for_array",
 		    hOV 0 [< pr_id id; 'sPC; 
 			     'sTR"is not an array" >]))
 
@@ -72,56 +72,56 @@ 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 ("Prog_errors.check_for_index",
+      (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 ("Prog_errors.check_no_effect",
+      (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 ("Prog_errors.should_be_boolean",
+    (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 ("Prog_errors.test_should_be_annotated",
+    (UserError ("Perror.test_should_be_annotated",
 		hOV 0 [< 'sTR"This test should be annotated" >]))
 
 let if_branches loc =
   Stdpp.raise_with_loc loc 
-    (UserError ("Prog_errors.if_branches",
+    (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 ("Prog_errors.check_for_not_mutable",
+      (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 ("Prog_errors.check_for_pure_type",
+      (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 ("Prog_errors.check_for_let_ref",
+      (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 ("Prog_errors.variant_informative",
+  (UserError ("Perror.variant_informative",
 	      hOV 0 [< 'sTR s; 'sPC; 'sTR"must be informative" >]))
 
 let variant_informative loc = informative loc "Variant"
@@ -129,42 +129,42 @@ let should_be_informative loc = informative loc "This term"
 
 let app_of_non_function loc =
   Stdpp.raise_with_loc loc 
-  (UserError ("Prog_errors.app_of_non_function",
+  (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 ("Prog_errors.partial_app",
+  (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 ("Prog_errors.expected_type",
+  (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 ("Prog_errors.expects_a_type",
+  (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 ("Prog_errors.expects_a_type",
+  (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 ("Prog_errors.should_be_a_variable",
+  (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 ("Prog_errors.should_be_a_reference",
+  (UserError ("Perror.should_be_a_reference",
 	      hOV 0 [< 'sTR"Argument of function should be a reference" >]))
 
    
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
index e81432c5f..28d805331 100644
--- a/contrib/correctness/pmlize.ml
+++ b/contrib/correctness/pmlize.ml
@@ -26,13 +26,10 @@ open Ptyping
 open Pmonad
 
 
-let mmk = make_module_marker [ "#Specif.obj" ]
-let sig_pattern = put_pat mmk "(sig ? ?)"
-
 let has_proof_part ren env c =
-  let sign = TradEnv.trad_sign_of ren env in
-  let ty = Mach.type_of (Evd.mt_evd()) sign c in
-  somatches ty sig_pattern
+  let sign = Pcicenv.trad_sign_of ren env in
+  let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in
+  is_matching (Coqlib.build_coq_sig_pattern ()) ty
 
 (* main part: translation of imperative programs into functional ones.
  * 
@@ -80,12 +77,14 @@ and trad_desc ren env ct d =
       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) (VAR id) 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 (VAR id) in 
+	  let h = make_pre_access ren env x (mkVar id) in 
 	  let_in_pre ty (anonymous_pre true h) t
 	else
 	  t 
@@ -120,15 +119,15 @@ and trad_desc ren env ct d =
       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) (VAR id1)
-		   (VAR id2) 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 (VAR id1) in
+	  let h = make_pre_access ren' env x (mkVar id1) in
 	  let_in_pre ty (anonymous_pre true h) t
 	else
 	  t 
@@ -211,12 +210,12 @@ and trad_desc ren env ct d =
       let tc_args =
 	List.combine
 	  (List.rev targs)
-	  (Std.map_succeed
+	  (Util.map_succeed
 	     (function
-		  Term x -> x.info.kappa
+		| Term x -> x.info.kappa
 		| Refarg _ -> failwith "caught"
 		| Type _ -> 
-		    (result_id,TypePure mkSet),Effects.bottom,[],None)
+		    (result_id,TypePure mkSet),Peffect.bottom,[],None)
 	     args)
       in
       make_app env ren tc_args ren' (tf,cf) (c,s,capp) ct
@@ -287,7 +286,7 @@ and trad_binders ren env = function
       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 (DOP0(Sort(Prop Pos)))) :: (trad_binders ren env bl)
+      (id, CC_typed_binder mkSet) :: (trad_binders ren env bl)
   | (_,Untyped)::_ -> invalid_arg "trad_binders"
 
 	
diff --git a/contrib/correctness/pmlize.mli b/contrib/correctness/pmlize.mli
index 964b4327c..473edd24c 100644
--- a/contrib/correctness/pmlize.mli
+++ b/contrib/correctness/pmlize.mli
@@ -16,5 +16,5 @@ open Names
 
 (* translation of imperative programs into intermediate functional programs *)
 
-val trans : Renamings.t -> typed_program -> cc_term
+val trans : Prename.t -> typed_program -> cc_term
 
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 92b904bc1..30892ee4c 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -74,7 +74,7 @@ let arrow ren env v pl =
 
 let rec abstract_post ren env (e,q) =
   let after_id id = id_of_string ((string_of_id id) ^ "'") in
-  let (_,go) = Effects.get_repr e in
+  let (_,go) = Peffect.get_repr e in
   let al = List.map (fun id -> (id,after_id id)) go in
   let q = option_app (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
@@ -93,12 +93,12 @@ and prod ren env g =
     g
 
 and input ren env e  =
-  let i,_ = Effects.get_repr e in
+  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 = Effects.get_repr e in
+  let _,o = Peffect.get_repr e in
   (prod ren env o) @ [id,tv]
 
 and input_output ren env c =
@@ -134,7 +134,7 @@ and trad_ml_type_v ren env = function
 		 let ren' = initial_renaming env' in
 		 (id,tt)::bl,ren',env'
 	     | (id, BindSet) ->
-		 (id,(DOP0(Sort(Prop Pos))))::bl,ren,env
+		 (id,mkSet) :: bl,ren,env
 	     | _ -> failwith "Monad: trad_ml_type_v: not yet implemented"
  	  )
  	  ([],ren,env) bl 
@@ -217,7 +217,7 @@ let result_tuple ren before env (res,v) (ef,q) =
 
    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
@@ -229,7 +229,7 @@ let multiple_let_in_pre ty hl t =
 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
+    | 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
@@ -268,15 +268,15 @@ let make_block ren env finish bl =
   let rec rec_block ren result = function
       [] ->
 	finish ren result
-   | (Assert c)::block ->
+   | (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 ->
+   | (Label s) :: block ->
        let ren' = push_date ren s in
        rec_block ren' result block
-   | (Statement (te,info))::block ->
+   | (Statement (te,info)) :: block ->
        let (_,tye),efe,pe,qe = info in
        let w = get_writes efe in
        let ren' = next ren w in
@@ -302,12 +302,12 @@ let lt r e1 e2 =
   Term.applist (r, [e1; e2])
 
 let is_recursive env = function
-    CC_var x -> 
+  | 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 ->
+  | CC_var x ->
       (try let v = find_recursion x env in (f v x) with Not_found -> [])
   | _ -> []
 
@@ -316,7 +316,7 @@ let dec_phi ren env s svi =
     (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 (VAR phi0))])
+       [CC_expr phi; CC_hole (lt r phi (mkVar phi0))])
 
 let eq_phi ren env s svi =
   if_recursion env
@@ -326,7 +326,7 @@ let eq_phi ren env s svi =
        [CC_hole (eq a phi phi)])
 
 let is_ref_binder = function 
-    (_,BindType (Ref _ | Array _)) -> true
+  | (_,BindType (Ref _ | Array _)) -> true
   | _ -> false
 
 let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
@@ -334,7 +334,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
   let (_,eapp,papp,qapp) = capp in
   let ((_,v),e,p,q) = c in
 
-  let bl = Std.map_succeed 
+  let bl = Util.map_succeed 
 	     (function b -> if is_ref_binder b then failwith "caught" else b) 
 	     bl
   in
@@ -380,7 +380,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
 	(res_f,trad_ml_type_v ren env tvf) (t,ty)
   in
   let rec eval_args ren = function
-      [] -> t
+    | [] -> t
     | (vx,(ta,((_,tva),ea,pa,qa)))::args ->
 	let w = get_writes ea in
 	let ren' = next ren w in
@@ -404,10 +404,10 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
 
 let make_if_case ren env ty (b,qb) (br1,br2) =
   let ty',id_b = match qb with
-      Some q ->  
+    | Some q ->  
   	let q = apply_post ren env (current_date ren) q in
     	let (name,t1,t2) = Term.destLambda q.a_value in
-    	Term.mkLambda name t1 (mkArrow t2 ty), q.a_name
+    	Term.mkLambda (name, t1, (mkArrow t2 ty)), q.a_name
     | None -> assert false
   in
   CC_app (CC_case (ty', (b, constant "bool"), [br1;br2]),
@@ -488,15 +488,15 @@ let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) =
   let t1 = 
     make_block ren' env 
       (fun ren'' result -> match result with
-	   Some (id,_) ->
+	 | 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'') (VAR id_phi0))]
+			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 -> [] 
+			    | None -> [] 
 			    | Some c -> 
 				[CC_hole (apply_assert ren'' env c).a_value])),
 	       ty
@@ -526,7 +526,7 @@ let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) =
   in
   let t = 
     CC_lam ([var_name Anonymous,
-	     CC_typed_binder (eq a (VAR id_phi0) (phi_of ren'))],t) 
+	     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
@@ -544,19 +544,19 @@ let make_while ren env (cphi,r,a) (tb,cb) tbl (i,c) =
     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
+      | 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 (VAR id_phi) (phi_of ren')) v 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 (VAR id_phi) (VAR id_phi0)) v) 
+      (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
@@ -574,7 +574,7 @@ let make_while ren env (cphi,r,a) (tb,cb) tbl (i,c) =
 	  @(List.map (fun (_,id) -> CC_var id) vars)
           @(CC_hole (eq a (phi_of ren) (phi_of ren)))
 	  ::(match i with
-		 None -> [] 
+	       | None -> [] 
 	       | Some c -> [CC_hole (apply_assert ren env c).a_value])) 
 
 
@@ -601,7 +601,7 @@ let make_letrec ren env (id_phi0,(cphi,r,a)) idf bl (te,ce) c =
     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 (VAR id_phi) (phi_of ren)) v 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) 
@@ -613,14 +613,14 @@ let make_letrec ren env (id_phi0,(cphi,r,a)) idf bl (te,ce) c =
   in
   let tw = 
     Term.mkNamedProd id_phi a
-      (Term.mkArrow (lt r (VAR id_phi) (VAR id_phi0)) v) 
+      (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 (VAR id_phi0) (phi_of ren))],
+		       CC_typed_binder (eq a (mkVar id_phi0) (phi_of ren))],
 		      bod) 
     in
     let bl' = binding_of_alist ren env al in
@@ -660,16 +660,13 @@ let array_info ren env id =
 
 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; VAR id'; c])
+  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)
-
+  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; VAR id'; c1; c2])
-
-
-(* $Id$ *)
+  Term.applist (constant "store", [size; ty_elem; mkVar id'; c1; c2])
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index 08a22f06f..02c84cf00 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -53,7 +53,6 @@ let rec red = function
 
 (* How to reduce uncomplete proof terms when they have become constr *)
 
-open Generic
 open Term
 open Reduction
 
@@ -64,16 +63,19 @@ open Reduction
  * puis on applique la reduction spéciale programmes définie dans
  * typing/reduction *)
 
+(*i
 let bin_app = function
-    DOPN(AppL,v) as c ->
+  | DOPN(AppL,v) as c ->
       (match Array.length v with
-	   1 -> v.(0)
+	 | 1 -> v.(0)
 	 | 2 -> c
 	 | n ->
 	     let f = DOPN(AppL,Array.sub v 0 (pred n)) in
-	       DOPN(AppL,[|f;v.(pred n)|]))
+	     DOPN(AppL,[|f;v.(pred n)|]))
   | c -> c
+i*)
 
 let red_cci c = 
-  let c = strong bin_app c in strong whd_programs c
+  (*i let c = strong bin_app c in i*) 
+  strong whd_programs (Global.env ()) Evd.empty c
 
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 620e42593..5eb03d23e 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -14,7 +14,6 @@ open Pp
 open Names
 open Term
 open Pfedit
-open Constrtypes
 open Vernacentries
 
 open Pmisc
@@ -33,43 +32,45 @@ open Pmonad
 
 let coqast_of_prog p =
   (* 1. db : séparation dB/var/const *)
-  let p = Prog_db.db_prog p in
+  let p = Pdb.db_prog p in
 
   (* 2. typage avec effets *)
-  deb_mess [< 'sTR"Prog_typing.states: Typage avec effets..."; 'fNL >];
-  let env = Prog_env.empty in
+  deb_mess [< 'sTR"Ptyping.states: Typage avec effets..."; 'fNL >];
+  let env = Penv.empty in
   let ren = initial_renaming env in
-  let p = Prog_typing.states ren env p in
+  let p = Ptyping.states ren env p in
   let ((_,v),_,_,_) as c = p.info.kappa in
-  Prog_errors.check_for_not_mutable p.loc v;
+  Perror.check_for_not_mutable p.loc v;
   deb_mess (pp_type_c c);
 
   (* 3. propagation annotations *)
-  let p = Prog_wp.propagate ren p in
+  let p = Pwp.propagate ren p in
 
   (* 4a. traduction type *)
-  let ty = Monad.trad_ml_type_c ren env c in
-  deb_mess (Himsg.pTERM ty);
+  let ty = Pmonad.trad_ml_type_c ren env c in
+  deb_mess (Printer.prterm ty);
 
   (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
   deb_mess 
     [< 'fNL; 'sTR"Mlise.trad: Traduction program -> cc_term..."; 'fNL >];
-  let cc = Mlise.trans ren p in
-  let cc = Prog_red.red cc in
-  deb_mess (Prog_utils.pp_cc_term cc);
+  let cc = Pmlize.trans ren p in
+  let cc = Pred.red cc in
+  deb_mess (Putil.pp_cc_term cc);
 
   (* 5. traduction en constr *)
   deb_mess 
-    [< 'fNL; 'sTR"Prog_cci.constr_of_prog: Traduction cc_term -> constr..."; 
+    [< 'fNL; 'sTR"Pcic.constr_of_prog: Traduction cc_term -> constr..."; 
        'fNL >];
-  let c = Prog_cci.constr_of_prog cc in
-  deb_mess (Himsg.pTERM c);
+  let c = Pcic.constr_of_prog cc in
+  deb_mess (Printer.prterm c);
 
   (* 6. résolution implicites *)
   deb_mess [< 'fNL; 'sTR"Résolution implicites (? => Meta(n))..."; 'fNL >];
-  let c =
+  let c = c in
+  (*i WAS
     (ise_resolve false (Evd.mt_evd()) [] (gLOB(initial_sign())) c)._VAL in
-  deb_mess (Himsg.pTERM c);
+  i*)
+  deb_mess (Printer.prterm c);
 
   p,c,ty,v
 
@@ -96,12 +97,28 @@ open Tactics
 open Tacticals
 open Equality
 
-let mmk = make_module_marker ["#Prelude.obj"; "#Wf.obj"]
-
-let wf_nat_pattern = put_pat mmk "(well_founded nat lt)"
-let zwf_nat_pattern = put_pat mmk "(well_founded Z (Zwf ?))"
-let and_pattern = put_pat mmk "(and ? ?)"
-let eq_pattern = put_pat mmk "(eq ? ? ?)"
+let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+
+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 ["Init";"fast_integer"] "Z", 0)
+let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0)
+let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0)
+
+(* ["(well_founded nat lt)"] *)
+let wf_nat_pattern = 
+  PApp (PRef well_founded, [| PRef nat; PRef lt |])
+(* ["((well_founded Z (Zwf ?))"] *)
+let wf_z_pattern = 
+  let zwf = ConstRef (coq_constant ["correctness";"Zwf"] "Zwf") in
+  PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta None |]) |])
+(* ["(and ? ?)"] *)
+let and_pattern = 
+  PApp (PRef and_, [| PMeta None; PMeta None |])
+(* ["(eq ? ? ?)"] *)
+let eq_pattern = 
+  PApp (PRef eq, [| PMeta None; PMeta None; PMeta None |])
 
 (* loop_ids: remove loop<i> hypotheses from the context, and rewrite
  * using Variant<i> hypotheses when needed. *)
@@ -109,27 +126,27 @@ let eq_pattern = put_pat mmk "(eq ? ? ?)"
 let (loop_ids : tactic) = fun gl ->
   let rec arec hyps gl =
     let concl = pf_concl gl in 
-      match hyps with
-	  ([],[]) -> tclIDTAC gl
-	| (id::sl,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 (sl,al)) gl
-	      else if n >= 7 & String.sub s 0 7 = "Variant" then begin
-		match dest_match gl (body_of_type a) eq_pattern with
-		    [_; VAR phi; _] ->
-		      if occur_var phi concl then
-			tclTHEN (rewriteLR (VAR id)) (arec (sl,al)) gl
-		      else
-			arec (sl,al) gl
-		  | _ -> assert false end
-	      else
-		arec (sl,al) gl
-	| _ -> assert false
+    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 (body_of_type a) with
+	      | [_; _,varphi; _] when isVar varphi ->
+		  let phi = destVar varphi in
+		  if occur_var 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 gl) gl
+  arec (pf_hyps_types gl) gl
 
 (* assumption_bis: like assumption, but also solves ... h:A/\B ... |- A 
  * (resp. B) *)
@@ -137,26 +154,25 @@ let (loop_ids : tactic) = fun gl ->
 let (assumption_bis : tactic) = fun gl ->
   let concl = pf_concl gl in 
   let rec arec = function
-      ([],[]) -> Std.error "No such assumption"
-    | (s::sl,a::al) ->
+    | [] -> Util.error "No such assumption"
+    | (s,a) :: al ->
 	let a = body_of_type a in
 	if pf_conv_x_leq gl a concl then 
-          refine (VAR s) gl
-	else if matches gl a and_pattern then
-	  match dest_match gl a and_pattern with
-	      [c1;c2] -> 
+          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 (applistc (constant "proj1") [c1;c2;VAR s]) gl
+		  exact_check (applistc (constant "proj1") [c1;c2;mkVar s]) gl
 		else if pf_conv_x_leq gl c2 concl then
-		  exact (applistc (constant "proj2") [c1;c2;VAR s]) gl
+		  exact_check (applistc (constant "proj2") [c1;c2;mkVar s]) gl
 		else
-		  arec (sl,al)
+		  arec al
 	    | _ -> assert false
 	else
-	  arec (sl,al)
-    | _ -> assert false
+	  arec al
   in 
-    arec (pf_hyps gl)
+  arec (pf_hyps_types gl)
 
 (* automatic: see above *)
 
@@ -165,40 +181,43 @@ let (automatic : tactic) =
     loop_ids
     (fun gl ->
        let c = pf_concl gl in
-	 if matches gl c wf_nat_pattern then
-	   exact (constant "lt_wf") gl
-	 else if matches gl c zwf_nat_pattern then
-	   let z = List.hd (dest_match gl c zwf_nat_pattern) in
-	     exact (Term.applist (constant "Zwf_well_founded",[z])) gl
-	 else if matches gl c and_pattern then
+	 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 matches gl c eq_pattern then
+	 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 -> unit
+(* [correctness s p] : string -> program -> tactic option -> unit
  *
- * Vernac: Correctness <string> <program>.
+ * Vernac: Correctness <string> <program> [; <tactic>].
  *)
 
 let correctness s p opttac =
-  Misc_utils.reset_names();
+  Pmisc.reset_names();
   let p,c,cty,v = coqast_of_prog p in
-  let sigma = Proof_trees.empty_evd in
-  let sign = initial_sign() in
-  let cty = Reduction.nf_betaiota cty in
-  start_proof_constr s NeverDischarge cty;
-  Prog_env.new_edited (id_of_string s) (v,p);
+  let env = Global.env () in
+  let sign = Global.named_context () in
+  let sigma = Evd.empty in
+  let cty = Reduction.nf_betaiota env sigma cty in
+  let id = id_of_string s in 
+  start_proof id Declare.NeverDischarge sign cty;
+  Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
-  deb_mess [< 'sTR"Prog_red.red_cci: Réduction..."; 'fNL >];
-  let c = Prog_red.red_cci c in
+  deb_mess [< 'sTR"Pred.red_cci: Réduction..."; 'fNL >];
+  let c = Pred.red_cci c in
   deb_mess [< 'sTR"APRES REDUCTION :"; 'fNL >];
-  deb_mess (Himsg.pTERM c);
-  let tac = (tclTHEN (Tcc.refine_tac c) automatic) in
+  deb_mess (Printer.prterm c);
+  let oc = [],c in (* TODO: quid des existentielles ici *)
+  let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
   let tac = match opttac with 
-      None -> tac
+    | None -> tac
     | Some t -> tclTHEN tac t
   in
   solve_nth 1 tac;
@@ -207,51 +226,47 @@ let correctness s p opttac =
 
 (* On redéfinit la commande "Save" pour enregistrer les nouveaux programmes *)
 
-open Initial
 open Vernacinterp
 
 let add = Vernacinterp.overwriting_vinterp_add
 
 let register id n =
   let id' = match n with None -> id | Some id' -> id' in
-    Prog_env.register id id'
+  Penv.register id id'
 
 let wrap_save_named b =
-  let pf_id = id_of_string (Pfedit.get_proof()) in
-    save_named b;
-    register pf_id None
+  let pf_id = Pfedit.get_current_proof_name () in
+  Command.save_named b;
+  register pf_id None
 
 let wrap_save_anonymous_thm b id =
-  let pf_id = id_of_string (Pfedit.get_proof()) in
-    save_anonymous_thm b (string_of_id id);
-    register pf_id (Some id)
+  let pf_id = Pfedit.get_current_proof_name () in
+  Command.save_anonymous_thm b (string_of_id id);
+  register pf_id (Some id)
 
 let wrap_save_anonymous_remark b id =
-  let pf_id = id_of_string (Pfedit.get_proof()) in
-    save_anonymous_remark b (string_of_id id);
-    register pf_id (Some id)
-;;
+  let pf_id = Pfedit.get_current_proof_name () in
+  Command.save_anonymous_remark b (string_of_id id);
+  register pf_id (Some id)
 
-add("SaveNamed",
-    function [] -> (fun () -> if not(is_silent()) then show_script();
+let _ = add "SaveNamed"
+    (function [] -> (fun () -> if not(Options.is_silent()) then show_script();
 		              wrap_save_named true)
-    |   _  -> assert false);;
+    |   _  -> assert false)
 
-add("DefinedNamed",
-    function [] -> (fun () -> if not(is_silent()) then show_script();
+let _ = add "DefinedNamed"
+    (function [] -> (fun () -> if not(Options.is_silent()) then show_script();
 		              wrap_save_named false)
-    |   _  -> assert false);;
+    |   _  -> assert false)
 
-add("SaveAnonymousThm",
-    function [VARG_IDENTIFIER id] -> 
-       (fun () -> if not(is_silent()) then show_script();
+let _ = add "SaveAnonymousThm"
+    (function [VARG_IDENTIFIER id] -> 
+       (fun () -> if not(Options.is_silent()) then show_script();
 	          wrap_save_anonymous_thm true id)
-    |   _  -> assert false);;
+    |   _  -> assert false)
 
-add("SaveAnonymousRmk",
-    function [VARG_IDENTIFIER id] -> 
-        (fun () -> if not(is_silent()) then show_script();
+let _ = add "SaveAnonymousRmk"
+    (function [VARG_IDENTIFIER id] -> 
+        (fun () -> if not(Options.is_silent()) then show_script();
 	            wrap_save_anonymous_remark true id)
-    |   _  -> assert false);;
-
-
+    |   _  -> assert false)
diff --git a/contrib/correctness/ptactic.mli b/contrib/correctness/ptactic.mli
index f1cd81a48..465e02bc2 100644
--- a/contrib/correctness/ptactic.mli
+++ b/contrib/correctness/ptactic.mli
@@ -18,5 +18,5 @@
  * Then an ad-hoc automatic tactic is applied on each subgoal to solve the
  * trivial proof obligations *)
 
-val correctness : string -> ProgAst.program -> Tacmach.tactic option -> unit
+val correctness : string -> Past.program -> Tacmach.tactic option -> unit
 
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index 773447f9a..29caf3107 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -14,7 +14,8 @@ open Pp
 open Util
 open Names
 open Term
-open Termast
+open Environ
+open Astterm
 open Himsg
 open Proof_trees
 
@@ -38,22 +39,22 @@ let type_v_sup loc t1 t2 =
   if t1 = t2 then
     t1
   else
-    Prog_errors.if_branches loc
+    Perror.if_branches loc
 
 let typed_var ren env (phi,r) =
-  let sign = TradEnv.before_after_sign_of ren env in
-  let a = Mach.type_of (Evd.mt_evd()) sign phi in
+  let sign = Pcicenv.before_after_sign_of ren env in
+  let a = Typing.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) -> 
-      Reduction.conv_x (Evd.mt_evd()) c1 c2
+      Reduction.is_conv (Global.env ()) Evd.empty c1 c2
   | (Ref v1, Ref v2) -> 
       convert (v1,v2)
   | (Array (s1,v1), Array (s2,v2)) -> 
-      (Reduction.conv_x (Evd.mt_evd()) s1 s2) && (convert (v1,v2))
+      (Reduction.is_conv (Global.env ()) Evd.empty s1 s2) && (convert (v1,v2))
   | (v1,v2) -> v1 = v2
       
 let effect_app ren env f args =
@@ -65,13 +66,13 @@ let effect_app ren env f args =
   let bl,c = 
     match tf with
 	Arrow (bl, c) ->
-	  if List.length bl <> n then Prog_errors.partial_app f.loc;
+	  if List.length bl <> n then Perror.partial_app f.loc;
 	  bl,c
-      | _ -> Prog_errors.app_of_non_function f.loc
+      | _ -> 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 Prog_errors.expected_type loc (pp_type_v v')
+    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. 
@@ -83,7 +84,7 @@ let effect_app ren env f args =
 	     let ta = type_in_env env id' in
 	     check_type f.loc v ta so;
 	     (id,id')::s, so, ok
-	 | _, Refarg _ -> Prog_errors.should_be_a_variable f.loc
+	 | _, 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;
@@ -91,10 +92,10 @@ let effect_app ren env f args =
 		  Expression c -> s, (id,c)::so, ok
 		| _ -> s,so,false)
 	 | (id,BindSet), Type v ->
-	     let c = Monad.trad_ml_type_v ren env v in
+	     let c = Pmonad.trad_ml_type_v ren env v in
 	     s, (id,c)::so, ok
-	 | (id,BindSet), Term t -> Prog_errors.expects_a_type id t.loc
-	 | (id,BindType _), Type _ -> Prog_errors.expects_a_term id
+	 | (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)
@@ -107,15 +108,16 @@ let effect_app ren env f args =
 
 let state_coq_ast sign a =
   let j =
-    reraise_with_loc (Ast.loc a) (fconstruct (Evd.mt_evd()) sign) a in
-  let ids = global_vars j._VAL in
-  j._VAL, j._TYPE, ids
+    let env = Global.env_of_context sign in
+    reraise_with_loc (Ast.loc a) (judgment_of_rawconstr Evd.empty env) a in
+  let ids = global_vars 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
-  Mach.type_of (Evd.mt_evd()) sign c
+  Typing.type_of (Global.env_of_context sign) Evd.empty c
 
 let rec is_pure_type_v = function
     TypePure _ -> true
@@ -154,13 +156,13 @@ and is_pure_arg ren env = function
  *)
 
 let state_var ren env (phi,r) = 
-  let sign = TradEnv.before_after_sign_of ren env in
+  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 Effects.add_read id e else e)
-	     Effects.bottom ids in
-  let r',_,_ = state_coq_ast (initial_sign()) r in
+		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
@@ -170,16 +172,16 @@ let state_var ren env (phi,r) =
 
 let state_pre ren env pl =
   let state e p =
-    let sign = TradEnv.before_sign_of ren env in
+    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
-		    Effects.add_read id e
+		    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
-		      Effects.add_read uid e
+		      Peffect.add_read uid e
 		    else
 		      e
 	     	  else
@@ -190,7 +192,7 @@ let state_pre ren env pl =
   in
   List.fold_left 
     (fun (e,cl) p -> let ef,c = state e p in (ef,c::cl)) 
-    (Effects.bottom,[]) pl
+    (Peffect.bottom,[]) pl
 
 let state_assert ren env a =
   let p = pre_of_assert true a in
@@ -198,7 +200,7 @@ let state_assert ren env a =
   e,assert_of_pre (List.hd l)
 
 let state_inv ren env = function
-    None -> Effects.bottom, None
+    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)
@@ -210,29 +212,29 @@ let state_inv ren env = function
  *)
 
 let state_post ren env (id,v,ef) = function
-    None -> Effects.bottom, None
+    None -> Peffect.bottom, None
   | Some q ->
-      let v' = Monad.trad_ml_type_v ren env v in
-      let sign = TradEnv.before_after_result_sign_of (Some (id,v')) ren env in
+      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
-		 Effects.add_write id e, c
+		 Peffect.add_write id e, c
 	       else
-		 Effects.add_read id e,
+		 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
-		 Effects.add_read uid e, c
+		 Peffect.add_read uid e, c
 	       else
 		 e,c
 	     else
 	       e,c)
-	  (Effects.bottom,cc) ids 
+	  (Peffect.bottom,cc) ids 
       in
       let c = abstract [id,v'] c in
       ef, Some { a_name = q.a_name; a_value = c }
@@ -240,10 +242,10 @@ let state_post ren env (id,v,ef) = function
 (* 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)
+  | Ref v -> Ref (cic_type_v env ren v)
   | Array (com,v) ->
-      let sign = TradEnv.now_sign_of ren env in
-      let c = constr_of_com (Evd.mt_evd()) sign com in
+      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' =
@@ -258,16 +260,16 @@ let rec cic_type_v env ren = function
       let c' = cic_type_c env' ren' c in
       Arrow (List.rev bl',c')
   | TypePure com ->
-      let sign = TradEnv.cci_sign_of ren env in
-      let c = constr_of_com (Evd.mt_evd()) sign com in
+      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 = Monad.trad_ml_type_v ren env 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 = Effects.union e (Effects.union efp efq) in
+  let ef = Peffect.union e (Peffect.union efp efq) in
   ((id,v'),ef,p',q')
 
 and cic_binder env ren = function
@@ -302,16 +304,16 @@ and cic_binders env ren = function
 
 let states_expression ren env expr =
   let rec effect pl = function
-      Var id -> 
-	(if is_global id then constant (string_of_id id) else VAR id),
-	pl, Effects.bottom
-    | Expression c -> c, pl, Effects.bottom
-    | Acc id -> VAR id, pl, Effects.add_read id Effects.bottom
+    | Var 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 = Monad.make_pre_access ren env id c in
-	Monad.make_raw_access ren env (id,id) c, 
-	(anonymous_pre true pre)::pl, Effects.add_read id ef
+	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
     | App (p,args) ->
 	let a,pl,e = effect pl p.desc in
 	let args,pl,e =
@@ -320,23 +322,25 @@ let states_expression ren env expr =
 	       match arg with
 		   Term p ->
 		     let carg,pl,earg = effect pl p.desc in
-		     carg::l,pl,Effects.union e earg
+		     carg::l,pl,Peffect.union e earg
 		 | Type v ->
 		     let v' = cic_type_v env ren v in
-		     (Monad.trad_ml_type_v ren env v')::l,pl,e
+		     (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 "Prog_typing.states_expression"
+    | _ -> 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 =TradEnv.before_sign_of ren env 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
-  let ty = Mach.type_of empty_evd sign c in
+  i*)
+  let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in
   let v = TypePure ty in
-  let ef = Effects.union e0 e in
+  let ef = Peffect.union e0 e in
   Expression c, (v,ef), pl0@pl
 
 
@@ -364,18 +368,18 @@ 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,Effects.bottom)
+      Expression c, (v,Peffect.bottom)
 
   | Acc _ ->
-      failwith "Prog_typing.states: term is supposed not to be pure"
+      failwith "Ptyping.states: term is supposed not to be pure"
 
   | Var id ->
       let v = type_in_env env id in
-      let ef = Effects.bottom in
+      let ef = Peffect.bottom in
       Var id, (v,ef)
 
   | Aff (x, e1) ->
-      Prog_errors.check_for_reference loc x (type_in_env env x);
+      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
@@ -385,7 +389,7 @@ let rec states_desc ren env loc = function
   | TabAcc (check, x, e) ->
       let s_e = states ren env e in
       let _,efe,_,_ = s_e.info.kappa in
-      let ef = Effects.add_read x efe 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)
 
@@ -394,7 +398,7 @@ let rec states_desc ren env loc = function
       let s_e2 = states ren env e2 in 
       let _,ef1,_,_ = s_e1.info.kappa in
       let _,ef2,_,_ = s_e2.info.kappa in
-      let ef = Effects.add_write x (Effects.union ef1 ef2) 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)
 
@@ -411,7 +415,7 @@ let rec states_desc ren env loc = function
       let efinv,inv = state_inv ren env invopt in
       let _,efb,_,_ = s_b.info.kappa in
       let ef = 
-	Effects.union (Effects.union ef_bl efb) (Effects.union efinv efphi)
+	Peffect.union (Peffect.union ef_bl efb) (Peffect.union efinv efphi)
       in
       let v = constant_unit () in
       let cvar = 
@@ -421,7 +425,7 @@ let rec states_desc ren env loc = function
       While (s_b,inv,(cvar,r'),s_bl), (v,ef)
       
   | Lam ([],_) ->
-      failwith "Prog_typing.states: abs. should have almost one binder"
+      failwith "Ptyping.states: abs. should have almost one binder"
 
   | Lam (bl, e) ->
       let bl' = cic_binders env ren bl in
@@ -429,7 +433,7 @@ let rec states_desc ren env loc = function
       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 = Effects.bottom in
+      let ef = Peffect.bottom in
       Lam(bl',s_e), (v,ef)
 	 
   (* Connectives AND and OR *)
@@ -438,7 +442,7 @@ let rec states_desc ren env loc = function
       and s_e2 = states ren env e2 in
       let (_,ef1,_,_) = s_e1.info.kappa
       and (_,ef2,_,_) = s_e2.info.kappa in
-      let ef = Effects.union ef1 ef2 in
+      let ef = Peffect.union ef1 ef2 in
       SApp ([Var id], [s_e1; s_e2]), 
       (TypePure (constant "bool"), ef)
 
@@ -449,7 +453,7 @@ let rec states_desc ren env loc = function
       SApp ([Var id], [s_e]), 
       (TypePure (constant "bool"), ef)
       
-  | SApp _ -> invalid_arg "Prog_typing.states (SApp)"
+  | SApp _ -> invalid_arg "Ptyping.states (SApp)"
 
   (* ATTENTION:
      Si un argument réel de type ref. correspond à une ref. globale
@@ -466,12 +470,12 @@ let rec states_desc ren env loc = function
       let ef_args = 
 	List.map 
 	  (function Term t -> let (_,e,_,_) = t.info.kappa in e
-	          | _ -> Effects.bottom) 
+	          | _ -> Peffect.bottom) 
 	  s_args 
       in
       let _,_,((_,tapp),efapp,_,_) = effect_app ren env s_f s_args in
       let ef = 
-	Effects.compose (List.fold_left Effects.compose eff ef_args) efapp
+	Peffect.compose (List.fold_left Peffect.compose eff ef_args) efapp
       in
       App (s_f, s_args), (tapp, ef)
       
@@ -482,18 +486,18 @@ let rec states_desc ren env loc = function
       let ren' = next ren [x] in
       let s_e2 = states ren' env' e2 in
       let (_,v2),ef2,_,_ = s_e2.info.kappa in
-      Prog_errors.check_for_let_ref loc v2;
-      let ef = Effects.compose ef1 (Effects.remove ef2 x) 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)
 	
   | LetIn (x, e1, e2) ->
       let s_e1 = states ren env e1 in
       let (_,v1),ef1,_,_ = s_e1.info.kappa in
-      Prog_errors.check_for_not_mutable e1.loc v1;
+      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 = Effects.compose ef1 ef2 in
+      let ef = Peffect.compose ef1 ef2 in
       LetIn (x, s_e1, s_e2), (v2,ef)
 	    
   | If (b, e1, e2) ->
@@ -503,7 +507,7 @@ let rec states_desc ren env loc = function
       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 = Effects.compose efb (disj ef1 ef2) 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)
 
@@ -529,13 +533,13 @@ let rec states_desc ren env loc = function
       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,Effects.bottom)
+      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 "Prog_typing.states: Debug: TODO"
+  | Debug _ -> failwith "Ptyping.states: Debug: TODO"
 
 
 and states_arg ren env = function
@@ -555,7 +559,7 @@ and states ren env expr =
   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' = Effects.union e (Effects.union ep eq) 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;
@@ -568,13 +572,13 @@ and states_block ren env bl =
   let rec ef_block ren tyres = function
       [] ->
 	begin match tyres with
-	    Some ty -> [],ty,Effects.bottom,ren
+	    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,Effects.union ep ef,ren'
+	(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
@@ -584,7 +588,7 @@ and states_block ren env bl =
 	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,Effects.compose efe ef,ren''
+	(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
index 985d7b52e..bfb7a9a86 100644
--- a/contrib/correctness/ptyping.mli
+++ b/contrib/correctness/ptyping.mli
@@ -19,17 +19,17 @@ open Penv
 
 (* This module realizes type and effect inference *)
 
-val cic_type_v : local_env -> Renamings.t -> CoqAst.t ml_type_v -> type_v
+val cic_type_v : local_env -> Prename.t -> Coqast.t ml_type_v -> type_v
 
-val effect_app : Renamings.t -> local_env
-            -> (typing_info,'b) ProgAst.t
+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 : Renamings.t -> local_env -> constr * constr -> variant
+val typed_var : Prename.t -> local_env -> constr * constr -> variant
 
-val type_of_expression : Renamings.t -> local_env -> constr -> constr
+val type_of_expression : Prename.t -> local_env -> constr -> constr
 
-val states : Renamings.t -> local_env -> program -> typed_program
+val states : Prename.t -> local_env -> program -> typed_program
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index af6801a1c..e73b9b233 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -10,11 +10,9 @@
 
 (* $Id$ *)
 
-open More_util
+open Util
 open Names
-open Generic
 open Term
-open Environ
 
 open Pmisc
 open Ptype
@@ -41,7 +39,7 @@ open Prename
 
 (* force a post-condition *)
 let update_post env top ef c =
-  let i,o = Effects.get_repr ef in
+  let i,o = Peffect.get_repr ef in
   let al = 
     List.fold_left 
       (fun l id -> 
@@ -109,18 +107,16 @@ let create_bool_post c =
  * (if result then c=true else c=false) if b is an expression c.
  *)
 
-let bool_id = id_of_string "bool"
-
 let is_bool = function
-    TypePure c ->
-      (match (strip_outer_cast c) with
-	   DOPN(MutInd _ as op,_) -> id_of_global op = bool_id
+  | TypePure c ->
+      (match kind_of_term (strip_outer_cast c) with
+	 | IsMutInd (op,_) -> Global.string_of_global (IndRef op) = "bool"
 	 | _ -> false)
   | _ -> false
 
 let normalize_boolean ren env b =
   let ((res,v),ef,p,q) = b.info.kappa in
-  Prog_errors.check_no_effect b.loc ef;
+  Perror.check_no_effect b.loc ef;
   if is_bool v then
     match q with
 	Some _ ->
@@ -142,7 +138,7 @@ let normalize_boolean ren env b =
 	    | _ -> b
 	end
   else
-    Prog_errors.should_be_boolean b.loc
+    Perror.should_be_boolean b.loc
 
 (* [decomp_boolean c] returns the specs R and S of a boolean expression *)
 
@@ -150,7 +146,7 @@ let decomp_boolean = function
     Some { a_value = q } ->
       Reduction.whd_betaiota (Term.applist (q, [constant "true"])),
       Reduction.whd_betaiota (Term.applist (q, [constant "false"]))
-  | _ -> invalid_arg "Prog_typing.decomp_boolean"
+  | _ -> invalid_arg "Ptyping.decomp_boolean"
 
 (* top point of a program *)
 
@@ -211,7 +207,7 @@ let rec propagate_desc ren info d =
     | TabAcc (ch,x,e) ->
       	TabAcc (ch, x, propagate ren e)
     | TabAff (ch,x,({desc=Expression c} as e1),e2) ->
-	let p = Monad.make_pre_access ren env x c in
+	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) ->
@@ -296,7 +292,7 @@ and propagate ren p =
 	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 (Evd.mt_evd()) c in
+	  let c = Reduction.whd_betadeltaiota (Global.env()) Evd.empty c in
 	  create_bool_post c
 	in
 	let d = 
@@ -310,7 +306,7 @@ and propagate ren p =
 	let (r1,s1) = decomp_boolean q1 in
 	let q = 
 	  let c = Term.applist (constant "spec_not", [r1; s1]) in
-	  let c = Reduction.whd_betadeltaiota (Evd.mt_evd()) c in
+	  let c = Reduction.whd_betadeltaiota (Global.env ()) Evd.empty c in
 	  create_bool_post c 
 	in
 	let d = SApp ([Var id; Expression (out_post q1)], [ e1 ]) in
@@ -328,7 +324,7 @@ and propagate_block ren env = function
   | (Statement p) :: (Assert q) :: rem when annotation_candidate p ->
       let q' =
 	let ((id,v),_,_,_) = p.info.kappa in
-	let tv = Monad.trad_ml_type_v ren env v 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
diff --git a/contrib/correctness/pwp.mli b/contrib/correctness/pwp.mli
index 7ccc52c82..a47a8b713 100644
--- a/contrib/correctness/pwp.mli
+++ b/contrib/correctness/pwp.mli
@@ -13,6 +13,6 @@
 open Term
 open Penv
 
-val update_post : local_env -> string -> Effects.t -> constr -> constr
+val update_post : local_env -> string -> Peffect.t -> constr -> constr
 
-val propagate : Renamings.t -> typed_program -> typed_program
+val propagate : Prename.t -> typed_program -> typed_program