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

47 files changed, 713 insertions, 651 deletions

diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 7696c6698..9919ee993 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 d13be7720..be8f14203 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 c1b4b0fa3..4663b3e37 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 a0651e90c..142ba63c9 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 466905962..feee251ff 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 1eb44d5bc..452e1b581 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 ad7779036..6d04befe2 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 a4359b6d8..3dbae5cd0 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 8fa2fa58e..aa8131003 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 053131567..6a9c41a72 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 70596779d..b85a50790 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 d4c3494a8..011c3c7e8 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 de5d2da7d..2e95f840f 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 73d1778ac..fecd577d7 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 1381bdf92..adaafbc68 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
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index fd7c3da03..65cc52fe8 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -10,13 +10,13 @@
 
 open Pp
 open Names
+open Nameops
 open Miniml
 open Table
 open Mlutil
 open Ocaml
 open Nametab
 
-
 (*s Modules considerations *)
 
 let current_module = ref None
@@ -53,7 +53,7 @@ let cache r f =
 module ToplevelParams = struct
   let toplevel = true
   let globals () = Idset.empty
-  let rename_global r = Names.id_of_string (Global.string_of_global r)
+  let rename_global r = Termops.id_of_global (Global.env()) r
   let pp_type_global = Printer.pr_global
   let pp_global = Printer.pr_global
 end
@@ -74,13 +74,13 @@ module MonoParams = struct
   let rename_type_global r =  
     cache r
       (fun r -> 
-	 let id = Environ.id_of_global (Global.env()) r in
+	 let id = Termops.id_of_global (Global.env()) r in
 	 rename_global_id (lowercase_id id))
       
   let rename_global r = 
     cache r
       (fun r -> 
-	 let id = Environ.id_of_global (Global.env()) r in
+	 let id = Termops.id_of_global (Global.env()) r in
 	 match r with
 	   | ConstructRef _ -> rename_global_id (uppercase_id id)
 	   | _ -> rename_global_id (lowercase_id id))
@@ -118,13 +118,13 @@ module ModularParams = struct
   let rename_type_global r = 
     cache r 
       (fun r ->     
-	 let id = Environ.id_of_global (Global.env()) r in 
+	 let id = Termops.id_of_global (Global.env()) r in 
 	 rename_global_id r id (lowercase_id id) "coq_")
 
   let rename_global r =
     cache r 
       (fun r -> 
-	 let id = Environ.id_of_global (Global.env()) r in 
+	 let id = Termops.id_of_global (Global.env()) r in 
 	 match r with
 	   | ConstructRef _ -> rename_global_id r id (uppercase_id id) "Coq_"
 	   | _ -> rename_global_id r id (lowercase_id id) "coq_")
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 823388f4b..122075c87 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -11,6 +11,7 @@
 open Miniml
 open Mlutil
 open Names
+open Nametab
 
 module ToplevelPp : Mlpp
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index da5d0d9c1..9ca23646f 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -17,6 +17,7 @@ open Extraction
 open Miniml
 open Table
 open Mlutil
+open Nametab
 open Vernacinterp
 open Common
 
@@ -164,9 +165,9 @@ let _ =
 	      let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
 	      match kind_of_term c with
 		(* If it is a global reference, then output the declaration *)
-		| IsConst sp -> extract_reference (ConstRef sp)
-		| IsMutInd ind -> extract_reference (IndRef ind)
-		| IsMutConstruct cs -> extract_reference (ConstructRef cs)
+		| Const sp -> extract_reference (ConstRef sp)
+		| Ind ind -> extract_reference (IndRef ind)
+		| Construct cs -> extract_reference (ConstructRef cs)
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) [] c with
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 5e7fadd8e..2fef10de1 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -11,10 +11,12 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
+open Termops
 open Declarations
 open Environ
-open Reduction
+open Reductionops
 open Inductive
 open Instantiate
 open Miniml
@@ -22,6 +24,7 @@ open Table
 open Mlutil
 open Closure
 open Summary
+open Nametab
 
 (*s Extraction results. *)
 
@@ -110,7 +113,7 @@ let whd_betaiotalet = clos_norm_flags (UNIFORM, mkflags [fBETA;fIOTA;fZETA])
 
 let is_axiom sp = (Global.lookup_constant sp).const_body = None
 
-type lamprod = Lam | Prod
+type lamprod = Lam | Product
 
 let flexible_name = id_of_string "flex"
 
@@ -141,19 +144,19 @@ let rec list_of_ml_arrows = function
 
 let rec get_arity env c =
   match kind_of_term (whd_betadeltaiota env none c) with
-    | IsProd (x,t,c0) -> get_arity (push_rel_assum (x,t) env) c0
-    | IsCast (t,_) -> get_arity env t
-    | IsSort s -> Some (family_of_sort s)
+    | Prod (x,t,c0) -> get_arity (push_rel (x,None,t) env) c0
+    | Cast (t,_) -> get_arity env t
+    | Sort s -> Some (family_of_sort s)
     | _ -> None
 
 (* idem, but goes through [Lambda] as well. Cf. [find_conclusion]. *)
 
 let rec get_lam_arity env c =
   match kind_of_term (whd_betadeltaiota env none c) with
-    | IsLambda (x,t,c0) -> get_lam_arity (push_rel_assum (x,t) env) c0
-    | IsProd (x,t,c0) -> get_lam_arity (push_rel_assum (x,t) env) c0
-    | IsCast (t,_) -> get_lam_arity env t
-    | IsSort s -> Some (family_of_sort s)
+    | Lambda (x,t,c0) -> get_lam_arity (push_rel (x,None,t) env) c0
+    | Prod (x,t,c0) -> get_lam_arity (push_rel (x,None,t) env) c0
+    | Cast (t,_) -> get_lam_arity env t
+    | Sort s -> Some (family_of_sort s)
     | _ -> None
 
 (*s Detection of non-informative parts. *)
@@ -193,7 +196,8 @@ type binders = (name * constr) list
 let rec lbinders_fold f acc env = function 
   | [] -> acc
   | (n,t) as b :: l -> 
-      f n t (v_of_t env t) (lbinders_fold f acc (push_rel_assum b env) l)
+      f n t (v_of_t env t)
+        (lbinders_fold f acc (push_rel_assum b env) l)
 
 (* [sign_of_arity] transforms an arity into a signature. It is used 
    for example with the types of inductive definitions, which are known
@@ -340,32 +344,31 @@ and extract_type_rec env c vl args =
 	    
 and extract_type_rec_info env c vl args = 
   match (kind_of_term (whd_betaiotalet env none c)) with
-    | IsSort _ ->
+    | Sort _ ->
 	assert (args = []); (* A sort can't be applied. *)
 	Tarity 
-    | IsProd (n,t,d) ->
+    | Prod (n,t,d) ->
 	assert (args = []); (* A product can't be applied. *)
-	extract_prod_lam env (n,t,d) vl Prod
-    | IsLambda (n,t,d) ->
+	extract_prod_lam env (n,t,d) vl Product
+    | Lambda (n,t,d) ->
 	assert (args = []); (* [c] is now in head normal form. *)
 	extract_prod_lam env (n,t,d) vl Lam
-    | IsApp (d, args') ->
+    | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type_rec_info env d vl (Array.to_list args' @ args)
-    | IsRel n -> 
-	(match lookup_rel_value n env with
-	   | Some t -> 
+    | Rel n -> 
+	(match lookup_rel n env with
+	   | (_,Some t,_) -> 
 	       extract_type_rec_info env (lift n t) vl args  
-	   | None ->
-	       let id = id_of_name (fst (lookup_rel_type n env)) in 
-	       Tmltype (Tvar id, [], vl))
-    | IsConst sp when args = [] && is_ml_extraction (ConstRef sp) ->
+	   | (id,_,_) ->
+	       Tmltype (Tvar (id_of_name id), [], vl))
+    | Const sp when args = [] && is_ml_extraction (ConstRef sp) ->
 	Tmltype (Tglob (ConstRef sp), [], vl)
-    | IsConst sp when is_axiom sp -> 
+    | Const sp when is_axiom sp -> 
 	let id = next_ident_away (basename sp) vl in 
 	Tmltype (Tvar id, [], id :: vl)
-    | IsConst sp ->
-	let t = constant_type env none sp in 
+    | Const sp ->
+	let t = constant_type env sp in 
 	if is_arity env none t then
 	  (match extract_constant sp with 
 	     | Emltype (Miniml.Tarity,_,_) -> Tarity
@@ -378,19 +381,19 @@ and extract_type_rec_info env c vl args =
 	  (*   which type is not an arity: we reduce this constant. *)
 	  let cvalue = constant_value env sp in
 	  extract_type_rec_info env (applist (cvalue, args)) vl []
-    | IsMutInd spi ->
+    | Ind spi ->
 	(match extract_inductive spi with 
 	   |Iml (si,vli) -> 
 	       extract_type_app env (IndRef spi,si,vli) vl args 
 	   |Iprop -> assert false (* Cf. initial tests *))
-    | IsMutCase _ | IsFix _ | IsCoFix _ ->
+    | Case _ | Fix _ | CoFix _ ->
 	let id = next_ident_away flexible_name vl in
 	Tmltype (Tvar id, [], id :: vl)
 	  (* Type without counterpart in ML: we generate a 
 	     new flexible type variable. *) 
-    | IsCast (c, _) ->
+    | Cast (c, _) ->
 	extract_type_rec_info env c vl args
-    | IsVar _ -> section_message ()
+    | Var _ -> section_message ()
     | _ -> 
 	assert false
 
@@ -412,12 +415,12 @@ and extract_prod_lam env (n,t,d) vl flag =
 	(match extract_type_rec_info  env' d vl [] with 
 	   | Tmltype (mld, sign, vl') -> Tmltype (mld, tag::sign, vl')
 	   | et -> et)
-    | (Logic, NotArity), Prod ->
+    | (Logic, NotArity), Product ->
 	(match extract_type_rec_info env' d vl [] with 
 	   | Tmltype (mld, sign, vl') ->
 	       Tmltype (Tarr (Miniml.Tprop, mld), tag::sign, vl')
 	   | et -> et)
-    | (Info, NotArity), Prod ->
+    | (Info, NotArity), Product ->
 	(* It is important to treat [d] first and [t] in second. *)
 	(* This ensures that the end of [vl] correspond to external binders. *)
 	(match extract_type_rec_info env' d vl [] with 
@@ -499,7 +502,7 @@ and extract_term_info env ctx c =
 
 and extract_term_info_with_type env ctx c t = 
    match kind_of_term c with
-     | IsLambda (n, t, d) ->
+     | Lambda (n, t, d) ->
 	 let v = v_of_t env t in 
 	 let env' = push_rel_assum (n,t) env in
 	 let ctx' = (snd v = NotArity) :: ctx in
@@ -509,9 +512,9 @@ and extract_term_info_with_type env ctx c t =
 	    | _,Arity -> d'
 	    | Logic,NotArity -> MLlam (prop_name, d')
 	    | Info,NotArity -> MLlam (id_of_name n, d'))
-     | IsLetIn (n, c1, t1, c2) ->
+     | LetIn (n, c1, t1, c2) ->
 	 let v = v_of_t env t1 in
-	 let env' = push_rel_def (n,c1,t1) env in
+	 let env' = push_rel (n,Some c1,t1) env in
 	 (match v with
 	    | (Info, NotArity) -> 
 		let c1' = extract_term_info_with_type env ctx c1 t1 in
@@ -520,25 +523,25 @@ and extract_term_info_with_type env ctx c t =
 		MLletin (id_of_name n,c1',c2')
 	    | _ ->
 		extract_term_info env' (false :: ctx) c2)
-     | IsRel n ->
+     | Rel n ->
 	 MLrel (renum_db ctx n)
-     | IsConst sp ->
+     | Const sp ->
 	 MLglob (ConstRef sp)
-     | IsApp (f,a) ->
+     | App (f,a) ->
       	 extract_app env ctx f a 
-     | IsMutConstruct cp ->
+     | Construct cp ->
 	 abstract_constructor cp
-     | IsMutCase ((_,(ip,_,_,_,_)),_,c,br) ->
+     | Case ({ci_ind=ip},_,c,br) ->
 	 extract_case env ctx ip c br
-     | IsFix ((_,i),recd) -> 
+     | Fix ((_,i),recd) -> 
 	 extract_fix env ctx i recd
-     | IsCoFix (i,recd) -> 
+     | CoFix (i,recd) -> 
 	 extract_fix env ctx i recd  
-     | IsCast (c, _) ->
+     | Cast (c, _) ->
 	 extract_term_info_with_type env ctx c t
-     | IsMutInd _ | IsProd _ | IsSort _ | IsMeta _ | IsEvar _ ->
+     | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ ->
 	 assert false 
-     | IsVar _ -> section_message ()
+     | Var _ -> section_message ()
 	 
 
 (* Abstraction of an inductive constructor: 
@@ -581,8 +584,8 @@ and abstract_constructor cp  =
 (* Extraction of a case *)
 
 and extract_case env ctx ip c br = 
-  let mis = Global.lookup_mind_specif ip in
-  let ni = Array.map List.length (mis_recarg mis) in
+  let (mib,mip) = Global.lookup_inductive ip in
+  let ni = Array.map List.length (mip.mind_listrec) in
   (* [ni]: number of arguments without parameters in each branch *)
   (* [br]: bodies of each branch (in functional form) *)
   let extract_branch j b = 	  
@@ -596,7 +599,7 @@ and extract_case env ctx ip c br =
     let ctx' = List.fold_left (fun l v -> (v = default)::l) ctx s in 
     (* Some pathological cases need an [extract_constr] here rather *)
     (* than an [extract_term]. See exemples in [test_extraction.v] *)
-    let env' = push_rels_assum rb env in
+    let env' = push_rel_context (List.map (fun (x,t) -> (x,None,t)) rb) env in
     let e' = mlterm_of_constr (extract_constr env' ctx' e) in
     let ids = 
       List.fold_right 
@@ -757,13 +760,13 @@ and extract_constructor (((sp,_),_) as c) =
    constructor which has one informative argument. This dummy case will 
    be simplified. *)
 
-and is_singleton_inductive (sp,_) = 
-  let mib = Global.lookup_mind sp in 
+and is_singleton_inductive ind = 
+  let (mib,mip) = Global.lookup_inductive ind in 
   (mib.mind_ntypes = 1) &&
-  let mis = build_mis (sp,0) mib in
-  (mis_nconstr mis = 1) && 
-  match extract_constructor ((sp,0),1) with 
-    | Cml ([mlt],_,_)-> (try parse_ml_type sp mlt; true with Found_sp -> false)
+  (Array.length mip.mind_consnames = 1) && 
+  match extract_constructor (ind,1) with 
+    | Cml ([mlt],_,_)->
+        (try parse_ml_type (fst ind) mlt; true with Found_sp -> false)
     | _ -> false
 	  
 and is_singleton_constructor ((sp,i),_) = 
@@ -774,15 +777,15 @@ and signature_of_constructor cp = match extract_constructor cp with
   | Cml (_,s,n) -> (s,n)
 
 and extract_mib sp =
-  if not (Gmap.mem (sp,0) !inductive_extraction_table) then begin
-    let mib = Global.lookup_mind sp in
+  let ind = (sp,0) in
+  if not (Gmap.mem ind !inductive_extraction_table) then begin
+    let (mib,mip) = Global.lookup_inductive ind in
     let genv = Global.env () in 
     (* Everything concerning parameters. 
        We do that first, since they are common to all the [mib]. *)
-    let mis = build_mis (sp,0) mib in
-    let nb = mis_nparams mis in
-    let rb = mis_params_ctxt mis in 
-    let env = push_rels rb genv in
+    let nb = mip.mind_nparams in
+    let rb = mip.mind_params_ctxt in 
+    let env = push_rel_context rb genv in
     let lb = List.rev_map (fun (n,s,t)->(n,t)) rb in 
     let nbtokeep = 
       lbinders_fold 
@@ -793,11 +796,11 @@ and extract_mib sp =
     let vl0 = iterate_for 0 (mib.mind_ntypes - 1)
 	(fun i vl -> 
 	   let ip = (sp,i) in 
-	   let mis = build_mis ip mib in 
-	   if (mis_sort mis) = (Prop Null) then begin
+	   let (mib,mip) = Global.lookup_inductive ip in 
+	   if mip.mind_sort = (Prop Null) then begin
 	     add_inductive_extraction ip Iprop; vl
 	   end else begin
-	     let arity = mis_nf_arity mis in
+	     let arity = mip.mind_nf_arity in
 	     let vla = List.rev (vl_of_arity genv arity) in 
 	     add_inductive_extraction ip 
 	       (Iml (sign_of_arity genv arity, vla));
@@ -812,16 +815,16 @@ and extract_mib sp =
       iterate_for 0 (mib.mind_ntypes - 1)
 	(fun i vl -> 
 	   let ip = (sp,i) in
-	   let mis = build_mis ip mib in
-	   if mis_sort mis = Prop Null then begin
-	     for j = 1 to mis_nconstr mis do
+           let (mib,mip) = Global.lookup_inductive ip in
+	   if mip.mind_sort = Prop Null then begin
+	     for j = 1 to Array.length mip.mind_consnames do
 	       add_constructor_extraction (ip,j) Cprop
 	     done;
 	     vl
 	   end else 
-	     iterate_for 1 (mis_nconstr mis)
+	     iterate_for 1 (Array.length mip.mind_consnames)
 	       (fun j vl -> 
-		  let t = mis_constructor_type j mis in
+		  let t = type_of_constructor genv (ip,j) in
 		  let t = snd (decompose_prod_n nb t) in
 		  match extract_type_rec_info env t vl [] with
 		    | Tarity | Tprop -> assert false
@@ -836,7 +839,6 @@ and extract_mib sp =
     (* Third pass: we update the type variables list in the inductives table *)
     for i = 0 to mib.mind_ntypes-1 do 
       let ip = (sp,i) in 
-      let mis = build_mis ip mib in
       match lookup_inductive_extraction ip with 
 	| Iprop -> ()
 	| Iml (s,l) -> add_inductive_extraction ip (Iml (s,vl@l));
@@ -844,8 +846,7 @@ and extract_mib sp =
     (* Fourth pass: we update also in the constructors table *)
     for i = 0 to mib.mind_ntypes-1 do 
       let ip = (sp,i) in 
-      let mis = build_mis ip mib in 
-      for j = 1 to mis_nconstr mis do
+      for j = 1 to Array.length mib.mind_packets.(i).mind_consnames do
 	let cp = (ip,j) in 
 	match lookup_constructor_extraction cp  with 
 	  | Cprop -> ()
@@ -884,14 +885,14 @@ and extract_inductive_declaration sp =
       iterate_for (1 - mib.mind_ntypes) 0
 	(fun i acc -> 
 	   let ip = (sp,-i) in
-	   let mis = build_mis ip mib in 
+	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
 	   match lookup_inductive_extraction ip with
 	     | Iprop -> acc
 	     | Iml (_,vl) -> 
-		 (List.rev vl, IndRef ip, one_ind ip (mis_nconstr mis)) :: acc)
+		 (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
 	[] 
     in
-    Dtype (l, not (mind_type_finite mib 0))
+    Dtype (l, not mib.mind_finite)
 
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index e75e39fe6..afc6efd6f 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -14,6 +14,7 @@ open Names
 open Term
 open Miniml
 open Environ
+open Nametab
 
 (*s Result of an extraction. *)
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index cb1ac038d..f59a282ca 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -13,11 +13,13 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
 open Miniml
 open Mlutil
 open Options
 open Ocaml
+open Nametab
 
 (*s Haskell renaming issues. *)
 
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index e1a7f0cd0..beed696d4 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -10,6 +10,7 @@
 
 open Pp
 open Names
+open Nametab
 open Miniml
 
 val keywords : Idset.t
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 125bf7865..a022d67d8 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -13,6 +13,7 @@
 open Pp
 open Names
 open Term
+open Nametab
 
 (*s ML type expressions. *)
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 2f3a67b6e..00da8e84b 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -14,6 +14,7 @@ open Term
 open Declarations
 open Util
 open Miniml
+open Nametab
 open Table
 open Options
 
@@ -603,4 +604,3 @@ let rec optimize prm = function
   | (Dtype _ | Dabbrev _ | Dcustom _) as d :: l -> 
       d :: (optimize prm l)
 
-
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 3771151b4..327ef5b94 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -11,6 +11,7 @@
 open Names
 open Term
 open Miniml
+open Nametab
 
 (*s Special identifiers. [prop_name] is to be used for propositions
     and will be printed as [_] in concrete (Caml) code. *)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 4470e00ac..185bbe0a7 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -13,11 +13,13 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
 open Miniml
 open Table
 open Mlutil
 open Options
+open Nametab
 
 let current_module = ref None
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index b982adcdc..e9faa1a0a 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -14,6 +14,7 @@ open Pp
 open Miniml
 open Names
 open Term
+open Nametab
 
 val current_module : identifier option ref
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 7953f1182..f1f00d1e3 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -18,7 +18,7 @@ open Util
 open Pp
 open Term 
 open Declarations
-
+open Nametab
 
 (*s AutoInline parameter *)
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 2a0a3092b..ff47bcede 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -10,6 +10,7 @@
 
 open Vernacinterp
 open Names
+open Nametab
 
 (*s AutoInline parameter *) 
 
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 5bc4e4433..00f0cbe89 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -177,8 +177,8 @@ Tactic Definition Multiply mul :=
     [Intro;
      Let id = GrepMult In
      Apply (mult_eq ?1 ?3 ?4 mul ?2 id)(*;
-     Cbv Beta Delta -[interp_ExprA] Zeta Evar Iota*)
-    |Cbv Beta Delta -[not] Zeta Evar Iota;
+     Cbv Beta Delta -[interp_ExprA] Zeta Iota*)
+    |Cbv Beta Delta -[not] Zeta Iota;
      Let AmultT = Eval Compute in (Amult ?1)
      And AoneT = Eval Compute in (Aone ?1) In
      (Match Context With
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 90e87c9df..5727f1fd7 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -23,7 +23,8 @@ let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
 
 (* Construction of constants *)
 let constant dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::"field"::dir)) in
+  let dir = make_dirpath
+    (List.map id_of_string (List.rev ("Coq"::"field"::dir))) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 652a96910..b3e141822 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -75,18 +75,18 @@ let pf_parse_constr gl s =
 
 let rec string_of_constr c =
  match kind_of_term c with
-   IsCast (c,t) -> string_of_constr c
-  |IsConst c -> string_of_path c
-  |IsVar(c) -> string_of_id c
+   Cast (c,t) -> string_of_constr c
+  |Const c -> string_of_path c
+  |Var(c) -> string_of_id c
   | _ -> "not_of_constant"
 ;;
 
 let rec rational_of_constr c =
   match kind_of_term c with
-  | IsCast (c,t) -> (rational_of_constr c)
-  | IsApp (c,args) ->
+  | Cast (c,t) -> (rational_of_constr c)
+  | App (c,args) ->
         (match kind_of_term c with
-           IsConst c ->
+           Const c ->
                (match (string_of_path c) with
 		 "Coq.Reals.Rdefinitions.Ropp" -> 
 		      rop (rational_of_constr args.(0))
@@ -106,7 +106,7 @@ let rec rational_of_constr c =
                              (rational_of_constr args.(1))
                 | _ -> failwith "not a rational")
           | _ -> failwith "not a rational")
-  | IsConst c ->
+  | Const c ->
         (match (string_of_path c) with
 	       "Coq.Reals.Rdefinitions.R1" -> r1
               |"Coq.Reals.Rdefinitions.R0" -> r0
@@ -117,10 +117,10 @@ let rec rational_of_constr c =
 let rec flin_of_constr c =
   try(
     match kind_of_term c with
-  | IsCast (c,t) -> (flin_of_constr c)
-  | IsApp (c,args) ->
+  | Cast (c,t) -> (flin_of_constr c)
+  | App (c,args) ->
         (match kind_of_term c with
-           IsConst c ->
+           Const c ->
             (match (string_of_path c) with
 	     "Coq.Reals.Rdefinitions.Ropp" -> 
                   flin_emult (rop r1) (flin_of_constr args.(0))
@@ -152,7 +152,7 @@ let rec flin_of_constr c =
                              (rinv b)))
             |_->assert false)
            |_ -> assert false)
-  | IsConst c ->
+  | Const c ->
         (match (string_of_path c) with
 	       "Coq.Reals.Rdefinitions.R1" -> flin_one ()
               |"Coq.Reals.Rdefinitions.R0" -> flin_zero ()
@@ -183,11 +183,11 @@ type hineq={hname:constr; (* le nom de l'hypothèse *)
 *)
 let ineq1_of_constr (h,t) =
     match (kind_of_term t) with
-       IsApp (f,args) ->
+       App (f,args) ->
          let t1= args.(0) in
          let t2= args.(1) in
          (match kind_of_term f with
-           IsConst c ->
+           Const c ->
             (match (string_of_path c) with
 		 "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
                            htype="Rlt";
@@ -218,13 +218,13 @@ let ineq1_of_constr (h,t) =
                                              (flin_of_constr t1);
 			   hstrict=false}]
                 |_->assert false)
-          | IsMutInd (sp,i) ->
+          | Ind (sp,i) ->
               (match (string_of_path sp) with 
 		 "Coq.Init.Logic_Type.eqT" ->  let t0= args.(0) in
                            let t1= args.(1) in
                            let t2= args.(2) in
 		    (match (kind_of_term t0) with
-                         IsConst c ->
+                         Const c ->
 			   (match (string_of_path c) with
 			      "Coq.Reals.Rdefinitions.R"->
                          [{hname=h;
@@ -370,7 +370,7 @@ let tac_use h = match h.htype with
 
 let is_ineq (h,t) =
     match (kind_of_term t) with
-       IsApp (f,args) ->
+       App (f,args) ->
          (match (string_of_constr f) with
 		 "Coq.Reals.Rdefinitions.Rlt" -> true
 		|"Coq.Reals.Rdefinitions.Rgt" -> true
@@ -399,7 +399,7 @@ let rec fourier gl=
        et le but à prouver devient False *)
     try (let tac =
      match (kind_of_term goal) with
-      IsApp (f,args) ->
+      App (f,args) ->
       (match (string_of_constr f) with
 	     "Coq.Reals.Rdefinitions.Rlt" -> 
 	       (tclTHEN
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 3dff01937..3b9d742e2 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -8,7 +8,7 @@ and ct_AST =
     CT_coerce_ID_OR_INT_to_AST of ct_ID_OR_INT
   | CT_coerce_ID_OR_STRING_to_AST of ct_ID_OR_STRING
   | CT_astnode of ct_ID * ct_AST_LIST
-  | CT_astpath of ct_ID_LIST * ct_ID
+  | CT_astpath of ct_ID_LIST
   | CT_astslam of ct_ID_OPT * ct_AST
 and ct_AST_LIST =
     CT_ast_list of ct_AST list
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 2f864b13e..bba7396b0 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -1,6 +1,7 @@
 
 (*Toplevel loop for the communication between Coq and Centaur *)
 open Names;;
+open Nameops
 open Util;;
 open Ast;;
 open Term;;
@@ -243,8 +244,10 @@ let filter_by_module_from_varg_list (l:vernac_arg list) =
 
 let add_search (global_reference:global_reference) assumptions cstr =
   try 
-  let id_string = string_of_qualid (Global.qualid_of_global global_reference) in
-  let ast = 
+    let env = Global.env() in
+    let id_string =
+      string_of_qualid (Nametab.qualid_of_global env global_reference) in
+    let ast = 
     try
       CT_premise (CT_ident id_string, translate_constr assumptions cstr)
     with Not_found ->
@@ -303,11 +306,13 @@ and ntyp = nf_betaiota typ in
 (* The following function is copied from globpr in env/printer.ml *)
 let globcv = function
   | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
-       convert_qualid
-	 (Global.qualid_of_global (IndRef(sp,tyi)))
+      let env = Global.env() in
+      convert_qualid
+	 (Nametab.qualid_of_global env (IndRef(sp,tyi)))
   | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
-       convert_qualid
-          (Global.qualid_of_global (ConstructRef ((sp, tyi), i)))
+      let env = Global.env() in
+      convert_qualid
+          (Nametab.qualid_of_global env (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
 let pbp_tac_pcoq =
@@ -389,7 +394,7 @@ let inspect n =
              	sp, Lib.Leaf lobj ->
 		  (match sp, object_tag lobj with
                        _, "VARIABLE" ->
-			 let ((_, _, v), _) = get_variable sp in
+			 let ((_, _, v), _) = get_variable (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | sp, ("CONSTANT"|"PARAMETER") ->
 			 let {const_type=typ} = Global.lookup_constant sp in
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index 5b97716fc..b356f5b28 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -11,15 +11,15 @@ type t =
   | Num of loc * int
   | Id of loc * string
   | Str of loc * string
-  | Path of loc * string list* string
+  | Path of loc * string list
   | Dynamic of loc * Dyn.t
 
-let section_path sl k =
+let section_path sl =
   match List.rev sl with
     | s::pa ->
 	make_path
 	  (make_dirpath (List.rev (List.map id_of_string pa)))
-	  (id_of_string s) (kind_of_string k)
+	  (id_of_string s)
     | [] -> invalid_arg "section_path"
 
 let is_meta s = String.length s > 0 && s.[0] == '$'
@@ -40,7 +40,7 @@ let rec ct_to_ast = function
   | Num (loc,a) -> Coqast.Num (loc,a)
   | Id (loc,a) -> Coqast.Id (loc,a)
   | Str (loc,a) -> Coqast.Str (loc,a)
-  | Path (loc,sl,k) -> Coqast.Path (loc,section_path sl k)
+  | Path (loc,sl) -> Coqast.Path (loc,section_path sl)
   | Dynamic (loc,a) -> Coqast.Dynamic (loc,a)
 
 let rec ast_to_ct = function
@@ -55,8 +55,9 @@ let rec ast_to_ct = function
   | Coqast.Id (loc,a) -> Id (loc,a)
   | Coqast.Str (loc,a) -> Str (loc,a)
   | Coqast.Path (loc,a) ->
-    let (sl,bn,pk) = repr_path a in
-    Path(loc, (List.map string_of_id (repr_dirpath sl)) @ [string_of_id bn],(* Bidon *) "CCI")
+    let (sl,bn) = repr_path a in
+    Path(loc, (List.map string_of_id
+                (List.rev (repr_dirpath sl))) @ [string_of_id bn])
   | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
 
 let loc = function
@@ -66,7 +67,7 @@ let loc = function
   | Num (loc,_) -> loc
   | Id (loc,_) -> loc
   | Str (loc,_) -> loc
-  | Path (loc,_,_) -> loc
+  | Path (loc,_) -> loc
   | Dynamic (loc,_) -> loc
 
 let str s = Str(Ast.dummy_loc,s)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index f84fe33ef..7f2ea95a4 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -15,6 +15,7 @@ open Ctast;;
 open Termast;;
 open Astterm;;
 open Vernacinterp;;
+open Nametab
 
 open Proof_type;;
 open Proof_trees;;
@@ -51,7 +52,7 @@ let zz = (0,0);;
 let rec get_subterm  (depth:int) (path: int list) (constr:constr) =
   match depth, path, kind_of_term constr with
     0, l, c -> (constr,l)
-  | n, 2::a::tl, IsApp(func,arr) -> 
+  | n, 2::a::tl, App(func,arr) -> 
       get_subterm (n - 2) tl arr.(a-1)
   | _,l,_ -> failwith (int_list_to_string 
                         "wrong path or wrong form of term"
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index e4523121c..8d3fd79c0 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -1,6 +1,7 @@
 open Sign;;
 open Classops;;
 open Names;;
+open Nameops
 open Coqast;;
 open Ast;;
 open Termast;;
@@ -15,6 +16,7 @@ open Inductive;;
 open Util;;
 open Pp;;
 open Declare;;
+open Nametab
 
 
 (* This function converts the parameter binders of an inductive definition,
@@ -86,8 +88,8 @@ let convert_qualid qid =
   let d, id = Nametab.repr_qualid qid in
     match repr_dirpath d with
 	[] -> nvar id
-      | d -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
-		   [nvar id]);;
+      | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l)
+		   [nvar id] d);;
 
 (* This function converts constructors for an inductive definition to a
    Coqast.t.  It is obtained directly from print_constructors in pretty.ml *)
@@ -106,9 +108,9 @@ let convert_constructors envpar names types =
 let convert_one_inductive sp tyi =
   let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
   let env = Global.env () in
-  let envpar = push_rels params env in
+  let envpar = push_rel_context params env in
   ope("VERNACARGLIST",
-      [convert_qualid (Global.qualid_of_global(IndRef (sp, tyi)));
+      [convert_qualid (Nametab.qualid_of_global env (IndRef (sp, tyi)));
        ope("CONSTR", [ast_of_constr true envpar arity]);
        ope("BINDERLIST", convert_env(List.rev params));
        convert_constructors envpar cstrnames cstrtypes]);;
@@ -123,7 +125,7 @@ let mutual_to_ast_list sp mib =
     Array.fold_right
       (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
   (ope("MUTUALINDUCTIVE",
-	  [str (if (mipv.(0)).mind_finite then "Inductive" else "CoInductive");
+	  [str (if mib.mind_finite then "Inductive" else "CoInductive");
 	  ope("VERNACARGLIST", ast_list)])::
      (implicit_args_to_ast_list sp mipv));;
 
@@ -157,17 +159,14 @@ let make_definition_ast name c typ implicits =
 (* This function is inspired by print_constant *)
 let constant_to_ast_list sp =
   let cb = Global.lookup_constant sp in
-    if kind_of_path sp = CCI then
-      let c = cb.const_body in
-      let typ = cb.const_type in
-      let l = constant_implicits_list sp in
-	(match c with
-	     None -> 
-	       make_variable_ast (basename sp) typ l
-	   | Some c1 ->
-	       make_definition_ast (basename sp) c1 typ l)
-    else
-      errorlabstrm "print" [< 'sTR "printing of FW terms not implemented" >];;
+  let c = cb.const_body in
+  let typ = cb.const_type in
+  let l = constant_implicits_list sp in
+  (match c with
+      None -> 
+	make_variable_ast (basename sp) typ l
+    | Some c1 ->
+	make_definition_ast (basename sp) c1 typ l)
 
 let variable_to_ast_list sp =
   let ((id, c, v), _) = get_variable sp in
@@ -182,18 +181,14 @@ let variable_to_ast_list sp =
 
 let inductive_to_ast_list sp =
   let mib = Global.lookup_mind sp in
-    if kind_of_path sp = CCI then
-      mutual_to_ast_list sp mib
-    else
-      errorlabstrm "print"
-	[< 'sTR "printing of FW not implemented" >];;
+  mutual_to_ast_list sp mib
 
 (* this function is inspired by print_leaf_entry from pretty.ml *)
 
 let leaf_entry_to_ast_list (sp,lobj) =
   let tag = object_tag lobj in
   match (sp,tag) with
-  | (_, "VARIABLE") -> variable_to_ast_list sp
+  | (_, "VARIABLE") -> variable_to_ast_list (basename sp)
   | (_, ("CONSTANT"|"PARAMETER")) -> constant_to_ast_list sp
   | (_, "INDUCTIVE") -> inductive_to_ast_list sp
   | (_, s) -> 
@@ -228,8 +223,8 @@ let name_to_ast (qid:Nametab.qualid) =
   	with Not_found -> 
 	  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
 	    let dir,name = Nametab.repr_qualid qid in 
-	      if dir <> make_dirpath [] then raise Not_found;
-	      let (c,typ) = Global.lookup_named name in 
+	      if (repr_dirpath dir) <> [] then raise Not_found;
+	      let (_,c,typ) = Global.lookup_named name in 
 		(match c with
 		     None -> make_variable_ast name typ []
 		   | Some c1 -> make_definition_ast name c1 typ [])
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 42daf3c19..6b2e38873 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -292,14 +292,9 @@ let parse_file_action reqid file_name =
 (* This function is taken from Mltop.add_path *)
 
 let add_path dir coq_dirpath =
-(*
-  if coq_dirpath = Names.make_dirpath [] then
-    anomaly "add_path: empty path in library";
-*)
   if exists_dir dir then
     begin
-      Library.add_load_path_entry (dir,coq_dirpath);
-      Nametab.push_library_root coq_dirpath
+      Library.add_load_path_entry (dir,coq_dirpath)
     end
   else
     wARNING [< 'sTR ("Cannot open " ^ dir) >]
@@ -309,18 +304,15 @@ let convert_string d =
   with _ -> failwith "caught"
 
 let add_rec_path dir coq_dirpath =
-(*
-  if coq_dirpath = Names.make_dirpath [] then anomaly "add_path: empty path in library";
-*)
   let dirs = all_subdirs dir in
   let prefix = Names.repr_dirpath coq_dirpath in
   if dirs <> [] then
     let convert_dirs (lp,cp) =
-      (lp,Names.make_dirpath (prefix@(List.map convert_string cp))) in
+      (lp,
+       Names.make_dirpath ((List.map convert_string (List.rev cp))@prefix)) in
     let dirs = map_succeed convert_dirs dirs in
     begin
-      List.iter Library.add_load_path_entry dirs;
-      Nametab.push_library_root coq_dirpath
+      List.iter Library.add_load_path_entry dirs
     end
     else
       wARNING [< 'sTR ("Cannot open " ^ dir) >];;
@@ -380,9 +372,9 @@ Libobject.relax true;
        else
 	 (mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in
      begin
-       add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nametab.coq_root]);
-       add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nametab.coq_root]);
-       add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nametab.coq_root]);
+       add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]);
+       add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]);
+       add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]);
        List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
      end;
 (try 
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 4ece713f5..13e307a47 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -75,7 +75,7 @@ let make_final_cmd f optname clear_names constr path =
     add_clear_names_if_necessary (f optname constr path) clear_names;;
 
 let (rem_cast:pbp_rule) = function
-    (a,c,cf,o, IsCast(f,_), p, func) ->
+    (a,c,cf,o, Cast(f,_), p, func) ->
       Some(func a c cf o (kind_of_term f) p)
   | _ -> None;;
 
@@ -84,7 +84,7 @@ let (forall_intro: pbp_rule) = function
    clear_names,
    clear_flag,
    None,
-   IsProd(Name x, _, body),
+   Prod(Name x, _, body),
    (2::path),
    f) ->
      let x' = next_global_ident_away x avoid in
@@ -95,7 +95,7 @@ let (forall_intro: pbp_rule) = function
 
 let (imply_intro2: pbp_rule) = function
   avoid, clear_names,
-  clear_flag, None, IsProd(Anonymous, _, body), 2::path, f ->
+  clear_flag, None, Prod(Anonymous, _, body), 2::path, f ->
    let h' = next_global_ident_away (id_of_string "H") avoid in
      Some(Node(zz, "TACTICLIST",
             [make_named_intro (string_of_id h');
@@ -105,7 +105,7 @@ let (imply_intro2: pbp_rule) = function
 
 let (imply_intro1: pbp_rule) = function
   avoid, clear_names,
-  clear_flag, None, IsProd(Anonymous, prem, body), 1::path, f ->
+  clear_flag, None, Prod(Anonymous, prem, body), 1::path, f ->
    let h' = next_global_ident_away (id_of_string "H") avoid in
    let str_h' = (string_of_id h') in
      Some(Node(zz, "TACTICLIST",
@@ -117,7 +117,7 @@ let (imply_intro1: pbp_rule) = function
 
 let (forall_elim: pbp_rule) = function
   avoid, clear_names, clear_flag, 
-  Some h, IsProd(Name x, _, body), 2::path, f ->
+  Some h, Prod(Name x, _, body), 2::path, f ->
   let h' = next_global_ident_away (id_of_string "H") avoid in
   let clear_names' = if clear_flag then h::clear_names else clear_names in
   let str_h' = (string_of_id h') in
@@ -135,7 +135,7 @@ let (forall_elim: pbp_rule) = function
           
 let (imply_elim1: pbp_rule) = function
   avoid, clear_names, clear_flag,
-  Some h, IsProd(Anonymous, prem, body), 1::path, f ->
+  Some h, Prod(Anonymous, prem, body), 1::path, f ->
   let clear_names' = if clear_flag then h::clear_names else clear_names in
   let h' = next_global_ident_away (id_of_string "H") avoid in
   let str_h' = (string_of_id h') in
@@ -156,7 +156,7 @@ let (imply_elim1: pbp_rule) = function
 
 let (imply_elim2: pbp_rule) = function
   avoid, clear_names, clear_flag,
-  Some h, IsProd(Anonymous, prem, body), 2::path, f ->
+  Some h, Prod(Anonymous, prem, body), 2::path, f ->
   let clear_names' = if clear_flag then h::clear_names else clear_names in
   let h' = next_global_ident_away (id_of_string "H") avoid in
   let str_h' = (string_of_id h') in
@@ -176,7 +176,8 @@ let (imply_elim2: pbp_rule) = function
   | _ -> None;;
 
 let reference dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::[dir])) in
+  let dir = make_dirpath 
+              (List.map id_of_string (List.rev ("Coq"::"Init"::[dir]))) in
   let id = id_of_string s in
   try 
     Nametab.locate_in_absolute_module dir id
@@ -204,7 +205,7 @@ let is_matching_local a b = is_matching (pattern_of_constr a) b;;
 
 let (and_intro: pbp_rule) = function
     avoid, clear_names, clear_flag,
-    None, IsApp(and_oper, [|c1; c2|]), 2::a::path, f 
+    None, App(and_oper, [|c1; c2|]), 2::a::path, f 
       ->
       if ((is_matching_local (andconstr()) and_oper) or
           (is_matching_local (prodconstr ()) and_oper)) & (a = 1 or a = 2) then
@@ -229,12 +230,12 @@ let (and_intro: pbp_rule) = function
 
 let (ex_intro: pbp_rule) = function
     avoid, clear_names, clear_flag, None,
-    IsApp(oper, [| c1; c2|]), 2::2::2::path, f
+    App(oper, [| c1; c2|]), 2::2::2::path, f
       when (is_matching_local (exconstr ()) oper) or (is_matching_local (exTconstr ()) oper)
  	or (is_matching_local (sigconstr ()) oper)
 	      or (is_matching_local (sigTconstr ()) oper) ->
 		(match kind_of_term c2 with
-		  IsLambda(Name x, _, body) ->
+		  Lambda(Name x, _, body) ->
 		    Some(Node(zz, "Split",
 			      [Node(zz, "BINDINGS",
 				    [Node(zz, "BINDING",
@@ -250,7 +251,7 @@ let (ex_intro: pbp_rule) = function
 
 let (or_intro: pbp_rule) = function
     avoid, clear_names, clear_flag, None,
-    IsApp(or_oper, [|c1; c2 |]), 2::a::path, f ->
+    App(or_oper, [|c1; c2 |]), 2::a::path, f ->
       if ((is_matching_local (orconstr ()) or_oper) or
         (is_matching_local (sumboolconstr ()) or_oper) or 
 	(is_matching_local (sumconstr ()) or_oper))
@@ -270,7 +271,7 @@ let dummy_id = id_of_string "Dummy";;
 
 let (not_intro: pbp_rule) = function
     avoid, clear_names, clear_flag, None,
-    IsApp(not_oper, [|c1|]), 2::1::path, f ->
+    App(not_oper, [|c1|]), 2::1::path, f ->
       if(is_matching_local (notconstr ()) not_oper) or 
 	(is_matching_local (notTconstr ()) not_oper) then
 	let h' = next_global_ident_away (id_of_string "H") avoid in
@@ -336,11 +337,11 @@ let rec down_prods: (types, constr) kind_of_term * (int list) * int ->
            string list * (int list) * int * (types, constr) kind_of_term *
   (int list) = 
    function
-     IsProd(Name x, _, body), 2::path, k ->
+     Prod(Name x, _, body), 2::path, k ->
 	let res_sl, res_il, res_i, res_cstr, res_p 
 	    = down_prods (kind_of_term body, path, k+1) in
 	(string_of_id x)::res_sl, (k::res_il), res_i, res_cstr, res_p
-   | IsProd(Anonymous, _, body), 2::path, k ->
+   | Prod(Anonymous, _, body), 2::path, k ->
         let res_sl, res_il, res_i, res_cstr, res_p 
 	    = down_prods (kind_of_term body, path, k+1) in
 	res_sl, res_il, res_i+1, res_cstr, res_p
@@ -361,14 +362,14 @@ let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) =
      | [] -> []
      | p::tl -> if n = p then tl else p::(delete n tl) in
    let rec check_rec l = function
-   | IsApp(f, array) ->
+   | App(f, array) ->
        Array.fold_left (fun l c -> check_rec l (kind_of_term c))
 	 (check_rec l (kind_of_term f)) array
-   | IsConst _ -> l
-   | IsMutInd _ -> l
-   | IsMutConstruct _ -> l
-   | IsVar _ -> l
-   | IsRel p ->
+   | Const _ -> l
+   | Ind _ -> l
+   | Construct _ -> l
+   | Var _ -> l
+   | Rel p ->
        let result = delete p l in
        if result = [] then
 	 raise (Pbp_internal [])
@@ -399,7 +400,7 @@ let (head_tactic_patt: pbp_rule) = function
     avoid, clear_names, clear_flag, Some h, cstr, path, f ->
     (match down_prods (cstr, path, 0) with
     | (str_list, _, nprems, 
-       IsApp(oper,[|c1|]), 2::1::path) 
+       App(oper,[|c1|]), 2::1::path) 
       	when
  	  (is_matching_local (notconstr ()) oper) or
  	  (is_matching_local (notTconstr ()) oper) ->
@@ -407,7 +408,7 @@ let (head_tactic_patt: pbp_rule) = function
 		   [elim_with_bindings h str_list;
 		     f avoid clear_names false None (kind_of_term c1) path]))
     | (str_list, _, nprems, 
-       IsApp(oper, [|c1; c2|]), 2::a::path) 
+       App(oper, [|c1; c2|]), 2::a::path) 
       when ((is_matching_local (andconstr()) oper) or
 	    (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
 	let h1 = next_global_ident_away (id_of_string "H") avoid in
@@ -431,18 +432,18 @@ let (head_tactic_patt: pbp_rule) = function
 			   cont_tac::(auxiliary_goals
 					clear_names clear_flag
 					h nprems))]))
-    | (str_list, _, nprems, IsApp(oper,[|c1; c2|]), 2::a::path)
+    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
       when ((is_matching_local (exconstr ()) oper) or
 	    (is_matching_local (exTconstr ()) oper) or
 	    (is_matching_local (sigconstr ()) oper) or
 	    (is_matching_local (sigTconstr()) oper)) & a = 2 ->
 		   (match (kind_of_term c2),path with
-		     IsLambda(Name x, _,body), (2::path) ->
+		     Lambda(Name x, _,body), (2::path) ->
 		       Some(Node(zz,"TACTICLIST",
 		    		 [elim_with_bindings h str_list;
 				   let x' = next_global_ident_away x avoid in
 				   let cont_body =
-				     IsProd(Name x', c1,
+				     Prod(Name x', c1,
 					    mkProd(Anonymous, body, 
 						   mkVar(dummy_id))) in
 				   let cont_tac 
@@ -456,7 +457,7 @@ let (head_tactic_patt: pbp_rule) = function
 						       clear_names clear_flag
 						       h nprems))]))
 		   | _ -> None)
-    | (str_list, _, nprems, IsApp(oper,[|c1; c2|]), 2::a::path)
+    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
 	when ((is_matching_local (orconstr ()) oper) or
               (is_matching_local (sumboolconstr ()) oper) or
 	      (is_matching_local (sumconstr ()) oper)) &
@@ -491,7 +492,7 @@ let (head_tactic_patt: pbp_rule) = function
 				   false "dummy" nprems))]))
     | (str_list, int_list, nprems, c, []) 
         when  (check_apply c (mk_db_indices int_list nprems)) &
-              (match c with IsProd(_,_,_) -> false
+              (match c with Prod(_,_,_) -> false
               |  _ -> true) &
               (List.length int_list) + nprems > 0 ->
           Some(add_clear_names_if_necessary
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 50aebb917..e4d4647f1 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -5,19 +5,22 @@ open Coqast;;
 open Environ
 open Evd
 open Names
+open Nameops
 open Stamps
 open Term
+open Termops
 open Util
 open Proof_type
 open Coqast
 open Pfedit
 open Translate
 open Term
-open Reduction
+open Reductionops
 open Clenv
 open Astterm
 open Typing
 open Inductive
+open Inductiveops
 open Vernacinterp
 open Declarations
 open Showproof_ct
@@ -205,7 +208,7 @@ let fill_unproved nt l =
 let new_sign osign sign =
     let res=ref [] in
     List.iter (fun (id,c,ty) ->
-		   try (let  ty1= (lookup_id_type id osign) in
+		   try (let  (_,_,ty1)= (lookup_named id osign) in
 			())
 		   with Not_found -> res:=(id,c,ty)::(!res))
               sign;
@@ -215,7 +218,7 @@ let new_sign osign sign =
 let old_sign osign sign =
     let res=ref [] in
     List.iter (fun (id,c,ty) ->
-		   try (let  ty1= (lookup_id_type id osign) in
+		   try (let (_,_,ty1) = (lookup_named id osign) in
 			if ty1 = ty then res:=(id,c,ty)::(!res))
 		   with Not_found -> ())
               sign;
@@ -711,7 +714,7 @@ let sort_of_type t ts =
        match ts with
          Prop(Null) -> Nformula
         |_ -> (match (kind_of_term t) with
-                IsProd(_,_,_) -> Nfunction
+                Prod(_,_,_) -> Nfunction
                |_ -> Ntype)
 ;;
 
@@ -722,22 +725,22 @@ let adrel (x,t) e =
 
 let rec nsortrec vl x = 
      match (kind_of_term x) with
-     IsProd(n,t,c)->
+     Prod(n,t,c)->
         let vl = (adrel (n,t) vl) in nsortrec vl c
-   | IsLambda(n,t,c) ->
+   | Lambda(n,t,c) ->
         let vl = (adrel (n,t) vl) in nsortrec vl c
-   | IsApp(f,args) -> nsortrec vl f
-   | IsSort(Prop(Null)) -> Prop(Null)
-   | IsSort(c) -> c
-   | IsMutInd(ind) ->
-          let dmi = lookup_mind_specif ind vl in
-          (mis_sort dmi)
-   | IsMutConstruct(c) ->
-          nsortrec vl (mkMutInd (inductive_of_constructor c))
-   | IsMutCase(_,x,t,a) 
+   | App(f,args) -> nsortrec vl f
+   | Sort(Prop(Null)) -> Prop(Null)
+   | Sort(c) -> c
+   | Ind(ind) ->
+          let (mib,mip) = lookup_mind_specif vl ind in
+          mip.mind_sort
+   | Construct(c) ->
+          nsortrec vl (mkInd (inductive_of_constructor c))
+   | Case(_,x,t,a) 
         -> nsortrec vl x
-   | IsCast(x,t)-> nsortrec vl t
-   | IsConst c  -> nsortrec vl (lookup_constant c vl).const_type
+   | Cast(x,t)-> nsortrec vl t
+   | Const c  -> nsortrec vl (lookup_constant c vl).const_type
    | _ -> nsortrec vl (type_of vl Evd.empty x)
 ;;
 let nsort x =
@@ -1056,7 +1059,7 @@ let first_name_hyp_of_ntree {t_goal={newhyp=lh}}=
 
 let rec find_type x t=
     match (kind_of_term (strip_outer_cast t)) with 
-      IsProd(y,ty,t) ->
+      Prod(y,ty,t) ->
 	(match y with
 	  Name y -> 
             if x=(string_of_id y) then ty
@@ -1071,9 +1074,9 @@ Traitement des égalités
 (*
 let is_equality e =
    match  (kind_of_term e) with
-     IsAppL args ->
+     AppL args ->
        (match (kind_of_term args.(0)) with
-	 IsConst (c,_) ->
+	 Const (c,_) ->
 	   (match (string_of_sp c) with
 	     "Equal" -> true
            | "eq" -> true
@@ -1088,14 +1091,14 @@ let is_equality e =
 let is_equality e =
   let e= (strip_outer_cast e) in
    match  (kind_of_term e) with
-     IsApp (f,args) -> (Array.length args) >= 3
+     App (f,args) -> (Array.length args) >= 3
    | _ -> false
 ;;
 
 let terms_of_equality e =
   let e= (strip_outer_cast e) in
   match  (kind_of_term e) with
-     IsApp (f,args) -> (args.(1) , args.(2))
+     App (f,args) -> (args.(1) , args.(2))
     | _ -> assert false
 ;;
 
@@ -1404,22 +1407,24 @@ and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
 and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
 and prod_head t =
   match (kind_of_term (strip_outer_cast t)) with 
-     IsProd(_,_,c) -> prod_head c
-(*    |IsApp(f,a) -> f *)
+     Prod(_,_,c) -> prod_head c
+(*    |App(f,a) -> f *)
     | _ -> t
 and string_of_sp sp = string_of_id (basename sp)
-and  constr_of_mind dmi i = (string_of_id (mis_consnames dmi).(i-1))
-and arity_of_constr_of_mind indf i =
-     (get_constructors indf).(i-1).cs_nargs
+and constr_of_mind mip i =
+  (string_of_id mip.mind_consnames.(i-1))
+and arity_of_constr_of_mind env indf i =
+     (get_constructors env indf).(i-1).cs_nargs
 and gLOB ge = Global.env_of_context ge  (* (Global.env()) *)
 
 and natural_case ig lh g gs ge arg1 ltree with_intros =
  let env= (gLOB ge) in
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors indf) in
- let IndFamily(dmi,_) = indf in
- let ti =(string_of_id (mis_typename dmi)) in
+ let ncti= Array.length(get_constructors env indf) in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) in
  let type_arg= targ1 (* List.nth targ (mis_index dmi)*)  in
  if  ncti<>1
 (* Zéro ou Plusieurs constructeurs *)
@@ -1436,9 +1441,9 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
             (let ci=ref 0 in
              (prli
                  (fun treearg -> ci:=!ci+1;
-                      let nci=(constr_of_mind dmi !ci) in
+                      let nci=(constr_of_mind mip !ci) in
                       let aci=if with_intros
-			      then (arity_of_constr_of_mind indf !ci)
+			      then (arity_of_constr_of_mind env indf !ci)
 		              else 0 in
                       let ici= (!ci) in
                     sph[ (natural_ntree  
@@ -1464,10 +1469,10 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
        (show_goal2 lh ig g gs "");
        de_A_on_a arg1;
        (let treearg=List.hd ltree in
-       let nci=(constr_of_mind dmi 1) in
+       let nci=(constr_of_mind mip 1) in
        let aci=
 	 if with_intros
-         then (arity_of_constr_of_mind indf 1)
+         then (arity_of_constr_of_mind env indf 1)
 	 else 0 in
        let ici= 1 in
        sph[ (natural_ntree  
@@ -1493,21 +1498,25 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
 *)
 and prod_list_var t =
    match (kind_of_term (strip_outer_cast t)) with 
-      IsProd(_,t,c) -> t::(prod_list_var c)
+      Prod(_,t,c) -> t::(prod_list_var c)
      |_ -> []
 and  hd_is_mind t ti =
-    try (let IndType (indf,targ) = find_rectype (Global.env()) Evd.empty t in
-	     let ncti= Array.length(get_constructors indf) in
-	     let IndFamily(dmi,_) = indf in
-	     (string_of_id (mis_typename dmi)) = ti)
+    try (let env = Global.env() in
+         let IndType (indf,targ) = find_rectype env Evd.empty t in
+	 let ncti= Array.length(get_constructors env indf) in
+	 let (ind,_) = indf in
+         let (mib,mip) = lookup_mind_specif env ind in
+	 (string_of_id mip.mind_typename) = ti)
     with _ -> false
 and mind_ind_info_hyp_constr indf c =
-  let IndFamily(dmi,_) = indf in
-  let p= mis_nparams dmi in
-  let a=arity_of_constr_of_mind indf c in
-  let lp=ref (get_constructors indf).(c).cs_args in
+  let env = Global.env() in
+  let (ind,_) = indf in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let p = mip.mind_nparams in
+  let a = arity_of_constr_of_mind env indf c in
+  let lp=ref (get_constructors env indf).(c).cs_args in
   let lr=ref [] in
-  let ti = (string_of_id (mis_typename dmi)) in
+  let ti = (string_of_id mip.mind_typename) in
   for i=1 to a do
      match !lp with
      ((_,_,t)::lp1)->
@@ -1530,9 +1539,10 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
  let env= (gLOB ge) in
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors indf) in
- let IndFamily(dmi,_) = indf in
- let ti =(string_of_id (mis_typename dmi)) in
+ let ncti= Array.length(get_constructors env indf) in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) in
  let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
   spv
          [  (natural_lhyp lh ig.ihsg);
@@ -1543,8 +1553,8 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
             (let ci=ref 0 in
              (prli
                  (fun treearg -> ci:=!ci+1;
-                      let nci=(constr_of_mind dmi !ci) in
-                      let aci=(arity_of_constr_of_mind indf !ci) in
+                      let nci=(constr_of_mind mip !ci) in
+                      let aci=(arity_of_constr_of_mind env indf !ci) in
                       let hci=
 			if with_intros
 			then mind_ind_info_hyp_constr indf  !ci
@@ -1575,13 +1585,14 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros=
  let env = (gLOB (g_env (List.hd ltree))) in
  let arg1=dbize env arg1 in
  let arg2 = match (kind_of_term arg1) with
-       IsVar(arg2) -> arg2
+       Var(arg2) -> arg2
       | _ -> assert false in
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors indf) in
- let IndFamily(dmi,_) = indf in
- let ti =(string_of_id (mis_typename dmi)) in
+ let ncti= Array.length(get_constructors env indf) in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) in
  let type_arg= targ1(*List.nth targ (mis_index dmi)*) in
 
  let lh1= hyps (List.hd ltree) in (* la liste des hyp jusqu'a n *)
@@ -1604,8 +1615,8 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros=
             (let ci=ref 0 in
              (prli
                  (fun treearg -> ci:=!ci+1;
-                      let nci=(constr_of_mind dmi !ci) in
-                      let aci=(arity_of_constr_of_mind indf !ci) in
+                      let nci=(constr_of_mind mip !ci) in
+                      let aci=(arity_of_constr_of_mind env indf !ci) in
                       let hci= 
 			if with_intros
 			then mind_ind_info_hyp_constr indf  !ci
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index e35b9d3bc..778220322 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -26,10 +26,9 @@ and fAST = function
    fID x1;
    fAST_LIST x2;
    fNODE "astnode" 2
-| CT_astpath(x1, x2) ->
+| CT_astpath(x1) ->
    fID_LIST x1;
-   fID x2;
-   fNODE "astpath" 2
+   fNODE "astpath" 1
 | CT_astslam(x1, x2) ->
    fID_OPT x1;
    fAST x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ccaa08f50..c7552847f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -381,18 +381,18 @@ let xlate_op the_node opn a b =
       *)
    "CONST" ->
   (match a, b with
-  | ((Path (_, sl, kind)) :: []), [] ->
+  | ((Path (_, sl)) :: []), [] ->
     CT_coerce_ID_to_FORMULA(CT_ident
-       (Names.string_of_id (Names.basename (section_path sl kind))))
-  | ((Path (_, sl, kind)) :: []), tl ->
+       (Names.string_of_id (Nameops.basename (section_path sl))))
+  | ((Path (_, sl)) :: []), tl ->
  CT_coerce_ID_to_FORMULA(CT_ident   
-       (Names.string_of_id(Names.basename (section_path sl kind))))
+       (Names.string_of_id(Nameops.basename (section_path sl))))
   | _, _ -> xlate_error "xlate_op : CONST")
  | (** string_of_path needs to be investigated.
     *)
  "MUTIND" ->
      (match a, b with
-  	| [Path(_, sl, kind); Num(_, tyi)], [] ->
+  	| [Path(_, sl); Num(_, tyi)], [] ->
 	    if !in_coq_ref then
 	      match special_case_qualid ()
 		(!xlate_mut_stuff (Node((0,0),"MUTIND", a))) with
@@ -401,8 +401,7 @@ let xlate_op the_node opn a b =
 	    else
 	    CT_coerce_ID_to_FORMULA(
 	      CT_ident(Names.string_of_id
-			 (Names.basename
-			    (section_path sl kind))))
+			 (Nameops.basename (section_path sl))))
   	| _, _ -> xlate_error "xlate_op : MUTIND")
  | "MUTCASE" 
  | "CASE" ->
@@ -417,7 +416,7 @@ let xlate_op the_node opn a b =
       *)
    "MUTCONSTRUCT" ->
   (match a, b with
-	  | [Path(_, sl, kind);Num(_, tyi);Num(_, n)], cl ->
+	  | [Path(_, sl);Num(_, tyi);Num(_, n)], cl ->
    if !in_coq_ref then
      match
        special_case_qualid ()
@@ -425,7 +424,7 @@ let xlate_op the_node opn a b =
 	 | Some(Rform x) -> x
 	 | _ -> assert false
    else
-   let name = Names.string_of_path (section_path sl kind) in
+   let name = Names.string_of_path (section_path sl) in
      (* This is rather a patch to cope with the fact that identifier
         names have disappeared from the vo files for grammar rules *)
        let type_desc = (try Some (Hashtbl.find type_table name) with
@@ -1512,9 +1511,9 @@ let xlate_ast =
       CT_coerce_ID_OR_STRING_to_AST
        (CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
      | Dynamic(_,_) -> failwith "Dynamics not treated in xlate_ast"
-     | Path (_, sl, s) ->
+     | Path (_, sl) ->
       CT_astpath
-       (CT_id_list (List.map (function s -> CT_ident s) sl), CT_ident s) in
+       (CT_id_list (List.map (function s -> CT_ident s) sl)) in
  xlate_ast_aux;;
 
 let get_require_flags impexp spec =
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index d12f868ac..8e1d90489 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -21,7 +21,10 @@ open Reduction
 open Proof_type
 open Ast
 open Names
+open Nameops
 open Term
+open Termops
+open Declarations
 open Environ
 open Sign
 open Inductive
@@ -30,6 +33,7 @@ open Evar_refiner
 open Tactics
 open Clenv
 open Logic
+open Nametab
 open Omega
 
 (* Added by JCF, 09/03/98 *)
@@ -97,24 +101,24 @@ let reduce_to_mind gl t =
   let rec elimrec t l =
     let c, args = whd_stack t in
     match kind_of_term c, args with
-    | (IsMutInd ind,_) -> (ind,Environ.it_mkProd_or_LetIn t l)
-    | (IsConst _,_) -> 
+    | (Ind ind,_) -> (ind,Environ.it_mkProd_or_LetIn t l)
+    | (Const _,_) -> 
 	(try 
 	   let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l
          with e when catchable_exception e -> 
 	   errorlabstrm "tactics__reduce_to_mind"
              [< 'sTR"Not an inductive product" >])
-    | (IsMutCase _,_) ->
+    | (Case _,_) ->
 	(try 
 	   let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l
          with e when catchable_exception e -> 
 	   errorlabstrm "tactics__reduce_to_mind"
              [< 'sTR"Not an inductive product" >])
-    | (IsCast (c,_),[]) -> elimrec c l
-    | (IsProd (n,ty,t'),[]) -> 
+    | (Cast (c,_),[]) -> elimrec c l
+    | (Prod (n,ty,t'),[]) -> 
 	let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
 	elimrec t' ((n,None,ty')::l)
-    | (IsLetIn (n,b,ty,t'),[]) ->
+    | (LetIn (n,b,ty,t'),[]) ->
 	let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
 	elimrec t' ((n,Some b,ty')::l)
     | _ -> error "Not an inductive product"
@@ -127,7 +131,8 @@ let reduce_to_mind = pf_reduce_to_quantified_ind
 let constructor_tac nconstropt i lbind gl = 
   let cl = pf_concl gl in
   let (mind, redcl) = reduce_to_mind gl cl in
-  let nconstr = Global.mind_nconstr mind
+  let (mib,mip) = Global.lookup_inductive mind in
+  let nconstr = Array.length mip.mind_consnames
   and sigma = project gl in
   (match nconstropt with 
      | Some expnconstr -> 
@@ -135,7 +140,7 @@ let constructor_tac nconstropt i lbind gl =
            error "Not the expected number of constructors"
      | _ -> ());
   if i > nconstr then error "Not enough Constructors";
-  let c = mkMutConstruct (ith_constructor_of_inductive mind i) in 
+  let c = mkConstruct (ith_constructor_of_inductive mind i) in 
   let resolve_tac = resolve_with_bindings_tac (c,lbind) in
   (tclTHEN (tclTHEN (change_in_concl redcl) intros) resolve_tac) gl
 
@@ -169,7 +174,7 @@ let hide_constr,find_constr,clear_tables,dump_tables =
   (fun () -> l := []),
   (fun () -> !l)
 
-let get_applist = whd_stack
+let get_applist = decompose_app
 
 exception Destruct
 
@@ -177,12 +182,12 @@ let dest_const_apply t =
   let f,args = get_applist t in
   let ref = 
   match kind_of_term f with 
-    | IsConst sp         -> ConstRef sp
-    | IsMutConstruct csp -> ConstructRef csp
-    | IsMutInd isp       -> IndRef isp
+    | Const sp         -> ConstRef sp
+    | Construct csp -> ConstructRef csp
+    | Ind isp       -> IndRef isp
     | _ -> raise Destruct
   in
-  basename (Global.sp_of_global ref), args
+  id_of_global (Global.env()) ref, args
 
 type result = 
   | Kvar of string
@@ -192,17 +197,17 @@ type result =
 
 let destructurate t =
   let c, args = get_applist t in
+  let env = Global.env() in
   match kind_of_term c, args with
-    | IsConst sp, args ->
-	Kapp (string_of_id (basename (Global.sp_of_global (ConstRef sp))),args)
-    | IsMutConstruct csp , args ->
-	Kapp (string_of_id (basename (Global.sp_of_global (ConstructRef csp))),
-			    args)
-    | IsMutInd isp, args ->
-	Kapp (string_of_id (basename (Global.sp_of_global (IndRef isp))),args)
-    | IsVar id,[] -> Kvar(string_of_id id)
-    | IsProd (Anonymous,typ,body), [] -> Kimp(typ,body)
-    | IsProd (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
+    | Const sp, args ->
+	Kapp (string_of_id (id_of_global env (ConstRef sp)),args)
+    | Construct csp , args ->
+	Kapp (string_of_id (id_of_global env(ConstructRef csp)), args)
+    | Ind isp, args ->
+	Kapp (string_of_id (id_of_global env (IndRef isp)),args)
+    | Var id,[] -> Kvar(string_of_id id)
+    | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
+    | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
 let recognize_number t =
@@ -225,7 +230,7 @@ let recognize_number t =
  This is the right way to access to Coq constants in tactics ML code *)
 
 let constant dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
+  let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
@@ -389,7 +394,7 @@ let coq_imp_simp = lazy (logic_constant ["Decidable"] "imp_simp")
 (* Section paths for unfold *)
 open Closure
 let make_coq_path dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
+  let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in
   let id = id_of_string s in
   let ref = 
     try Nametab.locate_in_absolute_module dir id 
@@ -441,7 +446,7 @@ type constr_path =
   (* Abstraction and product *)
   | P_BODY 
   | P_TYPE
-  (* Mutcase *)
+  (* Case *)
   | P_BRANCH of int
   | P_ARITY
   | P_ARG
@@ -449,37 +454,37 @@ type constr_path =
 let context operation path (t : constr) =
   let rec loop i p0 t = 
     match (p0,kind_of_term t) with 
-      | (p, IsCast (c,t)) -> mkCast (loop i p c,t)
+      | (p, Cast (c,t)) -> mkCast (loop i p c,t)
       | ([], _) -> operation i t
-      | ((P_APP n :: p),  IsApp (f,v)) ->
+      | ((P_APP n :: p),  App (f,v)) ->
 (*	  let f,l = get_applist t in   NECESSAIRE ??
 	  let v' = Array.of_list (f::l) in  *)
 	  let v' = Array.copy v in
 	  v'.(n-1) <- loop i p v'.(n-1); mkApp (f, v')
-      | ((P_BRANCH n :: p), IsMutCase (ci,q,c,v)) ->
+      | ((P_BRANCH n :: p), Case (ci,q,c,v)) ->
 	  (* avant, y avait mkApp... anyway, BRANCH seems nowhere used *)
 	  let v' = Array.copy v in
-	  v'.(n) <- loop i p v'.(n); (mkMutCase (ci,q,c,v'))
-      | ((P_ARITY :: p),  IsApp (f,l)) ->
+	  v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v'))
+      | ((P_ARITY :: p),  App (f,l)) ->
 	  appvect (loop i p f,l)
-      | ((P_ARG :: p),  IsApp (f,v)) ->
+      | ((P_ARG :: p),  App (f,v)) ->
 	  let v' = Array.copy v in
 	  v'.(0) <- loop i p v'.(0); mkApp (f,v')
-      | (p, IsFix ((_,n as ln),(tys,lna,v))) ->
+      | (p, Fix ((_,n as ln),(tys,lna,v))) ->
 	  let l = Array.length v in
 	  let v' = Array.copy v in
 	  v'.(n) <- loop (i+l) p v.(n); (mkFix (ln,(tys,lna,v')))
-      | ((P_BODY :: p), IsProd (n,t,c)) ->
+      | ((P_BODY :: p), Prod (n,t,c)) ->
 	  (mkProd (n,t,loop (i+1) p c))
-      | ((P_BODY :: p), IsLambda (n,t,c)) ->
+      | ((P_BODY :: p), Lambda (n,t,c)) ->
 	  (mkLambda (n,t,loop (i+1) p c))
-      | ((P_BODY :: p), IsLetIn (n,b,t,c)) ->
+      | ((P_BODY :: p), LetIn (n,b,t,c)) ->
 	  (mkLetIn (n,b,t,loop (i+1) p c))
-      | ((P_TYPE :: p), IsProd (n,t,c)) ->
+      | ((P_TYPE :: p), Prod (n,t,c)) ->
 	  (mkProd (n,loop i p t,c))
-      | ((P_TYPE :: p), IsLambda (n,t,c)) ->
+      | ((P_TYPE :: p), Lambda (n,t,c)) ->
 	  (mkLambda (n,loop i p t,c))
-      | ((P_TYPE :: p), IsLetIn (n,b,t,c)) ->
+      | ((P_TYPE :: p), LetIn (n,b,t,c)) ->
 	  (mkLetIn (n,b,loop i p t,c))
       | (p, _) -> 
 	  pPNL [<Printer.prterm t>];
@@ -489,19 +494,19 @@ let context operation path (t : constr) =
 
 let occurence path (t : constr) =
   let rec loop p0 t = match (p0,kind_of_term t) with
-    | (p, IsCast (c,t)) -> loop p c
+    | (p, Cast (c,t)) -> loop p c
     | ([], _) -> t
-    | ((P_APP n :: p),  IsApp (f,v)) -> loop p v.(n-1)
-    | ((P_BRANCH n :: p), IsMutCase (_,_,_,v)) -> loop p v.(n)
-    | ((P_ARITY :: p),  IsApp (f,_)) -> loop p f
-    | ((P_ARG :: p),  IsApp (f,v)) -> loop p v.(0)
-    | (p, IsFix((_,n) ,(_,_,v))) -> loop p v.(n)
-    | ((P_BODY :: p), IsProd (n,t,c)) -> loop p c
-    | ((P_BODY :: p), IsLambda (n,t,c)) -> loop p c
-    | ((P_BODY :: p), IsLetIn (n,b,t,c)) -> loop p c
-    | ((P_TYPE :: p), IsProd (n,term,c)) -> loop p term
-    | ((P_TYPE :: p), IsLambda (n,term,c)) -> loop p term
-    | ((P_TYPE :: p), IsLetIn (n,b,term,c)) -> loop p term
+    | ((P_APP n :: p),  App (f,v)) -> loop p v.(n-1)
+    | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n)
+    | ((P_ARITY :: p),  App (f,_)) -> loop p f
+    | ((P_ARG :: p),  App (f,v)) -> loop p v.(0)
+    | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n)
+    | ((P_BODY :: p), Prod (n,t,c)) -> loop p c
+    | ((P_BODY :: p), Lambda (n,t,c)) -> loop p c
+    | ((P_BODY :: p), LetIn (n,b,t,c)) -> loop p c
+    | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term
+    | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
+    | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
     | (p, _) -> 
 	pPNL [<Printer.prterm t>];
 	failwith ("occurence " ^ string_of_int(List.length p)) 
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index b87ec5861..10c05ec0e 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -120,7 +120,8 @@ open Proof_type
   the constants are loaded in the environment *)
 
 let constant dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::"ring"::dir)) in
+  let dir = make_dirpath
+              (List.map id_of_string (List.rev ("Coq"::"ring"::dir))) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
@@ -200,9 +201,9 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
 
 let compute_lhs typ i nargsi =
   match kind_of_term typ with
-    | IsMutInd(sp,0) -> 
+    | Ind(sp,0) -> 
         let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
-        mkApp (mkMutConstruct ((sp,0),i+1), argsi)
+        mkApp (mkConstruct ((sp,0),i+1), argsi)
     | _ -> i_can't_do_that ()
 
 (*s This function builds the pattern from the RHS. Recursive calls are
@@ -211,11 +212,11 @@ let compute_lhs typ i nargsi =
 let compute_rhs bodyi index_of_f =
   let rec aux c = 
     match decomp_term c with
-      | IsApp (j, args) when j = mkRel (index_of_f) (* recursive call *) -> 
+      | App (j, args) when j = mkRel (index_of_f) (* recursive call *) -> 
           let i = destRel (array_last args) in mkMeta i
-      | IsApp (f,args) ->
+      | App (f,args) ->
           mkApp (f, Array.map aux args)
-      | IsCast (c,t) -> aux c 
+      | Cast (c,t) -> aux c 
       | _ -> c
   in
   pattern_of_constr (aux bodyi)
@@ -224,13 +225,13 @@ let compute_rhs bodyi index_of_f =
 
 let compute_ivs gl f cs =
   let cst = try destConst f with _ -> i_can't_do_that () in
-  let body = constant_value (Global.env()) cst in
+  let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
-    | IsFix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
+    | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
         begin match decomp_term body3 with
-          | IsMutCase(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
+          | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
               let n_lhs_rhs = ref []
               and v_lhs = ref (None : constr option)
               and c_lhs = ref (None : constr option) in
@@ -246,7 +247,7 @@ let compute_ivs gl f cs =
                      c_lhs := Some (compute_lhs (snd (List.hd args3))
                                       i nargsi)
            (* Then we test if the RHS is the RHS for variables *)
-                   else begin match decomp_app bodyi with 
+                   else begin match decompose_app bodyi with 
                      | vmf, [_; _; a3; a4 ]
                          when isRel a3 & isRel a4 &
 			   pf_conv_x gl vmf 
@@ -267,7 +268,7 @@ let compute_ivs gl f cs =
 
 	      (* The Cases predicate is a lambda; we assume no dependency *)
 	      let p = match kind_of_term p with
-		| IsLambda (_,_,p) -> pop p
+		| Lambda (_,_,p) -> pop p
 		| _ -> p
 	      in
               
@@ -300,8 +301,8 @@ binary search trees (see file \texttt{Quote.v}) *)
 let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
-     | IsCast(c,_) -> closed_under cset c  
-     | IsApp(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
+     | Cast(c,_) -> closed_under cset c  
+     | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
      | _ -> false)
     
 (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
@@ -362,8 +363,8 @@ let path_of_int n =
 let rec subterm gl (t : constr) (t' : constr) = 
   (pf_conv_x gl t t') or
   (match (kind_of_term t) with 
-     | IsApp (f,args) -> array_exists (fun t -> subterm gl t t') args
-     | IsCast(t,_) -> (subterm gl t t')
+     | App (f,args) -> array_exists (fun t -> subterm gl t t') args
+     | Cast(t,_) -> (subterm gl t t')
      | _ -> false)
            
 (*s We want to sort the list according to reverse subterm order. *)
@@ -398,26 +399,26 @@ let quote_terms ivs lc gl=
             begin try 
               let s1 = matches rhs c in
               let s2 = List.map (fun (i,c_i) -> (i,aux c_i)) s1 in
-              Term.subst_meta s2 lhs
+              Termops.subst_meta s2 lhs
             with PatternMatchingFailure -> auxl tail
             end 
         |  [] -> 
              begin match ivs.variable_lhs with 
                | None -> 
                    begin match ivs.constant_lhs with
-                     | Some c_lhs -> Term.subst_meta [1, c] c_lhs
+                     | Some c_lhs -> Termops.subst_meta [1, c] c_lhs
                      | None -> anomaly "invalid inversion scheme for quote"
                    end
                | Some var_lhs -> 
                    begin match ivs.constant_lhs with
                      | Some c_lhs when closed_under ivs.constants c ->
-			 Term.subst_meta [1, c] c_lhs
+			 Termops.subst_meta [1, c] c_lhs
                      | _ -> 
 			 begin 
                            try Hashtbl.find varhash c 
                            with Not_found -> 
                              let newvar = 
-                               Term.subst_meta [1, (path_of_int !counter)] 
+                               Termops.subst_meta [1, (path_of_int !counter)] 
 				 var_lhs in
                              begin 
                                incr counter;
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 720c5a862..1043ecbdb 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -15,7 +15,8 @@ open Util
 open Options
 open Term
 open Names
-open Reduction
+open Nameops
+open Reductionops
 open Tacmach
 open Proof_type
 open Proof_trees
@@ -28,13 +29,14 @@ open Tacred
 open Tactics
 open Pattern 
 open Hiddentac
+open Nametab
 open Quote
 
 let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
 let constant dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
+  let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
@@ -138,6 +140,7 @@ val build_coq_eqT : constr delayed
 val build_coq_sym_eqT : constr delayed
 *)
 
+let mkLApp(fc,v) = mkApp(Lazy.force fc, v)
 
 (*********** Useful types and functions ************)
 
@@ -226,30 +229,31 @@ let unbox = function
 
 let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = 
   if theories_map_mem a then errorlabstrm "Add Semi Ring" 
-    [< 'sTR "A (Semi-)(Setoid-)Ring Structure is already declared for "; prterm a >];
+    [< 'sTR "A (Semi-)(Setoid-)Ring Structure is already declared for ";
+       prterm a >];
   let env = Global.env () in
     if (want_ring & want_setoid &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-		(mkApp (Lazy.force coq_Setoid_Ring_Theory, 
+		(mkLApp (coq_Setoid_Ring_Theory, 
 			[| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])))) &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
-		(mkApp ((Lazy.force coq_Setoid_Theory), [| a; (unbox aequiv) |]))))) then 
+		(mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then 
       errorlabstrm "addring" [< 'sTR "Not a valid Setoid-Ring theory" >];
     if (not want_ring & want_setoid &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-		(mkApp (Lazy.force coq_Semi_Setoid_Ring_Theory, 
+		(mkLApp (coq_Semi_Setoid_Ring_Theory, 
 			[| a; (unbox aequiv); aplus; amult; aone; azero; aeq|])))) &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
-		(mkApp ((Lazy.force coq_Setoid_Theory), [| a; (unbox aequiv) |]))))) then 
+		(mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then 
       errorlabstrm "addring" [< 'sTR "Not a valid Semi-Setoid-Ring theory" >];
     if (want_ring & not want_setoid &
 	not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-	       (mkApp (Lazy.force coq_Ring_Theory, 
+	       (mkLApp (coq_Ring_Theory, 
 		       [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])))) then
       errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >];
     if (not want_ring & not want_setoid &
 	not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
-	       (mkApp (Lazy.force coq_Semi_Ring_Theory, 
+	       (mkLApp (coq_Semi_Ring_Theory, 
 		       [| a; aplus; amult; aone; azero; aeq |])))) then 
       errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >];
     Lib.add_anonymous_leaf
@@ -437,17 +441,17 @@ let build_spolynom gl th lc =
      and builds the varmap with side-effects *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsApp (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
-	  mkAppA [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |]
-      | IsApp (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
-	  mkAppA [| Lazy.force coq_SPmult; th.th_a; aux c1; aux c2 |]
+      | App (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkLApp(coq_SPplus, [|th.th_a; aux c1; aux c2 |])
+      | App (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkLApp(coq_SPmult, [|th.th_a; aux c1; aux c2 |])
       | _ when closed_under th.th_closed c ->
-	  mkAppA [| Lazy.force coq_SPconst; th.th_a; c |]
+	  mkLApp(coq_SPconst, [|th.th_a; c |])
       | _ -> 
 	  try Hashtbl.find varhash c 
 	  with Not_found -> 
-	    let newvar = mkAppA [| Lazy.force coq_SPvar; th.th_a; 
-				   (path_of_int !counter) |] in
+	    let newvar =
+              mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in
 	    begin 
 	      incr counter;
 	      varlist := c :: !varlist;
@@ -459,18 +463,18 @@ let build_spolynom gl th lc =
   let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
   List.map 
     (fun p -> 
-       (mkAppA [| Lazy.force coq_interp_sp; th.th_a; th.th_plus; th.th_mult; 
-		  th.th_zero; v; p |],
-	mkAppA [| Lazy.force coq_interp_cs; th.th_a; th.th_plus; th.th_mult; 
-		  th.th_one; th.th_zero; v;
+       (mkLApp (coq_interp_sp,
+               [|th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
+	mkLApp (coq_interp_cs,
+               [|th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
 		  pf_reduce cbv_betadeltaiota gl 
-		    (mkAppA [| Lazy.force coq_spolynomial_simplify; 
-			       th.th_a; th.th_plus; th.th_mult; 
+		    (mkLApp (coq_spolynomial_simplify, 
+			    [| th.th_a; th.th_plus; th.th_mult; 
 			       th.th_one; th.th_zero; 
-			       th.th_eq; p|]) |],
-	mkAppA [| Lazy.force coq_spolynomial_simplify_ok;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
-		  th.th_eq; v; th.th_t; p |]))
+			       th.th_eq; p|])) |]),
+	mkLApp (coq_spolynomial_simplify_ok,
+	        [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+		  th.th_eq; v; th.th_t; p |])))
     lp
 
 (*
@@ -491,25 +495,26 @@ let build_polynom gl th lc =
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
-	  mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |]
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
-	  mkAppA [| Lazy.force coq_Pmult; th.th_a; aux c1; aux c2 |]
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |])
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |])
       (* The special case of Zminus *)
-      | IsApp (binop, [|c1; c2|])
-	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
-	                                 mkAppA [| (unbox th.th_opp); c2 |] |]) ->
-	    mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1;
-	              mkAppA [| Lazy.force coq_Popp; th.th_a; aux c2 |] |]
-      | IsApp (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
-	  mkAppA [| Lazy.force coq_Popp; th.th_a; aux c1 |]
+      | App (binop, [|c1; c2|])
+	  when pf_conv_x gl c
+            (mkApp (th.th_plus, [|c1; mkApp(unbox th.th_opp, [|c2|])|])) ->
+	    mkLApp(coq_Pplus,
+                  [|th.th_a; aux c1;
+	            mkLApp(coq_Popp, [|th.th_a; aux c2|]) |])
+      | App (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
+	  mkLApp(coq_Popp, [|th.th_a; aux c1|])
       | _ when closed_under th.th_closed c ->
-	  mkAppA [| Lazy.force coq_Pconst; th.th_a; c |]
+	  mkLApp(coq_Pconst, [|th.th_a; c |])
       | _ -> 
 	  try Hashtbl.find varhash c 
 	  with Not_found -> 
-	    let newvar = mkAppA [| Lazy.force coq_Pvar; th.th_a; 
-				   (path_of_int !counter) |] in
+	    let newvar =
+              mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in
 	    begin 
 	      incr counter;
 	      varlist := c :: !varlist;
@@ -521,18 +526,18 @@ let build_polynom gl th lc =
   let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
   List.map 
     (fun p -> 
-       (mkAppA [| Lazy.force coq_interp_p;
-		  th.th_a; th.th_plus; th.th_mult; th.th_zero; (unbox th.th_opp);
-		  v; p |],
-	mkAppA [| Lazy.force coq_interp_cs;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
+       (mkLApp(coq_interp_p,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
+                 (unbox th.th_opp); v; p |])),
+	mkLApp(coq_interp_cs,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
 		  pf_reduce cbv_betadeltaiota gl 
-		    (mkAppA [| Lazy.force coq_polynomial_simplify; 
-			       th.th_a; th.th_plus; th.th_mult; 
+		    (mkLApp(coq_polynomial_simplify,
+			    [| th.th_a; th.th_plus; th.th_mult; 
 			       th.th_one; th.th_zero; 
-			       (unbox th.th_opp); th.th_eq; p |]) |],
-	mkAppA [| Lazy.force coq_polynomial_simplify_ok;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+			       (unbox th.th_opp); th.th_eq; p |])) |]),
+	mkLApp(coq_polynomial_simplify_ok,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
 		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))
     lp
 
@@ -556,17 +561,16 @@ let build_aspolynom gl th lc =
      and builds the varmap with side-effects *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
-	  mkAppA [| Lazy.force coq_ASPplus; aux c1; aux c2 |]
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
-	  mkAppA [| Lazy.force coq_ASPmult; aux c1; aux c2 |]
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkLApp(coq_ASPplus, [| aux c1; aux c2 |])
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkLApp(coq_ASPmult, [| aux c1; aux c2 |])
       | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
       | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
       | _ -> 
 	  try Hashtbl.find varhash c 
 	  with Not_found -> 
-	    let newvar = mkAppA [| Lazy.force coq_ASPvar; 
-				   (path_of_int !counter) |] in
+	    let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in
 	    begin 
 	      incr counter;
 	      varlist := c :: !varlist;
@@ -578,15 +582,17 @@ let build_aspolynom gl th lc =
   let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
   List.map 
     (fun p -> 
-       (mkAppA [| Lazy.force coq_interp_asp; th.th_a; th.th_plus; th.th_mult; 
-		  th.th_one; th.th_zero; v; p |],
-	mkAppA [| Lazy.force coq_interp_acs; th.th_a; th.th_plus; th.th_mult; 
+       (mkLApp(coq_interp_asp,
+               [| th.th_a; th.th_plus; th.th_mult; 
+		  th.th_one; th.th_zero; v; p |]),
+	mkLApp(coq_interp_acs,
+               [| th.th_a; th.th_plus; th.th_mult; 
 		  th.th_one; th.th_zero; v;
 		  pf_reduce cbv_betadeltaiota gl 
-		    (mkAppA [| Lazy.force coq_aspolynomial_normalize; p|]) |],
-	mkAppA [| Lazy.force coq_spolynomial_simplify_ok;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
-		  th.th_eq; v; th.th_t; p |]))
+		    (mkLApp(coq_aspolynomial_normalize,[|p|])) |]),
+	mkLApp(coq_spolynomial_simplify_ok,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+		  th.th_eq; v; th.th_t; p |])))
     lp
 
 (*
@@ -607,25 +613,25 @@ let build_apolynom gl th lc =
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
-	  mkAppA [| Lazy.force coq_APplus; aux c1; aux c2 |]
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
-	  mkAppA [| Lazy.force coq_APmult; aux c1; aux c2 |]
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkLApp(coq_APplus, [| aux c1; aux c2 |])
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkLApp(coq_APmult, [| aux c1; aux c2 |])
       (* The special case of Zminus *)
-      | IsApp (binop, [|c1; c2|]) 
-	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
-	                                 mkAppA [|(unbox th.th_opp); c2 |] |]) ->
-	    mkAppA [| Lazy.force coq_APplus; aux c1;
-	              mkAppA [| Lazy.force coq_APopp; aux c2 |] |]
-      | IsApp (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
-	  mkAppA [| Lazy.force coq_APopp; aux c1 |]
+      | App (binop, [|c1; c2|]) 
+	  when pf_conv_x gl c
+            (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) ->
+	    mkLApp(coq_APplus,
+                   [|aux c1; mkLApp(coq_APopp,[|aux c2|]) |])
+      | App (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
+	  mkLApp(coq_APopp, [| aux c1 |])
       | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
       | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
       | _ -> 
 	  try Hashtbl.find varhash c 
 	  with Not_found -> 
-	    let newvar = mkAppA [| Lazy.force coq_APvar; 
-				   (path_of_int !counter) |] in
+	    let newvar =
+              mkLApp(coq_APvar, [| path_of_int !counter |]) in
 	    begin 
 	      incr counter;
 	      varlist := c :: !varlist;
@@ -637,17 +643,17 @@ let build_apolynom gl th lc =
   let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
   List.map 
     (fun p -> 
-       (mkAppA [| Lazy.force coq_interp_ap;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; 
-		  th.th_zero; (unbox th.th_opp); v; p |],
-	mkAppA [| Lazy.force coq_interp_sacs;
-		  th.th_a; th.th_plus; th.th_mult; 
+       (mkLApp(coq_interp_ap,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; 
+		  th.th_zero; (unbox th.th_opp); v; p |]),
+	mkLApp(coq_interp_sacs,
+	       [| th.th_a; th.th_plus; th.th_mult; 
 		  th.th_one; th.th_zero; (unbox th.th_opp); v; 
 		  pf_reduce cbv_betadeltaiota gl 
-		    (mkAppA [| Lazy.force coq_apolynomial_normalize; p |]) |],
-	mkAppA [| Lazy.force coq_apolynomial_normalize_ok;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
-		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))
+		    (mkLApp(coq_apolynomial_normalize, [|p|])) |]),
+	mkLApp(coq_apolynomial_normalize_ok,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |])))
     lp
     
 (*
@@ -668,25 +674,26 @@ let build_setpolynom gl th lc =
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
-	  mkAppA [| Lazy.force coq_SetPplus; th.th_a; aux c1; aux c2 |]
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
-	  mkAppA [| Lazy.force coq_SetPmult; th.th_a; aux c1; aux c2 |]
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |])
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |])
       (* The special case of Zminus *)
-      | IsApp (binop, [|c1; c2|])
-	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
-	                                 mkAppA [|(unbox th.th_opp); c2 |] |]) ->
-	    mkAppA [| Lazy.force coq_SetPplus; th.th_a; aux c1;
-	              mkAppA [| Lazy.force coq_SetPopp; th.th_a; aux c2 |] |]
-      | IsApp (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
-	  mkAppA [| Lazy.force coq_SetPopp; th.th_a; aux c1 |]
+      | App (binop, [|c1; c2|])
+	  when pf_conv_x gl c
+            (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|])|])) ->
+	    mkLApp(coq_SetPplus,
+                   [| th.th_a; aux c1;
+	              mkLApp(coq_SetPopp, [|th.th_a; aux c2|]) |])
+      | App (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
+	  mkLApp(coq_SetPopp, [| th.th_a; aux c1 |])
       | _ when closed_under th.th_closed c ->
-	  mkAppA [| Lazy.force coq_SetPconst; th.th_a; c |]
+	  mkLApp(coq_SetPconst, [| th.th_a; c |])
       | _ -> 
 	  try Hashtbl.find varhash c 
 	  with Not_found -> 
-	    let newvar = mkAppA [| Lazy.force coq_SetPvar; th.th_a; 
-				   (path_of_int !counter) |] in
+	    let newvar =
+              mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in
 	    begin 
 	      incr counter;
 	      varlist := c :: !varlist;
@@ -698,21 +705,22 @@ let build_setpolynom gl th lc =
   let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
   List.map 
     (fun p -> 
-       (mkAppA [| Lazy.force coq_interp_setp;
-		  th.th_a; th.th_plus; th.th_mult; th.th_zero; (unbox th.th_opp);
-		  v; p |],
-	mkAppA [| Lazy.force coq_interp_setcs;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
+       (mkLApp(coq_interp_setp,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
+                  (unbox th.th_opp); v; p |]),
+	mkLApp(coq_interp_setcs,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
 		  pf_reduce cbv_betadeltaiota gl 
-		    (mkAppA [| Lazy.force coq_setpolynomial_simplify; 
-			       th.th_a; th.th_plus; th.th_mult; 
+		    (mkLApp(coq_setpolynomial_simplify,
+			    [| th.th_a; th.th_plus; th.th_mult; 
 			       th.th_one; th.th_zero; 
-			       (unbox th.th_opp); th.th_eq; p |]) |],
-	mkAppA [| Lazy.force coq_setpolynomial_simplify_ok;
-		  th.th_a; (unbox th.th_equiv); th.th_plus; th.th_mult; th.th_one;
-		  th.th_zero;(unbox th.th_opp); th.th_eq; v; th.th_t; (unbox th.th_setoid_th);
+			       (unbox th.th_opp); th.th_eq; p |])) |]),
+	mkLApp(coq_setpolynomial_simplify_ok,
+	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
+                  th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp);
+                  th.th_eq; v; th.th_t; (unbox th.th_setoid_th);
 		  (unbox th.th_morph).plusm; (unbox th.th_morph).multm;
-		  (unbox th.th_morph).oppm; p |]))
+		  (unbox th.th_morph).oppm; p |])))
     lp
 
 (*
@@ -733,17 +741,17 @@ let build_setspolynom gl th lc =
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
-	  mkAppA [| Lazy.force coq_SetSPplus; th.th_a; aux c1; aux c2 |]
-      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
-	  mkAppA [| Lazy.force coq_SetSPmult; th.th_a; aux c1; aux c2 |]
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkLApp(coq_SetSPplus, [|th.th_a; aux c1; aux c2 |])
+      | App (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkLApp(coq_SetSPmult, [| th.th_a; aux c1; aux c2 |])
       | _ when closed_under th.th_closed c ->
-	  mkAppA [| Lazy.force coq_SetSPconst; th.th_a; c |]
+	  mkLApp(coq_SetSPconst, [| th.th_a; c |])
       | _ -> 
 	  try Hashtbl.find varhash c
 	  with Not_found ->
-	    let newvar = mkAppA [| Lazy.force coq_SetSPvar; th.th_a; 
-				   (path_of_int !counter) |] in
+	    let newvar =
+              mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in
 	    begin 
 	      incr counter;
 	      varlist := c :: !varlist;
@@ -755,20 +763,21 @@ let build_setspolynom gl th lc =
   let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
   List.map
     (fun p ->
-       (mkAppA [| Lazy.force coq_interp_setsp;
-		  th.th_a; th.th_plus; th.th_mult; th.th_zero;
-		  v; p |],
-	mkAppA [| Lazy.force coq_interp_setcs;
-		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
+       (mkLApp(coq_interp_setsp,
+	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
+	mkLApp(coq_interp_setcs,
+               [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
 		  pf_reduce cbv_betadeltaiota gl 
-		    (mkAppA [| Lazy.force coq_setspolynomial_simplify; 
-			       th.th_a; th.th_plus; th.th_mult; 
+		    (mkLApp(coq_setspolynomial_simplify,
+			    [| th.th_a; th.th_plus; th.th_mult; 
 			       th.th_one; th.th_zero; 
-			       th.th_eq; p |]) |],
-	mkAppA [| Lazy.force coq_setspolynomial_simplify_ok;
-		  th.th_a; (unbox th.th_equiv); th.th_plus; th.th_mult; th.th_one;
-		  th.th_zero; th.th_eq; v; th.th_t; (unbox th.th_setoid_th);
-		  (unbox th.th_morph).plusm; (unbox th.th_morph).multm; p |]))
+			       th.th_eq; p |])) |]),
+	mkLApp(coq_setspolynomial_simplify_ok,
+	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
+                  th.th_mult; th.th_one; th.th_zero; th.th_eq; v;
+                  th.th_t; (unbox th.th_setoid_th);
+		  (unbox th.th_morph).plusm;
+                  (unbox th.th_morph).multm; p |])))
     lp
 
 module SectionPathSet =
@@ -806,12 +815,12 @@ let constants_to_unfold =
 open RedFlags
 let polynom_unfold_tac =
   let flags =
-    (UNIFORM, mkflags(fBETA::fIOTA::fEVAR::(List.map fCONST constants_to_unfold))) in
+    (UNIFORM, mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
   reduct_in_concl (cbv_norm_flags flags)
       
 let polynom_unfold_tac_in_term gl =
   let flags = 
-    (UNIFORM,mkflags(fBETA::fIOTA::fEVAR::fZETA::(List.map fCONST constants_to_unfold)))
+    (UNIFORM,mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold)))
   in
   cbv_norm_flags flags (pf_env gl) (project gl)
 
@@ -854,10 +863,10 @@ let raw_polynom th op lc gl =
            (tclORELSE 
               (tclORELSE
 		 (h_exact c'i_eq_c''i)
-		 (h_exact (mkAppA
-			     [| (Lazy.force coq_seq_sym); 
-				th.th_a; (unbox th.th_equiv); (unbox th.th_setoid_th);
-				c'''i; ci; c'i_eq_c''i |])))
+		 (h_exact (mkLApp(coq_seq_sym, 
+				  [| th.th_a; (unbox th.th_equiv);
+                                     (unbox th.th_setoid_th);
+				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS 
 		 (Setoid_replace.setoid_replace ci c'''i None)
 		 [ tac;
@@ -866,12 +875,11 @@ let raw_polynom th op lc gl =
            (tclORELSE
               (tclORELSE
 		 (h_exact c'i_eq_c''i)
-		 (h_exact (mkAppA
-			     [| build_coq_sym_eqT (); 
-				th.th_a; c'''i; ci; c'i_eq_c''i |]))) 
+		 (h_exact (mkApp(build_coq_sym_eqT (),
+				 [|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS 
 		 (elim_type 
-		    (mkAppA [| build_coq_eqT (); th.th_a; c'''i; ci |]))
+		    (mkApp(build_coq_eqT (), [|th.th_a; c'''i; ci |])))
 		 [ tac;
                    h_exact c'i_eq_c''i ]))
 )
@@ -885,16 +893,16 @@ let guess_eq_tac th =
 	polynom_unfold_tac
 	(tclREPEAT 
 	   (tclORELSE 
-	      (apply (mkAppA [| build_coq_f_equal2 ();
-				th.th_a; th.th_a; th.th_a;
-				th.th_plus |])) 
-	      (apply (mkAppA [| build_coq_f_equal2 ();
-				th.th_a; th.th_a; th.th_a; 
-				th.th_mult |]))))))
+	      (apply (mkApp(build_coq_f_equal2 (),
+		            [| th.th_a; th.th_a; th.th_a;
+			       th.th_plus |])))
+	      (apply (mkApp(build_coq_f_equal2 (),
+		            [| th.th_a; th.th_a; th.th_a; 
+			       th.th_mult |])))))))
 let guess_equiv_tac th = 
-  (tclORELSE (apply (mkAppA [|(Lazy.force coq_seq_refl);
-			      th.th_a; (unbox th.th_equiv);
-			      (unbox th.th_setoid_th)|]))
+  (tclORELSE (apply (mkLApp(coq_seq_refl,
+			    [| th.th_a; (unbox th.th_equiv);
+			       (unbox th.th_setoid_th)|])))
      (tclTHEN 
 	polynom_unfold_tac
 	(tclREPEAT 
@@ -903,9 +911,9 @@ let guess_equiv_tac th =
 	      (apply (unbox th.th_morph).multm)))))
 
 let match_with_equiv c = match (kind_of_term c) with
-  | IsApp (e,a) -> 
+  | App (e,a) -> 
       if (List.mem e (Setoid_replace.equiv_list ()))
-      then Some (decomp_app c)
+      then Some (decompose_app c)
       else None
   | _ -> None
 
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index c64038323..76a6bdf52 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -16,37 +16,38 @@ type result =
  | Kufo;;
 
 let destructurate t =
-  let c, args = Reduction.whd_stack t in
+  let c, args = Term.decompose_app t in
+  let env = Global.env() in
   match Term.kind_of_term c, args with
-    | Term.IsConst sp, args ->
+    | Term.Const sp, args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global (Names.ConstRef sp))),
-                args)
-    | Term.IsMutConstruct csp , args ->
+		(Termops.id_of_global env (Nametab.ConstRef sp)),
+              args)
+    | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global(Names.ConstructRef csp))),
+		(Termops.id_of_global env (Nametab.ConstructRef csp)),
 	        args)
-    | Term.IsMutInd isp, args ->
+    | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global (Names.IndRef isp))),args)
-    | Term.IsVar id,[] -> Kvar(Names.string_of_id id)
-    | Term.IsProd (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
-    | Term.IsProd (Names.Name _,_,_),[] ->
+		(Termops.id_of_global env (Nametab.IndRef isp)),args)
+    | Term.Var id,[] -> Kvar(Names.string_of_id id)
+    | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
+    | Term.Prod (Names.Name _,_,_),[] ->
 	Util.error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
 exception Destruct
 
 let dest_const_apply t = 
-  let f,args = Reduction.whd_stack t in
+  let f,args = Term.decompose_app t in
   let ref = 
   match Term.kind_of_term f with 
-    | Term.IsConst sp         -> Names.ConstRef sp
-    | Term.IsMutConstruct csp -> Names.ConstructRef csp
-    | Term.IsMutInd isp       -> Names.IndRef isp
+    | Term.Const sp         -> Nametab.ConstRef sp
+    | Term.Construct csp -> Nametab.ConstructRef csp
+    | Term.Ind isp       -> Nametab.IndRef isp
     | _ -> raise Destruct
   in
-  Names.basename (Global.sp_of_global ref), args
+  Termops.id_of_global (Global.env()) ref, args
 
 let recognize_number t =
   let rec loop t =
@@ -64,8 +65,9 @@ let recognize_number t =
 let constant dir s =
   try
     Declare.global_absolute_reference
-      (Names.make_path (Names.make_dirpath (List.map Names.id_of_string dir))
-                       (Names.id_of_string s) Names.CCI)
+      (Names.make_path
+        (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
+        (Names.id_of_string s))
   with e -> print_endline (String.concat "." dir); print_endline s; 
             raise e
 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index f2de55314..79348a704 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -64,11 +64,11 @@ let extract_nparams pack =
  let module S = Sign in
 
   let {D.mind_nparams=nparams0} = pack.(0) in
-  let arity0 = D.mind_user_arity pack.(0) in
+  let arity0 = pack.(0).D.mind_user_arity in
   let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in
   for i = 1 to Array.length pack - 1 do
     let {D.mind_nparams=nparamsi} = pack.(i) in
-    let arityi = D.mind_user_arity pack.(i) in
+    let arityi = pack.(i).D.mind_user_arity in
     let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in
     if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
   done;
@@ -99,9 +99,10 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 (* section path is sp                                                         *)
 let uri_of_path sp tag =
  let module N = Names in
+ let module No = Nameops in
   let ext_of_sp sp = ext_of_tag tag in
-  let dir0 = N.extend_dirpath (N.dirpath sp) (N.basename sp) in
-  let dir = List.map N.string_of_id (N.repr_dirpath dir0) in
+  let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
+  let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
    "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp)
 ;;
 
@@ -193,10 +194,12 @@ let add_to_pvars x =
   let v =
    match x with
       Definition (v, bod, typ) ->
-       cumenv := E.push_named_def (Names.id_of_string v, bod, typ) !cumenv ;
+       cumenv :=
+         E.push_named_decl (Names.id_of_string v, Some bod, typ) !cumenv ;
        v
     | Assumption (v, typ) ->
-       cumenv := E.push_named_assum (Names.id_of_string v, typ) !cumenv ;
+       cumenv :=
+         E.push_named_decl (Names.id_of_string v, None, typ) !cumenv ;
        v
   in
    match !pvars with
@@ -305,18 +308,18 @@ let print_term inner_types l env csr =
     (* kind_of_term helps doing pattern matching hiding the lower level of *)
    (* coq coding of terms (the one of the logical framework)              *)
    match T.kind_of_term cstr with
-     T.IsRel n  ->
+     T.Rel n  ->
       let id =
        match List.nth l (n - 1) with
           N.Name id   -> id
-        | N.Anonymous -> N.make_ident "_" None
+        | N.Anonymous -> Nameops.make_ident "_" None
       in
        X.xml_empty "REL"
         (add_sort_attribute false
           ["value",(string_of_int n) ;
            "binder",(N.string_of_id id) ;
            "id", next_id])
-   | T.IsVar id ->
+   | T.Var id ->
       let depth =
        match get_depth_of_var (N.string_of_id id) with
           None -> "?" (* when printing via Show XML Proof or Print XML id *)
@@ -328,33 +331,33 @@ let print_term inner_types l env csr =
         (add_sort_attribute false
          ["relUri",depth ^ "," ^ (N.string_of_id id) ;
           "id", next_id])
-   | T.IsMeta n ->
+   | T.Meta n ->
       X.xml_empty "META"
        (add_sort_attribute false ["no",(string_of_int n) ; "id", next_id])
-   | T.IsSort s ->
+   | T.Sort s ->
       X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", next_id]
-   | T.IsCast (t1,t2) ->
+   | T.Cast (t1,t2) ->
       X.xml_nempty "CAST" (add_sort_attribute false ["id", next_id])
 (force
        [< X.xml_nempty "term" [] (term_display idradix false l env t1) ;
           X.xml_nempty "type" [] (term_display idradix false l env t2)
        >]
 )
-   | T.IsLetIn (nid,s,t,d)->
-      let nid' = N.next_name_away nid (names_to_ids l) in
+   | T.LetIn (nid,s,t,d)->
+      let nid' = Nameops.next_name_away nid (names_to_ids l) in
        X.xml_nempty "LETIN" (add_sort_attribute true ["id", next_id])
 (force
         [< X.xml_nempty "term" [] (term_display idradix false l env s) ;
            X.xml_nempty "letintarget" ["binder",(N.string_of_id nid')]
             (term_display idradix false
              ((N.Name nid')::l)
-             (E.push_rel_def (N.Name nid', s, t) env)
+             (E.push_rel (N.Name nid', Some s, t) env)
              d
             )
         >]
 )
-   | T.IsProd (N.Name _ as nid, t1, t2) ->
-      let nid' = N.next_name_away nid (names_to_ids l) in
+   | T.Prod (N.Name _ as nid, t1, t2) ->
+      let nid' = Nameops.next_name_away nid (names_to_ids l) in
        X.xml_nempty "PROD" (add_type_attribute ["id", next_id])
 (force
         [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
@@ -365,49 +368,49 @@ let print_term inner_types l env csr =
              else ["binder",(N.string_of_id nid')])
             (term_display idradix false
              ((N.Name nid')::l)
-             (E.push_rel_assum (N.Name nid', t1) env)
+             (E.push_rel (N.Name nid', None, t1) env)
              t2
             )
         >]
 )
-   | T.IsProd (N.Anonymous as nid, t1, t2) ->
+   | T.Prod (N.Anonymous as nid, t1, t2) ->
       X.xml_nempty "PROD" (add_type_attribute ["id", next_id])
 (force
        [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
           X.xml_nempty "target" []
            (term_display idradix false
             (nid::l)
-            (E.push_rel_assum (nid, t1) env)
+            (E.push_rel (nid, None, t1) env)
             t2
            )
        >]
 )
-   | T.IsLambda (N.Name _ as nid, t1, t2) ->
-      let nid' = N.next_name_away nid (names_to_ids l) in
+   | T.Lambda (N.Name _ as nid, t1, t2) ->
+      let nid' = Nameops.next_name_away nid (names_to_ids l) in
        X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id",next_id])
 (force
         [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
            X.xml_nempty "target" ["binder",(N.string_of_id nid')]
             (term_display idradix true
              ((N.Name nid')::l)
-             (E.push_rel_assum (N.Name nid', t1) env)
+             (E.push_rel (N.Name nid', None, t1) env)
              t2
             )
         >]
 )
-   | T.IsLambda (N.Anonymous as nid, t1, t2) ->
+   | T.Lambda (N.Anonymous as nid, t1, t2) ->
       X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id", next_id])
 (force
        [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
           X.xml_nempty "target" []
            (term_display idradix true
             (nid::l)
-            (E.push_rel_assum (nid, t1) env)
+            (E.push_rel (nid, None, t1) env)
             t2
           )
        >]
 )
-   | T.IsApp (h,t) ->
+   | T.App (h,t) ->
       X.xml_nempty "APPLY" (add_sort_attribute true ["id", next_id])
 (force
        [< (term_display idradix false l env h) ;
@@ -415,23 +418,23 @@ let print_term inner_types l env csr =
           (fun x i -> [< (term_display idradix false l env x); i >]) t [<>])
        >]
 )
-   | T.IsConst sp ->
+   | T.Const sp ->
       X.xml_empty "CONST"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Constant) ; "id", next_id])
-   | T.IsMutInd (sp,i) ->
+   | T.Ind (sp,i) ->
       X.xml_empty "MUTIND"
        ["uri",(uri_of_path sp Inductive) ;
         "noType",(string_of_int i) ;
         "id", next_id]
-   | T.IsMutConstruct ((sp,i),j) ->
+   | T.Construct ((sp,i),j) ->
       X.xml_empty "MUTCONSTRUCT"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Inductive) ;
          "noType",(string_of_int i) ;
          "noConstr",(string_of_int j) ;
          "id", next_id])
-   | T.IsMutCase ((_,((sp,i),_,_,_,_)),ty,term,a) ->
+   | T.Case ({T.ci_ind=(sp,i)},ty,term,a) ->
       let (uri, typeno) = (uri_of_path sp Inductive),i in
        X.xml_nempty "MUTCASE"
         (add_sort_attribute true
@@ -448,7 +451,7 @@ let print_term inner_types l env csr =
             ) a [<>]
         >]
 )
-   | T.IsFix ((ai,i),((f,t,b) as rec_decl)) ->
+   | T.Fix ((ai,i),((f,t,b) as rec_decl)) ->
       X.xml_nempty "FIX"
        (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id])
 (force
@@ -472,7 +475,7 @@ let print_term inner_types l env csr =
            [<>]
        >]
 )
-   | T.IsCoFix (i,((f,t,b) as rec_decl)) ->
+   | T.CoFix (i,((f,t,b) as rec_decl)) ->
       X.xml_nempty "COFIX"
        (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id])
 (force
@@ -494,7 +497,7 @@ let print_term inner_types l env csr =
 	   (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) f ) [<>]
        >]
 )
-   | T.IsEvar _ ->
+   | T.Evar _ ->
       Util.anomaly "Evar node in a term!!!"
   in
     (*CSC: ad l vanno andrebbero aggiunti i nomi da non *)
@@ -590,7 +593,7 @@ let print_variable id body typ env inner_types =
 (*          of mutual inductive definitions)                                 *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp   *)
 (* Used only by print_mutual_inductive                                       *)
-let print_mutual_inductive_packet inner_types names env p =
+let print_mutual_inductive_packet inner_types names env finite p =
  let module D = Declarations in
  let module N = Names in
  let module T = Term in
@@ -598,8 +601,7 @@ let print_mutual_inductive_packet inner_types names env p =
   let {D.mind_consnames=consnames ;
        D.mind_typename=typename ;
        D.mind_nf_lc=lc ;
-       D.mind_nf_arity=arity ;
-       D.mind_finite=finite} = p
+       D.mind_nf_arity=arity} = p
   in
    [< X.xml_nempty "InductiveType"
        ["name",(N.string_of_id typename) ;
@@ -628,7 +630,7 @@ let print_mutual_inductive_packet inner_types names env p =
 (*  and   nparams     is the number of "parameters" in the arity of the    *)
 (*                    mutual inductive types                               *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_mutual_inductive packs fv hyps env inner_types =
+let print_mutual_inductive finite packs fv hyps env inner_types =
  let module D = Declarations in
  let module E = Environ in
  let module X = Xml in
@@ -642,7 +644,7 @@ let print_mutual_inductive packs fv hyps env inner_types =
   let env =
    List.fold_right
     (fun {D.mind_typename=typename ; D.mind_nf_arity=arity} env ->
-     E.push_rel_assum (N.Name typename, arity) env)
+     E.push_rel (N.Name typename, None, arity) env)
     (Array.to_list packs)
     env
   in
@@ -655,7 +657,8 @@ let print_mutual_inductive packs fv hyps env inner_types =
         "params",(string_of_pvars fv hyps)]
        [< (Array.fold_right
             (fun x i ->
-             [< print_mutual_inductive_packet inner_types names env x ; i >]
+             [< print_mutual_inductive_packet
+                  inner_types names env finite x ; i >]
             ) packs [< >]
           )
        >]
@@ -664,7 +667,7 @@ let print_mutual_inductive packs fv hyps env inner_types =
 
 let string_list_of_named_context_list =
  List.map
-  (function (n,_,_) -> Names.string_of_id (Names.basename n))
+  (function (n,_,_) -> Names.string_of_id n)
 ;;
 
 let types_filename_of_filename =
@@ -700,24 +703,25 @@ let pp_cmds_of_inner_types inner_types target_uri =
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-let print sp fn =
+let print qid fn =
  let module D = Declarations in
  let module G = Global in
  let module N = Names in
  let module Nt = Nametab in
  let module T = Term in
  let module X = Xml in
-  let (_,id) = Nt.repr_qualid sp in
-  let glob_ref = Nametab.locate sp in
+  let (_,id) = Nt.repr_qualid qid in
+  let glob_ref = Nametab.locate qid in
   let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
   reset_ids () ;
   let inner_types = ref [] in
   let sp,tag,pp_cmds =
    match glob_ref with
-      N.VarRef sp ->
-       let (body,typ) = G.lookup_named id in
+      Nt.VarRef id ->
+        let sp = Declare.find_section_variable id in
+       let (_,body,typ) = G.lookup_named id in
         sp,Variable,print_variable id body (T.body_of_type typ) env inner_types
-    | N.ConstRef sp ->
+    | Nt.ConstRef sp ->
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
         G.lookup_constant sp in
        let hyps = string_list_of_named_context_list hyps in
@@ -728,12 +732,14 @@ let print sp fn =
             None ->   print_axiom id typ [] hyps env inner_types
           | Some c -> print_definition id c typ [] hyps env inner_types
         end
-    | N.IndRef (sp,_) ->
-       let {D.mind_packets=packs ; D.mind_hyps=hyps} = G.lookup_mind sp in
+    | Nt.IndRef (sp,_) ->
+       let {D.mind_packets=packs ;
+            D.mind_hyps=hyps;
+            D.mind_finite=finite} = G.lookup_mind sp in
         let hyps = string_list_of_named_context_list hyps in
          sp,Inductive,
-          print_mutual_inductive packs [] hyps env inner_types
-    | N.ConstructRef _ ->
+          print_mutual_inductive finite packs [] hyps env inner_types
+    | Nt.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in
    Xml.pp pp_cmds fn ;
@@ -795,11 +801,12 @@ let mkfilename dn sp ext =
   let module L = Library in
   let module S = System in
   let module N = Names in
+  let module No = Nameops in
    match dn with
       None         -> None
     | Some basedir ->
-	let dir0 = N.extend_dirpath (N.dirpath sp) (N.basename sp) in
-	let dir = List.map N.string_of_id (N.repr_dirpath dir0) in
+	let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
+	let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
        Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
 ;;
 
@@ -844,13 +851,14 @@ let print_object lobj id sp dn fv env =
       | "INDUCTIVE" ->
            let
             {D.mind_packets=packs ;
-             D.mind_hyps = hyps
+             D.mind_hyps = hyps;
+             D.mind_finite = finite
             } = G.lookup_mind sp
            in
             let hyps = string_list_of_named_context_list hyps in
-             print_mutual_inductive packs fv hyps env inner_types
+             print_mutual_inductive finite packs fv hyps env inner_types
       | "VARIABLE" ->
-          let (_,(varentry,_)) = Declare.out_variable lobj in
+          let (_,(_,varentry,_)) = Declare.out_variable lobj in
            begin
             match varentry with
                Declare.SectionLocalDef body ->
@@ -883,7 +891,7 @@ let rec print_library_segment state bprintleaf dn =
   List.iter
    (function (sp, node) ->
      print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ;
-     print_node node (Names.basename sp) sp bprintleaf dn ;
+     print_node node (Nameops.basename sp) sp bprintleaf dn ;
      print_if_verbose "\n"
    ) (List.rev state)
 (* print_node node id section_path bprintleaf directory_name             *)
@@ -921,10 +929,10 @@ with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
           end
        end
    | L.OpenedSection (dir,_) ->
-       let id = snd (Names.split_dirpath dir) in
+       let id = snd (Nameops.split_dirpath dir) in
        print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
    | L.ClosedSection (_,dir,state) ->
-      let id = snd (Names.split_dirpath dir) in
+      let id = snd (Nameops.split_dirpath dir) in
       print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
       if bprintleaf then
        begin
@@ -992,13 +1000,14 @@ let printModule qid dn =
 let printSection id dn =
  let module L = Library in
  let module N = Names in
+ let module No = Nameops in
  let module X = Xml in
-  let sp = Lib.make_path id N.OBJ in
+  let sp = Lib.make_path id in
   let ls =
    let rec find_closed_section =
     function
        [] -> raise Not_found
-     | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (N.split_dirpath dir) = id
+     | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id
 	 -> ls
      | _::t -> find_closed_section t
    in