GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

15 files changed, 115 insertions, 96 deletions

diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 7696c6698c..9919ee993f 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -48,7 +48,7 @@ type ('a, 'b) t = {
 }
 
 and ('a, 'b) t_desc =
-  | Var of variable
+  | Variable of variable
   | Acc of variable
   | Aff of variable * ('a, 'b) t
   | TabAcc of bool * variable * ('a, 'b) t
@@ -58,10 +58,10 @@ and ('a, 'b) t_desc =
                (('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
-  | App of ('a, 'b) t * ('a, 'b) arg list
+  | 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
-  | LetIn 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
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index d13be77200..be8f142032 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -12,9 +12,13 @@
 
 open Names
 open Term
+open Termops
+open Nametab
 open Declarations
+open Indtypes
 open Sign
 open Rawterm
+open Typeops
 
 open Pmisc
 open Past
@@ -30,7 +34,7 @@ let make_hole c = mkCast (isevar, c)
  * If necessary, tuples are generated ``on the fly''. *)
 
 let tuple_exists id =
-  try let _ = Nametab.sp_of_id CCI id in true with Not_found -> false
+  try let _ = Nametab.sp_of_id id in true with Not_found -> false
 
 let ast_set = Ast.ope ("SET", [])
 
@@ -73,8 +77,10 @@ let sig_n n =
     (List.rev_map (fun id -> (id, LocalAssum mkSet)) lT)
   in
   let lc = 
-    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 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
@@ -118,13 +124,13 @@ let tuple_ref dep n =
 	let name = Printf.sprintf "exist_%d" n in
 	let id = id_of_string name in
 	if not (tuple_exists id) then ignore (sig_n n);
-	Nametab.sp_of_id CCI id
+	Nametab.sp_of_id id
       end
     else begin
       let name = Printf.sprintf "Build_tuple_%d" n in
       let id = id_of_string name in
       if not (tuple_exists id) then tuple_n n;
-      Nametab.sp_of_id CCI id
+      Nametab.sp_of_id id
     end
 
 (* Binders. *)
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
index c1b4b0fa3f..4663b3e370 100644
--- a/contrib/correctness/pcicenv.ml
+++ b/contrib/correctness/pcicenv.ml
@@ -24,14 +24,17 @@ open Past
 
 (* 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
+  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 empty_named_context
 
 let add_sign (id,t) s =
-  if mem_named_context id s then
+  try 
+    let _ = lookup_named id s in
     modify_sign id t s
-  else
-    add_named_assum (id,t) s
+  with Not_found ->
+    add_named_decl (id,None,t) s
 
 let cast_set c = mkCast (c, mkSet)
 
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index a0651e90c2..142ba63c95 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -12,6 +12,8 @@
 
 open Names
 open Term
+open Termops
+open Nametab
 
 open Ptype
 open Past
@@ -90,7 +92,7 @@ let rec db_binders ((tids,pids,refs) as idl) = function
 let rec db_pattern = function
   | (PatVar id) as t ->
       (try 
-	 (match Nametab.sp_of_id CCI id with
+	 (match Nametab.sp_of_id id with
 	    | ConstructRef (x,y) -> [], PatConstruct (id,(x,y))
 	    | _                  -> [id],t)
        with Not_found -> [id],t)
@@ -115,7 +117,7 @@ let rec db_pattern = function
 let db_prog e =
   (* tids = type identifiers, ids = variables, refs = references and arrays *)
   let rec db_desc ((tids,ids,refs) as idl) = function
-    | (Var x) as t ->
+    | (Variable x) as t ->
 	(match lookup_var ids (Some e.loc) x with
 	     None -> t
 	   | Some c -> Expression c)
@@ -145,14 +147,14 @@ let db_prog e =
 	  
     | Lam (bl,e) ->
 	let idl',bl' = db_binders idl bl in Lam(bl', db idl' e)
-    | App (e1,l) ->
-	App (db idl e1, List.map (db_arg idl) l)
+    | 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)
-    | LetIn (x,e1,e2) ->
-	LetIn (x, db idl e1, db (tids,x::ids,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
@@ -166,7 +168,7 @@ let db_prog e =
     | PPoint (s,d) -> PPoint (s, db_desc idl d)
 	  
   and db_arg ((tids,_,refs) as idl) = function
-    | Term ({ desc = Var id } as t) -> 
+    | 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
@@ -178,7 +180,7 @@ let db_prog e =
       loc = e.loc; info = e.info }
 
   in
-  let ids = Sign.ids_of_named_context (Global.named_context ()) 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
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 466905962d..feee251ff5 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -128,7 +128,7 @@ let add_global id v p =
 	if is_mutable v then id 
         else id_of_string ("prog_" ^ (string_of_id id)) 
       in
-      Lib.add_leaf id' OBJ (inProg (id,TypeV v,p))
+      Lib.add_leaf id' (inProg (id,TypeV v,p))
     end
 
 let add_global_set id =
@@ -136,7 +136,7 @@ let add_global_set id =
     let _ = Env.find id !env in
     Perror.clash id None
   with
-    Not_found -> Lib.add_leaf id OBJ (inProg (id,Set,None))
+    Not_found -> Lib.add_leaf id (inProg (id,Set,None))
 
 let is_global id =
   try
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 1eb44d5bc5..452e1b5811 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -66,7 +66,7 @@ let is_constant_type s = function
     TypePure c ->
       let id = id_of_string s in
       let c' = Declare.global_reference id in
-      Reduction.is_conv (Global.env()) Evd.empty c c'
+      Reductionops.is_conv (Global.env()) Evd.empty c c'
   | _ -> false 
 
 let check_for_index_type loc v =
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index ad7779036e..6d04befe23 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -13,10 +13,9 @@
 open Pp
 open Coqast
 open Names
+open Nameops
 open Term
 
-module SpSet = Set.Make(struct type t = section_path let compare = sp_ord end)
-
 (* debug *)
 
 let debug = ref false
@@ -144,11 +143,12 @@ let real_subst_in_constr = replace_vars
 
 let coq_constant d s =
   make_path
-    (make_dirpath (List.map id_of_string ("Coq" :: d))) (id_of_string s) CCI
+    (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 = mkMutConstruct ((bool_sp,0),1)
-let coq_false = mkMutConstruct ((bool_sp,0),2)
+let coq_true = mkConstruct ((bool_sp,0),1)
+let coq_false = mkConstruct ((bool_sp,0),2)
 
 let constant s =
   let id = id_of_string s in
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index a4359b6d89..3dbae5cd0c 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -13,8 +13,6 @@
 open Names
 open Term
 
-module SpSet : Set.S with type elt = section_path
-
 (* Some misc. functions *)
 
 val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
index 8fa2fa58e1..aa81310030 100644
--- a/contrib/correctness/pmlize.ml
+++ b/contrib/correctness/pmlize.ml
@@ -58,7 +58,7 @@ and trad_desc ren env ct d =
       	let ty = trad_ml_type_v ren env tt in
       	make_tuple [ CC_expr c',ty ] qt ren env (current_date ren)
       
-  | Var id ->
+  | Variable id ->
       if is_mutable_in_env env id then
 	invalid_arg "Mlise.trad_desc"
       else if is_local env id then
@@ -170,7 +170,7 @@ and trad_desc ren env ct d =
       let te = trans ren' e in
       CC_lam (bl', te)
 
-  | SApp ([Var id; Expression q1; Expression q2], [e1; e2])
+  | 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
@@ -179,7 +179,7 @@ and trad_desc ren env ct d =
       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 ([Var id; Expression q], [e]) when id = connective_not ->
+  | 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
@@ -188,7 +188,7 @@ and trad_desc ren env ct d =
   | SApp _ ->
       invalid_arg "mlise.trad (SApp)"
 
-  | App (f, args) ->
+  | Apply (f, args) ->
       let trad_arg (ren,args) = function
 	| Term a ->
 	    let ((_,tya),efa,_,_) as ca = a.info.kappa in
@@ -239,7 +239,7 @@ and trad_desc ren env ct d =
       in
       t
 
-  | LetIn (x, e1, e2) ->
+  | 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
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index 0531315670..6a9c41a72a 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -88,7 +88,7 @@ let rec red = function
 (* How to reduce uncomplete proof terms when they have become constr *)
 
 open Term
-open Reduction
+open Reductionops
 
 (* Il ne faut pas reduire de redexe (beta/iota) qui impliquerait
  * la substitution d'une métavariable.
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 70596779d0..b85a50790f 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -115,15 +115,16 @@ let isevar = Expression isevar
 
 let bin_op op loc e1 e2 =
   without_effect loc
-    (App (without_effect loc (Expression (constant op)), [ Term e1; Term e2 ]))
+    (Apply (without_effect loc (Expression (constant op)),
+            [ Term e1; Term e2 ]))
 
 let un_op op loc e =
   without_effect loc
-    (App (without_effect loc (Expression (constant op)), [Term e]))
+    (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 ( [Var op], [a1; a2]) in
+  let d = SApp ( [Variable op], [a1; a2]) in
   w d
 
 let bool_or  loc = bool_bin connective_or loc
@@ -131,7 +132,7 @@ let bool_and loc = bool_bin connective_and loc
 
 let bool_not loc a =
   let w = without_effect loc in
-  let d = SApp ( [Var connective_not ], [a]) in
+  let d = SApp ( [Variable connective_not ], [a]) in
   w d
 
 let ast_zwf_zero loc =
@@ -147,9 +148,9 @@ let bdize c =
   Termast.ast_of_constr true env c
 
 let rec coqast_of_program loc = function
-  | Var id -> let s = string_of_id id in <:ast< ($VAR $s) >>
+  | Variable id -> let s = string_of_id id in <:ast< ($VAR $s) >>
   | Acc id -> let s = string_of_id id in <:ast< ($VAR $s) >>
-  | App (f,l) -> 
+  | 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
@@ -178,8 +179,8 @@ let ast_plus_un loc ast =
 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 (Var id_i) in
-  let var_f = without_effect loc (Var f) 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
@@ -190,7 +191,7 @@ let make_ast_for loc i v1 v2 inv block =
     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 (App (var_f, [Term succ_i])) 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' = 
@@ -205,14 +206,14 @@ let make_ast_for loc i v1 v2 inv block =
     let typez = ast_constant loc "Z" in
     [(id_of_string i, BindType (TypePure typez))] 
   in
-  let fv1 = without_effect loc (App (var_f, [Term v1])) in
+  let fv1 = without_effect loc (Apply (var_f, [Term v1])) in
   let v = TypePure (ast_constant loc "unit") in
   let var = 
     let zminus = ast_constant loc "Zminus" in
     let a = <:ast< (APPLIST $zminus $succ_v2 ($VAR $i)) >> in
     (a, ast_zwf_zero loc)
   in
-  LetIn (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1)
+  Let (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1)
 
 let mk_prog loc p pre post =
   { desc = p.desc; 
@@ -376,7 +377,7 @@ GEXTEND Gram
     ;
   ast7:
     [ [ v = variable -> 
-	  Var v
+	  Variable v
       | n = INT ->
 	  Expression (constr_of_int n)
       | "!"; v = variable ->
@@ -408,7 +409,7 @@ GEXTEND Gram
 	"in"; p2 = program ->
 	  LetRef (v, p1, p2)
       | IDENT "let"; v = variable; "="; p1 = program; "in"; p2 = program ->
-	  LetIn (v, p1, p2)
+	  Let (v, p1, p2)
       | IDENT "begin"; b = block; "end" ->
 	  Seq b
       | IDENT "fun"; bl = binders; "->"; p = program ->
@@ -421,7 +422,7 @@ GEXTEND Gram
 	bl = binders; ":"; v = type_v;
 	"{"; IDENT "variant"; var = variant; "}"; "="; p = program;
  	"in"; p2 = program ->
-	  LetIn (f, without_effect loc (LetRec (f,bl,v,var,p)), p2)
+	  Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2)
 
       | "@"; s = STRING; p = program ->
 	  Debug (s,p)
@@ -433,7 +434,7 @@ GEXTEND Gram
 		  Pp.warning "Some annotations are lost";
 		p.desc
             | _  -> 
-		App(p,args)
+		Apply(p,args)
      ] ]
   ;
   arg:
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index d4c3494a8a..011c3c7e88 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -95,6 +95,7 @@ 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")
@@ -136,7 +137,7 @@ let (loop_ids : tactic) = fun gl ->
 	    match pf_matches gl eq_pattern (body_of_type a) with
 	      | [_; _,varphi; _] when isVar varphi ->
 		  let phi = destVar varphi in
-		  if Environ.occur_var env phi concl then
+		  if Termops.occur_var env phi concl then
 		    tclTHEN (rewriteLR (mkVar id)) (arec al) gl
 		  else
 		    arec al gl
@@ -200,11 +201,11 @@ let (automatic : tactic) =
 let reduce_open_constr (em,c) =
   let existential_map_of_constr = 
     let rec collect em c = match kind_of_term c with
-      | IsCast (c',t) -> 
+      | Cast (c',t) -> 
 	  (match kind_of_term c' with
-	     | IsEvar ev -> (ev,t) :: em
+	     | Evar ev -> (ev,t) :: em
 	     | _ -> fold_constr collect em c)
-      | IsEvar _ -> 
+      | Evar _ -> 
 	  assert false (* all existentials should be casted *)
       | _ -> 
 	  fold_constr collect em c
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index de5d2da7d8..2e95f840f2 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -14,6 +14,7 @@ open Pp
 open Util
 open Names
 open Term
+open Termops
 open Environ
 open Astterm
 open Himsg
@@ -50,11 +51,11 @@ let typed_var ren env (phi,r) =
 
 let rec convert = function
   | (TypePure c1, TypePure c2) -> 
-      Reduction.is_conv (Global.env ()) Evd.empty c1 c2
+      Reductionops.is_conv (Global.env ()) Evd.empty c1 c2
   | (Ref v1, Ref v2) -> 
       convert (v1,v2)
   | (Array (s1,v1), Array (s2,v2)) -> 
-      (Reduction.is_conv (Global.env ()) Evd.empty s1 s2) && (convert (v1,v2))
+      (Reductionops.is_conv (Global.env ()) Evd.empty s1 s2) && (convert (v1,v2))
   | (v1,v2) -> v1 = v2
       
 let effect_app ren env f args =
@@ -132,15 +133,16 @@ and is_pure_type_c = function
   | _ -> false
 
 let rec is_pure_desc ren env = function
-    Var id -> not (is_in_env env id) or (is_pure_type_v (type_in_env env id))
+    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
-  | App (p,args) -> 
+  | 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 _ | LetIn _ | LetRec _ -> false
+  | 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 =
@@ -304,7 +306,7 @@ and cic_binders env ren = function
 
 let states_expression ren env expr =
   let rec effect pl = function
-    | Var id -> 
+    | Variable id -> 
 	(if is_global id then constant (string_of_id id) else mkVar id),
 	pl, Peffect.bottom
     | Expression c -> c, pl, Peffect.bottom
@@ -314,7 +316,7 @@ let states_expression ren env expr =
 	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) ->
+    | Apply (p,args) ->
 	let a,pl,e = effect pl p.desc in
 	let args,pl,e =
 	  List.fold_right
@@ -373,10 +375,10 @@ let rec states_desc ren env loc = function
   | Acc _ ->
       failwith "Ptyping.states: term is supposed not to be pure"
 
-  | Var id ->
+  | Variable id ->
       let v = type_in_env env id in
       let ef = Peffect.bottom in
-      Var id, (v,ef)
+      Variable id, (v,ef)
 
   | Aff (x, e1) ->
       Perror.check_for_reference loc x (type_in_env env x);
@@ -437,20 +439,20 @@ let rec states_desc ren env loc = function
       Lam(bl',s_e), (v,ef)
 	 
   (* Connectives AND and OR *)
-  | SApp ([Var id], [e1;e2]) ->
+  | 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 ([Var id], [s_e1; s_e2]), 
+      SApp ([Variable id], [s_e1; s_e2]), 
       (TypePure (constant "bool"), ef)
 
   (* Connective NOT *)
-  | SApp ([Var id], [e]) ->
+  | SApp ([Variable id], [e]) ->
       let s_e = states ren env e in
       let (_,ef,_,_) = s_e.info.kappa in
-      SApp ([Var id], [s_e]), 
+      SApp ([Variable id], [s_e]), 
       (TypePure (constant "bool"), ef)
       
   | SApp _ -> invalid_arg "Ptyping.states (SApp)"
@@ -463,7 +465,7 @@ let rec states_desc ren env loc = function
             donc si on l'applique à r justement, elle ne modifiera que r
             mais le séquencement ne sera pas correct. *)
 
-  | App (f, args) ->
+  | 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
@@ -477,7 +479,7 @@ let rec states_desc ren env loc = function
       let ef = 
 	Peffect.compose (List.fold_left Peffect.compose eff ef_args) efapp
       in
-      App (s_f, s_args), (tapp, ef)
+      Apply (s_f, s_args), (tapp, ef)
       
   | LetRef (x, e1, e2) ->
       let s_e1 = states ren env e1 in
@@ -490,7 +492,7 @@ let rec states_desc ren env loc = function
       let ef = Peffect.compose ef1 (Peffect.remove ef2 x) in
       LetRef (x, s_e1, s_e2), (v2,ef)
 	
-  | LetIn (x, e1, e2) ->
+  | 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;
@@ -498,7 +500,7 @@ let rec states_desc ren env loc = function
       let s_e2 = states ren env' e2 in
       let (_,v2),ef2,_,_ = s_e2.info.kappa in
       let ef = Peffect.compose ef1 ef2 in
-      LetIn (x, s_e1, s_e2), (v2,ef)
+      Let (x, s_e1, s_e2), (v2,ef)
 	    
   | If (b, e1, e2) ->
       let s_b = states ren env b in
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 73d1778ac0..fecd577d7c 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -13,6 +13,7 @@
 open Util
 open Names
 open Term
+open Termops
 open Pattern
 open Environ
 
@@ -196,15 +197,15 @@ let dest_sig c = match matches (Coqlib.build_coq_sig_pattern ()) c with
 
 (* TODO: faire un test plus serieux sur le type des objets Coq *)
 let rec is_pure_cci c = match kind_of_term c with
-  | IsCast (c,_) -> is_pure_cci c
-  | IsProd(_,_,c') -> is_pure_cci c'
-  | IsRel _ | IsMutInd _ | IsConst _ -> true (* heu... *)
-  | IsApp _ -> not (is_matching (Coqlib.build_coq_sig_pattern ()) c)
+  | Cast (c,_) -> is_pure_cci c
+  | Prod(_,_,c') -> is_pure_cci c'
+  | Rel _ | Ind _ | Const _ -> true (* heu... *)
+  | App _ -> not (is_matching (Coqlib.build_coq_sig_pattern ()) c)
   | _ -> Util.error "CCI term not acceptable in programs"
 
 let rec v_of_constr c = match kind_of_term c with
-  | IsCast (c,_) -> v_of_constr c
-  | IsProd _ ->
+  | Cast (c,_) -> v_of_constr c
+  | Prod _ ->
       let revbl,t2 = Term.decompose_prod c in
       let bl =
 	List.map
@@ -213,7 +214,7 @@ let rec v_of_constr c = match kind_of_term c with
       in
       let vars = List.rev (List.map (fun (id,_) -> mkVar id) bl) in
       Arrow (bl, c_of_constr (substl vars t2))
-  | IsMutInd _ | IsConst _ | IsApp _ ->
+  | Ind _ | Const _ | App _ ->
       TypePure c
   | _ -> 
       failwith "v_of_constr: TODO"
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index 1381bdf92c..adaafbc68f 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -13,7 +13,9 @@
 open Util
 open Names
 open Term
+open Termops
 open Environ
+open Nametab
 
 open Pmisc
 open Ptype
@@ -79,7 +81,7 @@ let post_if_none env q = function
  * post-condition *)
 
 let annotation_candidate = function
-  | { desc = If _ | LetIn _ | LetRef _ ; post = None } -> true
+  | { desc = If _ | Let _ | LetRef _ ; post = None } -> true
   | _ -> false
 
 (* [extract_pre p] erase the pre-condition of p and returns it *)
@@ -111,7 +113,8 @@ let create_bool_post c =
 let is_bool = function
   | TypePure c ->
       (match kind_of_term (strip_outer_cast c) with
-	 | IsMutInd op -> Global.string_of_global (IndRef op) = "bool"
+	 | Ind op ->
+             string_of_id (id_of_global (Global.env()) (IndRef op)) = "bool"
 	 | _ -> false)
   | _ -> false
 
@@ -145,8 +148,8 @@ let normalize_boolean ren env b =
 
 let decomp_boolean = function
   | Some { a_value = q } ->
-      Reduction.whd_betaiota (Term.applist (q, [constant "true"])),
-      Reduction.whd_betaiota (Term.applist (q, [constant "false"]))
+      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 *)
@@ -213,8 +216,8 @@ let rec propagate_desc ren info d =
       	TabAff (false, x, propagate ren e1', propagate ren e2)
     | TabAff (ch,x,e1,e2) ->
       	TabAff (ch, x, propagate ren e1, propagate ren e2)
-    | App (f,l) ->
-      	App (propagate ren f, List.map (propagate_arg ren) l)
+    | 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
@@ -236,16 +239,16 @@ let rec propagate_desc ren info d =
 	let ren' = push_date ren top in
 	PPoint (top, LetRef (x, propagate ren' e1, 
 	      		     propagate ren' (post_if_none_up env top q e2)))
-    | LetIn (x,e1,e2) ->
+    | Let (x,e1,e2) ->
 	let top = label_name() in
 	let ren' = push_date ren top in
-      	PPoint (top, LetIn (x, propagate ren' e1, 
+      	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 _ | Var _ 
+    | Debug _ | Variable _ 
     | Acc _ | Expression _ as d -> d
 	  
 
@@ -253,7 +256,7 @@ let rec propagate_desc ren info d =
 and propagate ren p =
   let env = p.info.env in
   let p = match p.desc with
-    | App (f,l) ->
+    | Apply (f,l) ->
 	let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in
 	if ok then
 	  let q = option_app (named_app (real_subst_in_constr so)) qapp in
@@ -284,7 +287,7 @@ and propagate ren p =
 	let q = option_app (named_app abstract_unit) q in
 	post_if_none env q p
 
-    | SApp ([Var id], [e1;e2]) 
+    | SApp ([Variable id], [e1;e2]) 
       when id = connective_and or id = connective_or ->
 	let (_,_,_,q1) = e1.info.kappa
 	and (_,_,_,q2) = e2.info.kappa in
@@ -293,24 +296,26 @@ 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 (Global.env()) Evd.empty c in
+	  let c = Reduction.whd_betadeltaiota (Global.env()) c in
 	  create_bool_post c
 	in
 	let d = 
-	  SApp ([Var id; Expression (out_post q1); Expression (out_post q2)], 
+	  SApp ([Variable id;
+                 Expression (out_post q1);
+                 Expression (out_post q2)], 
 		[e1; e2] ) 
 	in
 	post_if_none env q (change_desc p d)
 
-    | SApp ([Var id], [e1]) when id = connective_not ->
+    | 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 ()) Evd.empty c in
+	  let c = Reduction.whd_betadeltaiota (Global.env ()) c in
 	  create_bool_post c 
 	in
-	let d = SApp ([Var id; Expression (out_post q1)], [ e1 ]) in
+	let d = SApp ([Variable id; Expression (out_post q1)], [ e1 ]) in
 	post_if_none env q (change_desc p d)
 
     | _ -> p