Suppression des arguments sur les constantes, inductifs et constructeurs

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

23 files changed, 356 insertions, 450 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 82847ae152..283b60e28d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -97,7 +97,7 @@ module RedFlags = (struct
     r_iota : bool }
 
   type red_kind = BETA | DELTA | EVAR | IOTA | ZETA
-	      | CONST of constant_path | VAR of identifier
+	      | CONST of constant | VAR of identifier
   let fBETA = BETA
   let fDELTA = DELTA
   let fEVAR = EVAR 
@@ -566,8 +566,8 @@ and fterm =
   | FAtom of constr
   | FCast of fconstr * fconstr
   | FFlex of freference
-  | FInd of inductive_path * fconstr array
-  | FConstruct of constructor_path * fconstr array
+  | FInd of inductive
+  | FConstruct of constructor
   | FApp of fconstr * fconstr array
   | FFix of (int array * int) * (name array * fconstr array * fconstr array)
       * constr array * fconstr subs
@@ -583,7 +583,7 @@ and fterm =
 
 and freference =
   (* only vars as args of FConst ... exploited for caching *)
-  | FConst of section_path * fconstr array
+  | FConst of constant
   | FEvar of existential_key * fconstr array
   | FVar of identifier
   | FFarRel of int (* index in the rel_context part of _initial_ environment *)
@@ -677,13 +677,13 @@ let mk_clos_deep clos_fun env t =
     | IsApp (f,v) ->
         { norm = Red;
 	  term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
-    | IsMutInd (sp,v) ->
-        { norm = Cstr; term = FInd (sp, Array.map (clos_fun env) v) }
-    | IsMutConstruct (sp,v) ->
-        { norm = Cstr; term = FConstruct (sp,Array.map (clos_fun env) v)}
-    | IsConst (sp,v) ->
+    | IsMutInd sp ->
+        { norm = Norm; term = FInd sp }
+    | IsMutConstruct sp ->
+        { norm = Norm; term = FConstruct sp }
+    | IsConst sp ->
         { norm = Red;
-	  term = FFlex (FConst (sp,Array.map (clos_fun env) v)) }
+	  term = FFlex (FConst sp) }
     | IsEvar (n,v) ->
         { norm = Red;
 	  term = FFlex (FEvar (n, Array.map (clos_fun env) v)) }
@@ -736,14 +736,11 @@ let rec to_constr constr_fun lfts v =
           | _ -> assert false)
     | FCast (a,b) ->
         mkCast (constr_fun lfts a, constr_fun lfts b)
-    | FFlex (FConst (op,ve)) ->
-	mkConst (op, Array.map (constr_fun lfts) ve)
+    | FFlex (FConst op) -> mkConst op
     | FFlex (FEvar (n,args)) ->
 	mkEvar (n, Array.map (constr_fun lfts) args)
-    | FInd (op,ve) ->
-	mkMutInd (op, Array.map (constr_fun lfts) ve)
-    | FConstruct (op,ve) -> 
-	mkMutConstruct (op, Array.map (constr_fun lfts) ve)
+    | FInd op -> mkMutInd op
+    | FConstruct op -> mkMutConstruct op
     | FCases (ci,p,c,ve) ->
 	mkMutCase (ci, constr_fun lfts p,
 		   constr_fun lfts c,
@@ -984,9 +981,8 @@ let rec knr info m stk =
       (match get_arg m stk with
           (Some(depth,arg),s) -> knit info (subs_shift_cons(depth,e,arg)) f s
         | (None,s) -> (m,s))
-  | FFlex(FConst(sp,args)) when can_red info stk (fCONST sp) ->
-      let cst = (sp, Array.map term_of_fconstr args) in
-      (match ref_value_cache info (ConstBinding cst) with
+  | FFlex(FConst sp) when can_red info stk (fCONST sp) ->
+      (match ref_value_cache info (ConstBinding sp) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
   | FFlex(FEvar (n,args)) when can_red info stk fEVAR ->
@@ -1004,7 +1000,7 @@ let rec knr info m stk =
       (match ref_value_cache info (FarRelBinding k) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FConstruct((sp,c),args) when can_red info stk fIOTA ->
+  | FConstruct(ind,c) when can_red info stk fIOTA ->
       (match strip_update_shift_app m stk with
           (depth, args, Zcase(((*cn*) npar,_),_,br)::s) ->
             assert (npar>=0);
@@ -1061,15 +1057,9 @@ and down_then_up info m stk =
             FLetIn(na, kl info a, kl info b, kl info c, f, e)
         | FProd(na,dom,rng,f,e) ->
             FProd(na, kl info dom, kl info rng, f, e)
-        | FInd(ind,args) ->
-            FInd(ind, Array.map (kl info) args)
-        | FConstruct(c,args) ->
-            FConstruct(c, Array.map (kl info) args)
         | FCoFix(n,(na,ftys,fbds),bds,e) ->
             FCoFix(n,(na, Array.map (kl info) ftys,
                           Array.map (kl info) fbds),bds,e)
-        | FFlex(FConst(sp,args)) ->
-            FFlex(FConst(sp, Array.map (kl info) args))
         | FFlex(FEvar(i,args)) ->
             FFlex(FEvar(i, Array.map (kl info) args))
         | t -> t in
@@ -1097,9 +1087,7 @@ let create_clos_infos flgs env sigma =
   create (fun _ -> inject) flgs env sigma
 
 let unfold_reference info = function
-  | FConst (op,v) -> 
-      let cst = (op, Array.map (norm_val info) v) in
-      ref_value_cache info (ConstBinding cst)
+  | FConst op -> ref_value_cache info (ConstBinding op)
   | FEvar (n,v) ->
       let evar = (n, Array.map (norm_val info) v) in
       ref_value_cache info (EvarBinding evar)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 5c86624209..16de949aff 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -166,8 +166,8 @@ type fterm =
   | FAtom of constr
   | FCast of fconstr * fconstr
   | FFlex of freference
-  | FInd of inductive_path * fconstr array
-  | FConstruct of constructor_path * fconstr array
+  | FInd of inductive
+  | FConstruct of constructor
   | FApp of fconstr * fconstr array
   | FFix of (int array * int) * (name array * fconstr array * fconstr array)
       * constr array * fconstr subs
@@ -182,7 +182,7 @@ type fterm =
   | FLOCKED
 
 and freference =
-  | FConst of section_path * fconstr array
+  | FConst of constant
   | FEvar of existential_key * fconstr array
   | FVar of identifier
   | FFarRel of int
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1bccf60f6c..79420e0404 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -20,37 +20,21 @@ open Reduction
 
 (*s Cooking the constants. *)
 
-type modification_action = ABSTRACT | ERASE
-
 type 'a modification =
   | NOT_OCCUR
-  | DO_ABSTRACT of 'a * modification_action list
+  | DO_ABSTRACT of 'a * constr array
   | DO_REPLACE of constant_body
 
 type work_list =
-    (section_path * section_path modification) list
-    * (inductive_path * inductive_path modification) list
-    * (constructor_path * constructor_path modification) list
+    (constant * constant modification) list
+    * (inductive * inductive modification) list
+    * (constructor * constructor modification) list
 
 type recipe = {
   d_from : constant_body;
   d_abstract : identifier list;
   d_modlist : work_list }
 
-let rec modif_length = function
-  | ABSTRACT :: l -> 1 + modif_length l
-  | ERASE :: l -> modif_length l
-  | [] -> 0
-
-let interp_modif absfun mkfun (sp,modif) cl = 
-  let rec interprec = function
-    | ([], cl) -> mkfun (sp, Array.of_list cl)
-    | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
-    | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
-    | _ -> assert false
-  in 
-  interprec (modif, Array.to_list cl)
-
 let failure () =
   anomalylabstrm "generic__modify_opers"
     [< 'sTR"An oper which was never supposed to appear has just appeared" ;
@@ -61,7 +45,7 @@ let failure () =
        'sPC ; 'sTR"is broken - this function is an internal system" ;
        'sPC ; 'sTR"for internal system use only" >]
 
-let modify_opers replfun absfun (constl,indl,cstrl) =
+let modify_opers replfun (constl,indl,cstrl) =
   let rec substrec c =
     let op, cl = splay_constr c in
     let cl' = Array.map substrec cl in
@@ -69,51 +53,51 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
       | OpMutCase (n,(spi,a,b,c,d) as oper) ->
 	  (try
 	     match List.assoc spi indl with
-	       | DO_ABSTRACT (spi',modif) ->
-		   let n' = modif_length modif + n in
+	       | DO_ABSTRACT (spi',abs_vars) ->
+		   let n' = Array.length abs_vars + n in
 		   gather_constr (OpMutCase (n',(spi',a,b,c,d)),cl')
 	       | _ -> raise Not_found
 	   with
 	     | Not_found -> gather_constr (op,cl'))
 
       | OpMutInd spi ->
+	  assert (Array.length cl=0);
 	  (try
 	     (match List.assoc spi indl with
 		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',modif) ->
-		    assert (List.length modif <= Array.length cl);
-		    interp_modif absfun mkMutInd (oper',modif) cl'
+		| DO_ABSTRACT (oper',abs_vars) ->
+                    mkApp (mkMutInd oper', abs_vars)
 		| DO_REPLACE _ -> assert false)
 	   with 
-	     | Not_found -> mkMutInd (spi,cl'))
+	     | Not_found -> mkMutInd spi)
 
       | OpMutConstruct spi ->
+	  assert (Array.length cl=0);
 	  (try
 	     (match List.assoc spi cstrl with
 		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',modif) ->
-		    assert (List.length modif <= Array.length cl);
-		    interp_modif absfun mkMutConstruct (oper',modif) cl'
+		| DO_ABSTRACT (oper',abs_vars) ->
+		    mkApp (mkMutConstruct oper', abs_vars)
 		| DO_REPLACE _ -> assert false)
 	   with 
-	     | Not_found -> mkMutConstruct (spi,cl'))
+	     | Not_found -> mkMutConstruct spi)
 
       | OpConst sp ->
+	  assert (Array.length cl=0);
 	  (try
 	     (match List.assoc sp constl with
 		| NOT_OCCUR -> failure ()
-		| DO_ABSTRACT (oper',modif) ->
-		    assert (List.length modif <= Array.length cl);
-		    interp_modif absfun mkConst (oper',modif) cl'
+		| DO_ABSTRACT (oper',abs_vars) ->
+		    mkApp (mkConst oper', abs_vars)
 		| DO_REPLACE cb -> substrec (replfun sp cb cl'))
 	   with 
-	     | Not_found -> mkConst (sp,cl'))
+	     | Not_found -> mkConst sp)
   
     | _ -> gather_constr (op, cl')
   in 
   if (constl,indl,cstrl) = ([],[],[]) then fun x -> x else substrec
 
-let expmod_constr oldenv modlist c =
+let expmod_constr modlist c =
   let sigma = Evd.empty in
   let simpfun = 
     if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
@@ -130,22 +114,20 @@ let expmod_constr oldenv modlist c =
           instantiate_constr cb.const_hyps body (Array.to_list args)
       | None -> assert false
   in
-  let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
+  let c' =
+    modify_opers expfun modlist c in
   match kind_of_term c' with
     | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
     | _ -> simpfun c'
 
-let expmod_type oldenv modlist c =
-  type_app (expmod_constr oldenv modlist) c
+let expmod_type modlist c =
+  type_app (expmod_constr modlist) c
 
 let abstract_constant ids_to_abs hyps (body,typ) =
   let abstract_once ((hyps,body,typ) as sofar) id =
     match hyps with
       | (hyp,c,t as decl)::rest when hyp = id ->
-	  let body' = match body with
-	    | None -> None
-	    | Some c -> Some (mkNamedLambda_or_LetIn decl c)
-	  in
+	  let body' = option_app (mkNamedLambda_or_LetIn decl) body in
 	  let typ' = mkNamedProd_wo_LetIn decl typ in
 	  (rest, body', typ')
       | _ -> 
@@ -157,9 +139,9 @@ let abstract_constant ids_to_abs hyps (body,typ) =
 
 let cook_constant env r =
   let cb = r.d_from in
-  let typ = expmod_type env r.d_modlist cb.const_type in
-  let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
+  let typ = expmod_type r.d_modlist cb.const_type in
+  let body = option_app (expmod_constr r.d_modlist) cb.const_body in
   let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
-  let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in
+  let hyps = map_named_context (expmod_constr r.d_modlist) hyps in
   let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
   (body, typ, cb.const_constraints, cb.const_opaque)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 48f4dfc831..3cd03fc9a2 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -16,17 +16,15 @@ open Univ
 
 (*s Cooking the constants. *)
 
-type modification_action = ABSTRACT | ERASE
-
 type 'a modification =
   | NOT_OCCUR
-  | DO_ABSTRACT of 'a * modification_action list
+  | DO_ABSTRACT of 'a * constr array
   | DO_REPLACE of constant_body
 
 type work_list =
-    (section_path * section_path modification) list
-    * (inductive_path * inductive_path modification) list
-    * (constructor_path * constructor_path modification) list
+    (constant * constant modification) list
+    * (inductive * inductive modification) list
+    * (constructor * constructor modification) list
 
 type recipe = {
   d_from : constant_body;
@@ -38,7 +36,7 @@ val cook_constant :
 
 (*s Utility functions used in module [Discharge]. *)
 
-val expmod_constr : env -> work_list -> constr -> constr
-val expmod_type : env -> work_list -> types -> types
+val expmod_constr : work_list -> constr -> constr
+val expmod_type : work_list -> types -> types
 
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index f751281480..47f65d4a38 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -45,7 +45,7 @@ type recarg =
   | Param of int 
   | Norec 
   | Mrec of int 
-  | Imbr of inductive_path * recarg list
+  | Imbr of inductive * recarg list
 
 type one_inductive_body = {
   mind_consnames : identifier array;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e7c88f6f42..735f6f1411 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -47,7 +47,7 @@ type recarg =
   | Param of int 
   | Norec 
   | Mrec of int 
-  | Imbr of inductive_path * (recarg list)
+  | Imbr of inductive * (recarg list)
 
 (* [mind_typename] is the name of the inductive; [mind_arity] is
    the arity generalized over global parameters; [mind_lc] is the list
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a34191a3e5..98f54337f3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -214,6 +214,112 @@ let lookup_constant sp env =
 let lookup_mind sp env =
   Spmap.find sp env.env_globals.env_inductives
 
+
+(* Lookup of section variables *)
+let lookup_constant_variables c env =
+  let cmap = lookup_constant c env in
+  Sign.instance_from_section_context cmap.const_hyps
+
+let lookup_inductive_variables (sp,i) env =
+  let mis = lookup_mind sp env in
+  Sign.instance_from_section_context mis.mind_hyps
+
+let lookup_constructor_variables (ind,_) env =
+  lookup_inductive_variables ind env
+
+(* Returns the list of global variables in a term *)
+
+let vars_of_global env constr =
+  match kind_of_term constr with
+      IsVar id -> [id]
+    | IsConst sp ->
+        List.map destVar 
+          (Array.to_list (lookup_constant_variables sp env))
+    | IsMutInd ind ->
+        List.map destVar 
+          (Array.to_list (lookup_inductive_variables ind env))
+    | IsMutConstruct cstr ->
+        List.map destVar 
+          (Array.to_list (lookup_constructor_variables cstr env))
+    | _ -> []
+
+let rec global_varsl env l constr =
+  let l = vars_of_global env constr @ l in
+  fold_constr (global_varsl env) l constr
+
+let global_vars env = global_varsl env []
+
+let global_vars_decl env = function
+  | (_, None, t) -> global_vars env t
+  | (_, Some c, t) -> (global_vars env c)@(global_vars env t)
+
+let global_vars_set env constr = 
+  let rec filtrec acc c =
+    let vl = vars_of_global env c in
+    let acc = List.fold_right Idset.add vl acc in
+    fold_constr filtrec acc c
+  in 
+  filtrec Idset.empty constr
+
+
+exception Occur
+
+let occur_in_global env id constr =
+  let vars = vars_of_global env constr in
+  if List.mem id vars then raise Occur
+
+let occur_var env s c = 
+  let rec occur_rec c =
+    occur_in_global env s c;
+    iter_constr occur_rec c
+  in 
+  try occur_rec c; false with Occur -> true
+
+let occur_var_in_decl env hyp (_,c,typ) =
+  match c with
+    | None -> occur_var env hyp (body_of_type typ)
+    | Some body ->
+        occur_var env hyp (body_of_type typ) ||
+        occur_var env hyp body
+
+(* [keep_hyps sign ids] keeps the part of the signature [sign] which 
+   contains the variables of the set [ids], and recursively the variables 
+   contained in the types of the needed variables. *)
+
+let rec keep_hyps env needed = function
+  | (id,copt,t as d) ::sign when Idset.mem id needed ->
+      let globc = 
+	match copt with
+	  | None -> Idset.empty
+	  | Some c -> global_vars_set env c in
+      let needed' =
+	Idset.union (global_vars_set env (body_of_type t)) 
+	  (Idset.union globc needed) in
+      d :: (keep_hyps env needed' sign)
+  | _::sign -> keep_hyps env needed sign
+  | [] -> []
+
+(* This renames bound variables with fresh and distinct names *)
+(* in such a way that the printer doe not generate new names  *)
+(* and therefore that printed names are the intern names      *)
+(* In this way, tactics such as Induction works well          *)
+
+let rec rename_bound_var env l c =
+  match kind_of_term c with
+  | IsProd (Name s,c1,c2)  ->
+      if dependent (mkRel 1) c2 then
+        let s' = next_ident_away s (global_vars env c2@l) in
+        let env' = push_rel (Name s',None,c1) env in
+        mkProd (Name s', c1, rename_bound_var env' (s'::l) c2)
+      else 
+        let env' = push_rel (Name s,None,c1) env in
+	mkProd (Name s, c1, rename_bound_var env' l c2)
+  | IsProd (Anonymous,c1,c2) ->
+        let env' = push_rel (Anonymous,None,c1) env in
+        mkProd (Anonymous, c1, rename_bound_var env' l c2)
+  | IsCast (c,t) -> mkCast (rename_bound_var env l c, t)
+  | x -> c
+
 (* First character of a constr *)
 
 let lowercase_first_char id = String.lowercase (first_char id)
@@ -244,15 +350,15 @@ let hdchar env c =
     | IsLetIn (_,_,_,c)    -> hdrec (k+1) c
     | IsCast (c,_)         -> hdrec k c
     | IsApp (f,l)         -> hdrec k f
-    | IsConst (sp,_)       ->
+    | IsConst sp       ->
 	let c = lowercase_first_char (basename sp) in
 	if c = "?" then "y" else c
-    | IsMutInd ((sp,i) as x,_) ->
+    | IsMutInd ((sp,i) as x) ->
 	if i=0 then 
 	  lowercase_first_char (basename sp)
 	else 
 	  lowercase_first_char (id_of_global env (IndRef x))
-    | IsMutConstruct ((sp,i) as x,_) ->
+    | IsMutConstruct ((sp,i) as x) ->
 	lowercase_first_char (id_of_global env (ConstructRef x))
     | IsVar id  -> lowercase_first_char id
     | IsSort s -> sort_hdchar s
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2a778b76e3..761f196c03 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -104,12 +104,18 @@ val lookup_rel_value : int -> env -> constr option
 
 (* Looks up in the context of global constant names *)
 (* raises [Not_found] if the required path is not found *)
-val lookup_constant : constant_path -> env -> constant_body
+val lookup_constant : constant -> env -> constant_body
 
 (* Looks up in the context of global inductive names *)
 (* raises [Not_found] if the required path is not found *)
 val lookup_mind : section_path -> env -> mutual_inductive_body
 
+(* Looks up the array of section variables used by a global (constant,
+   inductive or constructor). *)
+val lookup_constant_variables : constant -> env -> constr array
+val lookup_inductive_variables : inductive -> env -> constr array
+val lookup_constructor_variables : constructor -> env -> constr array
+
 (*s Miscellanous *)
 
 val sp_of_global : env -> global_reference -> section_path
@@ -158,12 +164,30 @@ val it_mkNamedProd_wo_LetIn : constr -> named_context -> constr
 val lambda_create : env -> types * constr -> constr
 val prod_create : env -> types * constr -> constr
 
-val defined_constant : env -> constant_path -> bool
-val evaluable_constant : env -> constant_path -> bool
+val defined_constant : env -> constant -> bool
+val evaluable_constant : env -> constant -> bool
 
 val evaluable_named_decl : env -> identifier -> bool
 val evaluable_rel_decl : env -> int -> bool
 
+(*s Ocurrence of section variables. *)
+(* [(occur_var id c)] returns [true] if variable [id] occurs free
+   in c, [false] otherwise *)
+val occur_var : env -> identifier -> constr -> bool
+val occur_var_in_decl : env -> identifier -> named_declaration -> bool
+
+(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
+val global_vars : env -> constr -> identifier list
+
+(* [global_vars_decl d] returns the list of [id]'s occurring as [VAR
+    id] in declaration [d] (type and body if any) *)
+val global_vars_decl : env -> named_declaration -> identifier list
+val global_vars_set : env -> constr -> Idset.t
+
+val keep_hyps : env -> Idset.t -> named_context -> named_context
+
+val rename_bound_var : env -> identifier list -> constr -> constr
+
 (*s Modules. *)
 
 type compiled_env
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index c28055ae6b..47e56e3b03 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -189,13 +189,13 @@ let listrec_mconstr env ntypes hyps nparams i indlc =
             else Norec
 	  else
 	    raise (IllFormedInd (LocalNonPos n))
-      | IsMutInd (ind_sp,a) -> 
-          if array_for_all (noccur_between n ntypes) a
-            && List.for_all (noccur_between n ntypes) largs 
+      | IsMutInd ind_sp -> 
+          if List.for_all (noccur_between n ntypes) largs 
 	  then Norec
-          else Imbr(ind_sp,imbr_positive env n (ind_sp,a) largs)
+          else Imbr(ind_sp,imbr_positive env n ind_sp largs)
       | err -> 
-	  if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs 
+	  if noccur_between n ntypes x &&
+             List.for_all (noccur_between n ntypes) largs 
 	  then Norec
 	  else raise (IllFormedInd (LocalNonPos n))
 
@@ -315,9 +315,9 @@ let is_recursive listind =
 let abstract_inductive ntypes hyps (par,np,id,arity,cnames,issmall,isunit,lc) =
   let args = instance_from_named_context (List.rev hyps) in
   let nhyps = List.length hyps in
-  let nparams = List.length args in (* nparams = nhyps - nb(letin) *)
+  let nparams = Array.length args in (* nparams = nhyps - nb(letin) *)
   let new_refs =
-    list_tabulate (fun k -> applist(mkRel (k+nhyps+1),args)) ntypes in
+    list_tabulate (fun k -> appvect(mkRel (k+nhyps+1),args)) ntypes in
   let abs_constructor b = it_mkNamedProd_or_LetIn (substl new_refs b) hyps in
   let lc' = Array.map abs_constructor lc in
   let arity' = it_mkNamedProd_or_LetIn arity hyps in
@@ -329,14 +329,15 @@ let cci_inductive locals env env_ar kind finite inds cst =
   let ids = 
     List.fold_left 
       (fun acc (_,_,_,ar,_,_,_,lc) -> 
-	 Idset.union (global_vars_set (body_of_type ar))
+	 Idset.union (global_vars_set env (body_of_type ar))
 	   (Array.fold_left
-	      (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc)
+	      (fun acc c ->
+                Idset.union (global_vars_set env (body_of_type c)) acc)
 	      acc
 	      lc))
       Idset.empty inds
   in
-  let hyps = keep_hyps ids (named_context env) in
+  let hyps = keep_hyps env ids (named_context env) in
   let inds' =
     if Options.immediate_discharge then
       List.map (abstract_inductive ntypes hyps) inds
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index f5a6ca236e..93bfb54549 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -49,7 +49,7 @@ val mind_check_wellformed : env -> mutual_inductive_entry -> unit
 (* [cci_inductive] checks positivity and builds an inductive body *)
 
 val cci_inductive : 
-  (identifier * variable_path) list -> env -> env -> path_kind -> bool -> 
+  (identifier * variable) list -> env -> env -> path_kind -> bool -> 
    (Sign.rel_context * int * identifier * types * 
     identifier list * bool * bool * types array)
       list ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b528225145..6cd04f76fd 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -21,12 +21,11 @@ type inductive_instance = {
   mis_sp : section_path;
   mis_mib : mutual_inductive_body;
   mis_tyi : int;
-  mis_args : constr array;
   mis_mip : one_inductive_body }
 
 
-let build_mis ((sp,tyi),args) mib =
-  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
+let build_mis (sp,tyi) mib =
+  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi;
     mis_mip = mind_nth_type_packet mib tyi }
 
 let mis_ntypes mis = mis.mis_mib.mind_ntypes
@@ -47,28 +46,18 @@ let mis_consnames mis = mis.mis_mip.mind_consnames
 let mis_conspaths mis =
   let dir = dirpath mis.mis_sp in
   Array.map (fun id -> make_path dir id CCI) mis.mis_mip.mind_consnames
-let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
+let mis_inductive mis = (mis.mis_sp,mis.mis_tyi)
 let mis_finite mis = mis.mis_mip.mind_finite
 
 let mis_typed_nf_lc mis =
   let sign = mis.mis_mib.mind_hyps in
-(*  let args = Array.to_list mis.mis_args in *)
-  Array.map (fun t -> (* Instantiate.instantiate_type sign*) t (*args*))
-    mis.mis_mip.mind_nf_lc
+  mis.mis_mip.mind_nf_lc
 
 let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
 
 let mis_user_lc mis = 
   let sign = mis.mis_mib.mind_hyps in
-(*i
-  let at = mind_user_lc mis.mis_mip in 
-  if Array.length mis.mis_args = 0 then at
-  else 
-  let args = Array.to_list mis.mis_args in
-  Array.map (fun t -> Instantiate.instantiate_constr sign t args) at
-i*)
-  Array.map (fun t -> (*Instantiate.instantiate_type sign*) t (*args*))
-    (mind_user_lc mis.mis_mip)
+  (mind_user_lc mis.mis_mip)
 
 (* gives the vector of constructors and of 
    types of constructors of an inductive definition 
@@ -78,10 +67,9 @@ let mis_type_mconstructs mispec =
   let specif = Array.map body_of_type (mis_user_lc mispec)
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) 
-  and make_Ck k = mkMutConstruct
-		    (((mispec.mis_sp,mispec.mis_tyi),k+1),
-		       mispec.mis_args) in
+  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) 
+  and make_Ck k =
+     mkMutConstruct ((mispec.mis_sp,mispec.mis_tyi),k+1) in
   (Array.init nconstr make_Ck, 
    Array.map (substl (list_tabulate make_Ik ntypes)) specif)
 
@@ -89,7 +77,7 @@ let mis_nf_constructor_type i mispec =
   let specif = mis_nf_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in 
   if i > nconstr then error "Not enough constructors in the type";
   substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
@@ -97,22 +85,17 @@ let mis_constructor_type i mispec =
   let specif = mis_user_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in 
   if i > nconstr then error "Not enough constructors in the type";
   substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
 let mis_arity mis =
-  let hyps = mis.mis_mib.mind_hyps 
-  in let ar = mind_user_arity mis.mis_mip
-  in if Array.length mis.mis_args = 0 then ar
-    else let largs = Array.to_list mis.mis_args in
-      Instantiate.instantiate_type hyps ar largs
+  let hyps = mis.mis_mib.mind_hyps  in
+  mind_user_arity mis.mis_mip
 
 let mis_nf_arity mis =
-  let hyps = mis.mis_mib.mind_hyps 
-  in if Array.length mis.mis_args = 0 then mis.mis_mip.mind_nf_arity
-    else let largs = Array.to_list mis.mis_args in
-  Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
+  let hyps = mis.mis_mib.mind_hyps in
+  mis.mis_mip.mind_nf_arity
 
 let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt
 (*
@@ -124,31 +107,13 @@ let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt
 
 let mis_sort mispec = mispec.mis_mip.mind_sort
 
-let liftn_inductive_instance n depth mis = {
-  mis_sp = mis.mis_sp;
-  mis_mib = mis.mis_mib;
-  mis_tyi = mis.mis_tyi;
-  mis_args = Array.map (liftn n depth) mis.mis_args;
-  mis_mip = mis.mis_mip
-}
-
-let lift_inductive_instance n = liftn_inductive_instance n 1
-
-let substnl_ind_instance l n mis = {
-  mis_sp = mis.mis_sp;
-  mis_mib = mis.mis_mib;
-  mis_tyi = mis.mis_tyi;
-  mis_args = Array.map (substnl l n) mis.mis_args;
-  mis_mip = mis.mis_mip
-}
-
 (* [inductive_family] = [inductive_instance] applied to global parameters *)
 type inductive_family = IndFamily of inductive_instance * constr list
 
 type inductive_type = IndType of inductive_family * constr list
 
-let liftn_inductive_family n d (IndFamily (mis, params)) =
-  IndFamily (liftn_inductive_instance n d mis, List.map (liftn n d) params)
+let liftn_inductive_family n d (IndFamily (mis,params)) =
+  IndFamily (mis, List.map (liftn n d) params)
 let lift_inductive_family n = liftn_inductive_family n 1
 
 let liftn_inductive_type n d (IndType (indf, realargs)) =
@@ -156,7 +121,7 @@ let liftn_inductive_type n d (IndType (indf, realargs)) =
 let lift_inductive_type n = liftn_inductive_type n 1
 
 let substnl_ind_family l n (IndFamily (mis,params)) =
-  IndFamily (substnl_ind_instance l n mis, List.map (substnl l n) params)
+  IndFamily (mis, List.map (substnl l n) params)
 
 let substnl_ind_type l n (IndType (indf,realargs)) =
   IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs)
@@ -198,12 +163,9 @@ let make_default_case_info mis =
 
 (*s Useful functions *)
 
-let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
-let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
-
-let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args)
-let index_of_constructor ((ind_sp,i),args) = i
-let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args)
+let inductive_of_constructor (ind_sp,i) = ind_sp
+let index_of_constructor (ind_sp,i) = i
+let ith_constructor_of_inductive ind_sp i = (ind_sp,i)
 
 exception Induc
 
@@ -222,19 +184,19 @@ let find_mrectype env sigma c =
 let find_inductive env sigma c =
   let (t, l) = whd_betadeltaiota_stack env sigma c in
   match kind_of_term t with
-    | IsMutInd ((sp,i),_ as ind)
+    | IsMutInd ((sp,i) as ind)
         when mind_type_finite (lookup_mind sp env) i -> (ind, l)
     | _ -> raise Induc
 
 let find_coinductive env sigma c =
   let (t, l) = whd_betadeltaiota_stack env sigma c in
   match kind_of_term t with
-    | IsMutInd ((sp,i),_ as ind)
+    | IsMutInd ((sp,i) as ind)
         when not (mind_type_finite (lookup_mind sp env) i) -> (ind, l)
     | _ -> raise Induc
 
 (* raise Induc if not an inductive type *)
-let lookup_mind_specif ((sp,tyi),args as ind) env =
+let lookup_mind_specif ((sp,tyi) as ind) env =
   build_mis ind (lookup_mind sp env)
 
 let find_rectype env sigma ty =
@@ -253,7 +215,7 @@ type constructor_summary = {
 }
 
 let lift_constructor n cs = {
-  cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
+  cs_cstr = cs.cs_cstr;
   cs_params = List.map (lift n) cs.cs_params;
   cs_nargs = cs.cs_nargs;
   cs_args = lift_rel_context n cs.cs_args;
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c8f49ed611..2aee7f4209 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -67,10 +67,10 @@ type inductive_family = IndFamily of inductive_instance * constr list
 val make_ind_family : inductive_instance * constr list -> inductive_family
 val dest_ind_family : inductive_family -> inductive_instance * constr list
 
-val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
-val lift_inductive_family : int -> inductive_family -> inductive_family
-val substnl_ind_family : constr list -> int -> inductive_family 
-  -> inductive_family
+val liftn_inductive_family :
+  int -> int -> inductive_family -> inductive_family
+val lift_inductive_family : 
+  int -> inductive_family -> inductive_family
 
 (*s [inductive_type] = [inductive_family] applied to ``real'' parameters *)
 type inductive_type = IndType of inductive_family * constr list
@@ -90,10 +90,6 @@ val inductive_of_constructor : constructor -> inductive
 val index_of_constructor : constructor -> int
 val ith_constructor_of_inductive : inductive -> int -> constructor
 
-val inductive_path_of_constructor_path : constructor_path -> inductive_path
-val ith_constructor_path_of_inductive_path :
-  inductive_path -> int -> constructor_path
-
 (*s This type gathers useful informations about some instance of a constructor
     relatively to some implicit context (the current one)
 
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index a92de9e604..c1e864523a 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -61,23 +61,20 @@ let instantiate_type sign tty args =
 (* Constants. *)
 
 (* constant_type gives the type of a constant *)
-let constant_type env sigma (sp,args) =
+let constant_type env sigma sp =
   let cb = lookup_constant sp env in
-  (* TODO: check args *)
-(*  instantiate_type cb.const_hyps *) cb.const_type (*(Array.to_list args)*)
+  cb.const_type  
 
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
 
-let constant_value env (sp,args) =
+let constant_value env sp =
   let cb = lookup_constant sp env in
   if cb.const_opaque then raise (NotEvaluableConst Opaque);
   match cb.const_body with
-    | Some body -> 
-        instantiate_constr cb.const_hyps body (Array.to_list args)
-    | None ->
-	raise (NotEvaluableConst NoBody)
+    | Some body -> body
+    | None -> raise (NotEvaluableConst NoBody)
 
 let constant_opt_value env cst =
   try Some (constant_value env cst)
@@ -133,7 +130,7 @@ let destEvalRef c = match kind_of_term c with
   | _ -> anomaly "Not an evaluable reference"
 
 let evaluable_reference sigma env = function
-  | EvalConst (sp,_) -> evaluable_constant env sp
+  | EvalConst sp -> evaluable_constant env sp
   | EvalVar id -> evaluable_named_decl env id
   | EvalRel n -> evaluable_rel_decl env n
   | EvalEvar (ev,_) -> Evd.is_defined sigma ev
diff --git a/kernel/names.ml b/kernel/names.ml
index 3d72326edb..811672ba3d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -316,11 +316,11 @@ module Spmap = Map.Make(SpOrdered)
 
 (* Special references for inductive objects *)
 
-type variable_path = section_path
-type constant_path = section_path
-type inductive_path = section_path * int
-type constructor_path = inductive_path * int
-type mutual_inductive_path = section_path
+type variable = section_path
+type constant = section_path
+type inductive = section_path * int
+type constructor = inductive * int
+type mutual_inductive = section_path
 
 (* Hash-consing of name objects *)
 module Hname = Hashcons.Make(
diff --git a/kernel/names.mli b/kernel/names.mli
index 5af331075b..cdf8c8c83a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -112,11 +112,11 @@ module Sppred : Predicate.S with type elt = section_path
 module Spmap  : Map.S with type key = section_path
 
 (*s Specific paths for declarations *)
-type variable_path = section_path
-type constant_path = section_path
-type inductive_path = section_path * int
-type constructor_path = inductive_path * int
-type mutual_inductive_path = section_path
+type variable = section_path
+type constant = section_path
+type inductive = section_path * int
+type constructor = inductive * int
+type mutual_inductive = section_path
 
 (* Hash-consing *)
 val hcons_names : unit ->
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5c0a4fa634..734187a9c7 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -201,7 +201,7 @@ let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
 
 let reduce_mind_case mia =
   match kind_of_term mia.mconstr with
-    | IsMutConstruct (ind_sp,i as cstr_sp, args) ->
+    | IsMutConstruct (ind_sp,i as cstr_sp) ->
 (*	let ncargs = (fst mia.mci).(i-1) in*)
 	let real_cargs = snd (list_chop (fst mia.mci) mia.mcargs) in
         applist (mia.mlf.(i-1),real_cargs)
@@ -574,17 +574,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
         let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in
 	convert_stacks infos lft1 lft2 v1 v2 u3
 
-     | (FInd (op1,cl1), FInd(op2,cl2)) ->
-         if op1 = op2 then
-           let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in
-           convert_stacks infos lft1 lft2 v1 v2 u1
+     | (FInd op1, FInd op2) ->
+         if op1 = op2
+         then convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
 
-     | (FConstruct (op1,cl1), FConstruct(op2,cl2)) ->
+     | (FConstruct op1, FConstruct op2) ->
          if op1 = op2
-         then
-	   let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in
-           convert_stacks infos lft1 lft2 v1 v2 u1
+         then convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
 
      | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1c7d5e17fb..6eba041828 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -264,14 +264,15 @@ let safe_infer_declaration env = function
       let (j,cst) = safe_infer env t in
       None, assumption_of_judgment env Evd.empty j, cst
 
-type local_names = (identifier * variable_path) list
+type local_names = (identifier * variable) list
 
 let add_global_declaration sp env locals (body,typ,cst) op =
   let env' = add_constraints cst env in
   let ids = match body with 
-    | None -> global_vars_set typ
-    | Some b -> Idset.union (global_vars_set b) (global_vars_set typ) in
-  let hyps = keep_hyps ids (named_context env) in
+    | None -> global_vars_set env typ
+    | Some b ->
+        Idset.union (global_vars_set env b) (global_vars_set env typ) in
+  let hyps = keep_hyps env ids (named_context env) in
   let body, typ =
     if Options.immediate_discharge then
       option_app (fun c -> it_mkNamedLambda_or_LetIn c hyps) body,
@@ -312,8 +313,9 @@ let add_discharged_constant sp r locals env =
 	add_parameter sp typ locals (* Bricolage avant poubelle *) env'
     | Some c -> 
 	(* let c = hcons1_constr c in *)
-	let ids = Idset.union (global_vars_set c) (global_vars_set typ)	in
-	let hyps = keep_hyps ids (named_context env') in
+	let ids =
+          Idset.union (global_vars_set env c) (global_vars_set env typ)	in
+	let hyps = keep_hyps env ids (named_context env') in
 	let sp_hyps =
 	  List.map (fun (id,b,t) -> (List.assoc id locals,b,t)) hyps in
 	let cb =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 90c6e2466b..23a970b494 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -45,7 +45,7 @@ val check_and_push_named_def :
   identifier * constr -> safe_environment -> 
     (constr option * types * constraints) * safe_environment
 
-type local_names = (identifier * variable_path) list
+type local_names = (identifier * variable) list
 
 val add_parameter :
   section_path -> constr -> local_names -> safe_environment -> safe_environment
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 573d6f8094..0d7168c007 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -43,10 +43,12 @@ let pop_named_decl id = function
   | (id',_,_) :: sign -> assert (id = id'); sign
   | [] -> assert false
 let ids_of_named_context = List.map (fun (id,_,_) -> id)
-let rec instance_from_named_context = function
-  | (id,None,_) :: sign -> mkVar id :: instance_from_named_context sign
-  | _ :: sign -> instance_from_named_context sign
-  | [] -> []
+let instance_from_named_context sign =
+  let rec inst_rec = function
+    | (id,None,_) :: sign -> mkVar id :: inst_rec sign
+    | _ :: sign -> inst_rec sign
+    | [] -> [] in
+  Array.of_list (inst_rec sign)
 let map_named_context = map
 let rec mem_named_context id = function
   | (id',_,_) :: _ when id=id' -> true
@@ -59,15 +61,17 @@ let it_named_context_quantifier f = List.fold_left (fun c d -> f d c)
 
 (*s Signatures of ordered section variables *)
 
-type section_declaration = variable_path * constr option * constr
+type section_declaration = variable * constr option * constr
 type section_context = section_declaration list
-let rec instance_from_section_context = function
-  | (sp,None,_) :: sign -> 
-      mkVar (basename sp) :: instance_from_section_context sign
-  | _ :: sign -> instance_from_section_context sign
-  | [] -> []
+let instance_from_section_context sign =
+  let rec inst_rec = function
+    | (sp,None,_) :: sign ->  mkVar (basename sp) :: inst_rec sign
+    | _ :: sign -> inst_rec sign
+    | [] -> [] in
+  Array.of_list (inst_rec sign)
 let instance_from_section_context x =
-  if Options.immediate_discharge then [] else instance_from_section_context x
+  if Options.immediate_discharge then [||]
+  else instance_from_section_context x
 
 (*s Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
@@ -156,23 +160,6 @@ let instantiate_sign sign args =
   in 
   instrec (sign,args)
 
-(* [keep_hyps sign ids] keeps the part of the signature [sign] which 
-   contains the variables of the set [ids], and recursively the variables 
-   contained in the types of the needed variables. *)
-
-let rec keep_hyps needed = function
-  | (id,copt,t as d) ::sign when Idset.mem id needed ->
-      let globc = 
-	match copt with
-	  | None -> Idset.empty
-	  | Some c -> global_vars_set c in
-      let needed' =
-	Idset.union (global_vars_set (body_of_type t)) 
-	  (Idset.union globc needed) in
-      d :: (keep_hyps needed' sign)
-  | _::sign -> keep_hyps needed sign
-  | [] -> []
-
 (*************************)
 (*   Names environments  *)
 (*************************)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 6180906cbe..dd5aba6c6d 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -40,15 +40,14 @@ val it_named_context_quantifier :
   (named_declaration -> constr -> constr) -> constr -> named_context -> constr
 val instantiate_sign :
   named_context -> constr list -> (identifier * constr) list
-val keep_hyps : Idset.t -> named_context -> named_context
-val instance_from_named_context : named_context -> constr list
+val instance_from_named_context : named_context -> constr array
 
 (*s Signatures of ordered section variables *)
 
-type section_declaration = variable_path * constr option * constr
+type section_declaration = variable * constr option * constr
 type section_context = section_declaration list
 
-val instance_from_section_context : section_context -> constr list
+val instance_from_section_context : section_context -> constr array
 
 (*s Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 8b276c0683..e79fd5fb36 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -24,7 +24,7 @@ type existential_key = int
 type pattern_source = DefaultPat of int | RegularPat
 type case_style = PrintLet | PrintIf | PrintCases
 type case_printing =
-    inductive_path * identifier array * int
+    inductive * identifier array * int
     * case_style option * pattern_source array
 type case_info = int * case_printing
 
@@ -62,9 +62,9 @@ let family_of_sort = function
 
 type global_reference =
   | VarRef of section_path
-  | ConstRef of constant_path
-  | IndRef of inductive_path
-  | ConstructRef of constructor_path
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
 
 (********************************************************************)
 (*       Constructions as implemented                               *)
@@ -80,9 +80,6 @@ module type InternalSig = sig
 
 type constr
 type existential = existential_key * constr array
-type constant = section_path * constr array
-type constructor = constructor_path * constr array
-type inductive = inductive_path * constr array
 type rec_declaration = name array * constr array * constr array
 type fixpoint = (int array * int) * rec_declaration
 type cofixpoint = int * rec_declaration
@@ -143,9 +140,6 @@ struct
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type 'constr existential = existential_key * 'constr array
-type 'constr constant = constant_path * 'constr array
-type 'constr constructor = constructor_path * 'constr array
-type 'constr inductive = inductive_path * 'constr array
 type ('constr, 'types) rec_declaration =
     name array * 'types array * 'constr array
 type ('constr, 'types) fixpoint =
@@ -170,9 +164,9 @@ type ('constr, 'types) kind_of_term =
   | IsLetIn        of name * 'constr * 'types * 'constr
   | IsApp          of 'constr * 'constr array
   | IsEvar         of 'constr existential
-  | IsConst        of 'constr constant
-  | IsMutInd       of 'constr inductive
-  | IsMutConstruct of 'constr constructor
+  | IsConst        of constant
+  | IsMutInd       of inductive
+  | IsMutConstruct of constructor
   | IsMutCase      of case_info * 'constr * 'constr * 'constr array
   | IsFix          of ('constr, 'types) fixpoint
   | IsCoFix        of ('constr, 'types) cofixpoint
@@ -180,9 +174,6 @@ type ('constr, 'types) kind_of_term =
 type constr = (constr,constr) kind_of_term
 
 type existential = existential_key * constr array
-type constant = constant_path * constr array
-type constructor = constructor_path * constr array
-type inductive = inductive_path * constr array
 type rec_declaration = name array * constr array * constr array
 type fixpoint = (int array * int) * rec_declaration
 type cofixpoint = int * rec_declaration
@@ -204,10 +195,9 @@ let comp_term t1 t2 =
       n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
   | IsApp (c1,l1), IsApp (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
   | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 (==) l1 l2
-  | IsConst (c1,l1), IsConst (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
-  | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
-  | IsMutConstruct (c1,l1), IsMutConstruct (c2,l2) ->
-      c1 == c2 & array_for_all2 (==) l1 l2
+  | IsConst c1, IsConst c2 -> c1 == c2
+  | IsMutInd c1, IsMutInd c2 -> c1 == c2
+  | IsMutConstruct c1, IsMutConstruct c2 -> c1 == c2
   | IsMutCase (ci1,p1,c1,bl1), IsMutCase (ci2,p2,c2,bl2) ->
       ci1 == ci2 & p1 == p2 & c1 == c2 & array_for_all2 (==) bl1 bl2
   | IsFix (ln1,(lna1,tl1,bl1)), IsFix (ln2,(lna2,tl2,bl2)) ->
@@ -233,10 +223,9 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id)) t =
   | IsLetIn (na,b,t,c) -> IsLetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
   | IsApp (c,l) -> IsApp (sh_rec c, Array.map sh_rec l)
   | IsEvar (e,l) -> IsEvar (e, Array.map sh_rec l)
-  | IsConst (c,l) -> IsConst (sh_sp c, Array.map sh_rec l)
-  | IsMutInd ((sp,i),l) -> IsMutInd ((sh_sp sp,i), Array.map sh_rec l)
-  | IsMutConstruct (((sp,i),j),l) ->
-      IsMutConstruct (((sh_sp sp,i),j), Array.map sh_rec l)
+  | IsConst c -> IsConst (sh_sp c)
+  | IsMutInd (sp,i) -> IsMutInd (sh_sp sp,i)
+  | IsMutConstruct ((sp,i),j) -> IsMutConstruct ((sh_sp sp,i),j)
   | IsMutCase (ci,p,c,bl) -> (* TO DO: extract ind_sp *)
       IsMutCase (ci, sh_rec p, sh_rec c, Array.map sh_rec bl)
   | IsFix (ln,(lna,tl,bl)) ->
@@ -465,17 +454,9 @@ let isApp c = match kind_of_term c with IsApp _ -> true | _ -> false
 
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
-  | IsConst (sp, a as r) -> r
+  | IsConst sp -> sp
   | _ -> invalid_arg "destConst"
 
-let path_of_const c = match kind_of_term c with
-  | IsConst (sp,_) -> sp
-  | _ -> anomaly "path_of_const called with bad args"
-
-let args_of_const c = match kind_of_term c with
-  | IsConst (_,args) -> args
-  | _ -> anomaly "args_of_const called with bad args"
-
 let isConst c = match kind_of_term c with IsConst _ -> true | _ -> false
 
 (* Destructs an existential variable *)
@@ -491,28 +472,12 @@ let num_of_evar c = match kind_of_term c with
 let destMutInd c = match kind_of_term c with
   | IsMutInd (sp, a as r) -> r
   | _ -> invalid_arg "destMutInd"
-	
-let op_of_mind c = match kind_of_term c with
-  | IsMutInd (ind_sp,_) -> ind_sp
-  | _ -> anomaly "op_of_mind called with bad args"
-
-let args_of_mind c = match kind_of_term c with
-  | IsMutInd (_,args) -> args
-  | _ -> anomaly "args_of_mind called with bad args"
 
 (* Destructs a constructor *)
 let destMutConstruct c = match kind_of_term c with
   | IsMutConstruct (sp, a as r) -> r
   | _ -> invalid_arg "dest"
 
-let op_of_mconstr c = match kind_of_term c with
-  | IsMutConstruct (sp,_) -> sp
-  | _ -> anomaly "op_of_mconstr called with bad args"
-
-let args_of_mconstr c = match kind_of_term c with
-  | IsMutConstruct (_,args) -> args
-  | _ -> anomaly "args_of_mconstr called with bad args"
-
 let isMutConstruct c = match kind_of_term c with
     IsMutConstruct _ -> true | _ -> false
 
@@ -571,16 +536,14 @@ let rec strip_head_cast c = match kind_of_term c with
    the usual representation of the constructions; it is not recursive *)
 
 let fold_constr f acc c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> acc
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> acc
   | IsCast (c,t) -> f (f acc c) t
   | IsProd (_,t,c) -> f (f acc t) c
   | IsLambda (_,t,c) -> f (f acc t) c
   | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c
   | IsApp (c,l) -> Array.fold_left f (f acc c) l
   | IsEvar (_,l) -> Array.fold_left f acc l
-  | IsConst (_,l) -> Array.fold_left f acc l
-  | IsMutInd (_,l) -> Array.fold_left f acc l
-  | IsMutConstruct (_,l) -> Array.fold_left f acc l
   | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
   | IsFix (_,(lna,tl,bl)) ->
       let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
@@ -597,16 +560,14 @@ let fold_constr f acc c = match kind_of_term c with
    each binder traversal; it is not recursive *)
 
 let fold_constr_with_binders g f n acc c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> acc
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> acc
   | IsCast (c,t) -> f n (f n acc c) t
   | IsProd (_,t,c) -> f (g n) (f n acc t) c
   | IsLambda (_,t,c) -> f (g n) (f n acc t) c
   | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
   | IsApp (c,l) -> Array.fold_left (f n) (f n acc c) l
   | IsEvar (_,l) -> Array.fold_left (f n) acc l
-  | IsConst (_,l) -> Array.fold_left (f n) acc l
-  | IsMutInd (_,l) -> Array.fold_left (f n) acc l
-  | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l
   | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | IsFix (_,(lna,tl,bl)) -> 
       let n' = iterate g (Array.length tl) n in
@@ -622,16 +583,14 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
    not specified *)
 
 let iter_constr f c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> ()
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> ()
   | IsCast (c,t) -> f c; f t
   | IsProd (_,t,c) -> f t; f c
   | IsLambda (_,t,c) -> f t; f c
   | IsLetIn (_,b,t,c) -> f b; f t; f c
   | IsApp (c,l) -> f c; Array.iter f l
   | IsEvar (_,l) -> Array.iter f l
-  | IsConst (_,l) -> Array.iter f l
-  | IsMutInd (_,l) -> Array.iter f l
-  | IsMutConstruct (_,l) -> Array.iter f l
   | IsMutCase (_,p,c,bl) -> f p; f c; Array.iter f bl
   | IsFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | IsCoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
@@ -643,16 +602,14 @@ let iter_constr f c = match kind_of_term c with
    subterms are processed is not specified *)
 
 let iter_constr_with_binders g f n c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> ()
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> ()
   | IsCast (c,t) -> f n c; f n t
   | IsProd (_,t,c) -> f n t; f (g n) c
   | IsLambda (_,t,c) -> f n t; f (g n) c
   | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c
   | IsApp (c,l) -> f n c; Array.iter (f n) l
   | IsEvar (_,l) -> Array.iter (f n) l
-  | IsConst (_,l) -> Array.iter (f n) l
-  | IsMutInd (_,l) -> Array.iter (f n) l
-  | IsMutConstruct (_,l) -> Array.iter (f n) l
   | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
   | IsFix (_,(_,tl,bl)) -> 
       Array.iter (f n) tl;
@@ -666,16 +623,14 @@ let iter_constr_with_binders g f n c = match kind_of_term c with
    not specified *)
 
 let map_constr f c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> c
   | IsCast (c,t) -> mkCast (f c, f t)
   | IsProd (na,t,c) -> mkProd (na, f t, f c)
   | IsLambda (na,t,c) -> mkLambda (na, f t, f c)
   | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
   | IsApp (c,l) -> mkApp (f c, Array.map f l)
   | IsEvar (e,l) -> mkEvar (e, Array.map f l)
-  | IsConst (c,l) -> mkConst (c, Array.map f l)
-  | IsMutInd (c,l) -> mkMutInd (c, Array.map f l)
-  | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l)
   | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl)
   | IsFix (ln,(lna,tl,bl)) ->
       mkFix (ln,(lna,Array.map f tl,Array.map f bl))
@@ -689,16 +644,14 @@ let map_constr f c = match kind_of_term c with
    subterms are processed is not specified *)
 
 let map_constr_with_binders g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> c
   | IsCast (c,t) -> mkCast (f l c, f l t)
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
   | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
   | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
   | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
-  | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
-  | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al)
   | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl)
   | IsFix (ln,(lna,tl,bl)) ->
       let l' = iterate g (Array.length tl) l in
@@ -714,16 +667,14 @@ let map_constr_with_binders g f l c = match kind_of_term c with
    and the order with which subterms are processed is not specified *)
 
 let map_constr_with_named_binders g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> c
   | IsCast (c,t) -> mkCast (f l c, f l t)
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
   | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
   | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
   | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
-  | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
-  | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al)
   | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl)
   | IsFix (ln,(lna,tl,bl)) ->
       let l' = Array.fold_left (fun l na -> g na l) l lna in
@@ -765,7 +716,8 @@ let array_map_left_pair f a g b =
   end
 
 let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> c
   | IsCast (c,t) -> let c' = f l c in mkCast (c', f l t)
   | IsProd (na,t,c) -> let t' = f l t in mkProd (na, t', f (g l) c)
   | IsLambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c)
@@ -774,9 +726,6 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
   | IsApp (c,al) -> 
       let c' = f l c in mkApp (c', array_map_left (f l) al)
   | IsEvar (e,al) -> mkEvar (e, array_map_left (f l) al)
-  | IsConst (c,al) -> mkConst (c, array_map_left (f l) al)
-  | IsMutInd (c,al) -> mkMutInd (c, array_map_left (f l) al)
-  | IsMutConstruct (c,al) -> mkMutConstruct (c, array_map_left (f l) al)
   | IsMutCase (ci,p,c,bl) ->
       let p' = f l p in let c' = f l c in
       mkMutCase (ci, p', c', array_map_left (f l) bl)
@@ -791,16 +740,14 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
 
 (* strong *)
 let map_constr_with_full_binders g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
+  | (IsRel _ | IsMeta _ | IsVar _   | IsSort _ | IsConst _ | IsMutInd _
+    | IsMutConstruct _) -> c
   | IsCast (c,t) -> mkCast (f l c, f l t)
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c)
   | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g (na,Some b,t) l) c)
   | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
   | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
-  | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
-  | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al)
   | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl)
   | IsFix (ln,(lna,tl,bl)) ->
       let l' =
@@ -837,10 +784,9 @@ let compare_constr f t1 t2 =
           f h1 h2 & List.for_all2 f l1 l2
         else false
   | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
-  | IsConst (c1,l1), IsConst (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
-  | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
-  | IsMutConstruct (c1,l1), IsMutConstruct (c2,l2) ->
-      c1 = c2 & array_for_all2 f l1 l2
+  | IsConst c1, IsConst c2 -> c1 = c2
+  | IsMutInd c1, IsMutInd c2 -> c1 = c2
+  | IsMutConstruct c1, IsMutConstruct c2 -> c1 = c2
   | IsMutCase (_,p1,c1,bl1), IsMutCase (_,p2,c2,bl2) ->
       f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
   | IsFix (ln1,(_,tl1,bl1)), IsFix (ln2,(_,tl2,bl2)) ->
@@ -1421,25 +1367,6 @@ let le_kind_implicit k1 k2 =
   (k1=mkImplicit) or (isprop k1) or (k2=mkImplicit) or (is_Type k2)
 
 
-(* Returns the list of global variables in a term *)
-
-let rec global_varsl l constr = match kind_of_term constr with
-  | IsVar id -> id::l
-  | _        -> fold_constr global_varsl l constr
-
-let global_vars = global_varsl []
-
-let global_vars_decl = function
-  | (_, None, t) -> global_vars t
-  | (_, Some c, t) -> (global_vars c)@(global_vars t)
-
-let global_vars_set constr = 
-  let rec filtrec acc c = match kind_of_term c with
-    | IsVar id -> Idset.add id acc
-    | _        -> fold_constr filtrec acc c
-  in 
-  filtrec Idset.empty constr
-
 (* Rem: end of import from old module Generic *)
 
 (* Various occurs checks *)
@@ -1448,7 +1375,7 @@ let global_vars_set constr =
  * false otherwise *)
 let occur_const s c = 
   let rec occur_rec c = match kind_of_term c with
-    | IsConst (sp,_) when sp=s -> raise Occur
+    | IsConst sp when sp=s -> raise Occur
     | _ -> iter_constr occur_rec c
   in 
   try occur_rec c; false with Occur -> true
@@ -1460,18 +1387,6 @@ let occur_evar n c =
   in 
   try occur_rec c; false with Occur -> true
 
-let occur_var s c = 
-  let rec occur_rec c = match kind_of_term c with
-    | IsVar id when id=s -> raise Occur
-    | _ -> iter_constr occur_rec c
-  in 
-  try occur_rec c; false with Occur -> true
-
-let occur_var_in_decl hyp (_,c,typ) =
-  match c with
-    | None -> occur_var hyp (body_of_type typ)
-    | Some body -> occur_var hyp (body_of_type typ) || occur_var hyp body
-
 (***************************************)
 (*  alpha and eta conversion functions *)                         
 (***************************************)
@@ -1529,23 +1444,6 @@ let eta_eq_constr =
   in aux
 
 
-(* This renames bound variables with fresh and distinct names *)
-(* in such a way that the printer doe not generate new names  *)
-(* and therefore that printed names are the intern names      *)
-(* In this way, tactics such as Induction works well          *)
-
-let rec rename_bound_var l c =
-  match kind_of_term c with
-  | IsProd (Name s,c1,c2)  ->
-      if dependent (mkRel 1) c2 then
-        let s' = next_ident_away s (global_vars c2@l) in
-        mkProd (Name s', c1, rename_bound_var (s'::l) c2)
-      else 
-	mkProd (Name s, c1, rename_bound_var l c2)
-  | IsProd (Anonymous,c1,c2) -> mkProd (Anonymous, c1, rename_bound_var l c2)
-  | IsCast (c,t) -> mkCast (rename_bound_var l c, t)
-  | x -> c
-
 (***************************)
 (*  substitution functions *)                         
 (***************************)
@@ -1789,10 +1687,10 @@ type constr_operator =
   | OpSort of sorts
   | OpRel of int | OpVar of identifier
   | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
-  | OpApp | OpConst of constant_path
+  | OpApp | OpConst of constant
   | OpEvar of existential_key
-  | OpMutInd of inductive_path
-  | OpMutConstruct of constructor_path
+  | OpMutInd of inductive
+  | OpMutConstruct of constructor
   | OpMutCase of case_info
   | OpRec of fix_kind * name array
 
@@ -1806,10 +1704,10 @@ let splay_constr c = match kind_of_term c with
   | IsLambda (x, t1, t2)       -> OpLambda x, [|t1;t2|]
   | IsLetIn (x, b, t1, t2)     -> OpLetIn x, [|b;t1;t2|]
   | IsApp (f,a)                -> OpApp, Array.append [|f|] a
-  | IsConst (sp, a)            -> OpConst sp, a
+  | IsConst sp                 -> OpConst sp,[||]
   | IsEvar (sp, a)             -> OpEvar sp, a
-  | IsMutInd (ind_sp, l)       -> OpMutInd ind_sp, l
-  | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, l
+  | IsMutInd ind_sp            -> OpMutInd ind_sp,[||]
+  | IsMutConstruct cstr_sp     -> OpMutConstruct cstr_sp, [||]
   | IsMutCase (ci,p,c,bl)      -> OpMutCase ci, Array.append [|p;c|] bl
   | IsFix (fi,(lna,tl,bl))     -> OpRec (RFix fi,lna), Array.append tl bl
   | IsCoFix (fi,(lna,tl,bl))   -> OpRec (RCoFix fi,lna), Array.append tl bl
@@ -1824,10 +1722,10 @@ let gather_constr = function
   | OpLambda x, [|t1;t2|] -> mkLambda (x, t1, t2)
   | OpLetIn x, [|b;t1;t2|] -> mkLetIn (x, b, t1, t2)
   | OpApp, v     -> let f = v.(0) and a = array_tl v in mkApp (f, a)
-  | OpConst sp, a -> mkConst (sp, a)
+  | OpConst sp, [||] -> mkConst sp
   | OpEvar sp, a  -> mkEvar (sp, a) 
-  | OpMutInd ind_sp, l        -> mkMutInd (ind_sp, l) 
-  | OpMutConstruct cstr_sp, l -> mkMutConstruct (cstr_sp, l)
+  | OpMutInd ind_sp, [||]    -> mkMutInd ind_sp
+  | OpMutConstruct cstr_sp, [||] -> mkMutConstruct cstr_sp
   | OpMutCase ci,  v    ->
       let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2)
       in mkMutCase (ci, p, c, bl)   
@@ -1849,10 +1747,10 @@ let splay_constr_with_binders c = match kind_of_term c with
   | IsLambda (x, t1, t2)       -> OpLambda x, [x,None,t1], [|t2|]
   | IsLetIn (x, b, t1, t2)     -> OpLetIn x, [x,Some b,t1], [|t2|]
   | IsApp (f,v)                -> OpApp, [], Array.append [|f|] v
-  | IsConst (sp, a)            -> OpConst sp, [], a
+  | IsConst sp                 -> OpConst sp, [], [||]
   | IsEvar (sp, a)             -> OpEvar sp, [], a
-  | IsMutInd (ind_sp, l)       -> OpMutInd ind_sp, [], l
-  | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, [], l
+  | IsMutInd ind_sp            -> OpMutInd ind_sp, [], [||]
+  | IsMutConstruct cstr_sp     -> OpMutConstruct cstr_sp, [], [||]
   | IsMutCase (ci,p,c,bl)      ->
       let v = Array.append [|p;c|] bl in OpMutCase ci, [], v
   | IsFix (fi,(na,tl,bl)) ->
@@ -1878,10 +1776,10 @@ let gather_constr_with_binders = function
   | OpLambda _, [x,None,t1], [|t2|] -> mkLambda (x, t1, t2)
   | OpLetIn _, [x,Some b,t1], [|t2|] -> mkLetIn (x, b, t1, t2)
   | OpApp, [], v     -> let f = v.(0) and a = array_tl v in mkApp (f, a)
-  | OpConst sp, [], a -> mkConst (sp, a)
+  | OpConst sp, [], [||] -> mkConst sp
   | OpEvar sp, [], a  -> mkEvar (sp, a) 
-  | OpMutInd ind_sp, [], l        -> mkMutInd (ind_sp, l) 
-  | OpMutConstruct cstr_sp, [], l -> mkMutConstruct (cstr_sp, l)
+  | OpMutInd ind_sp, [], [||]        -> mkMutInd ind_sp
+  | OpMutConstruct cstr_sp, [], [||] -> mkMutConstruct cstr_sp
   | OpMutCase ci, [], v    ->
       let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2)
       in mkMutCase (ci, p, c, bl)   
diff --git a/kernel/term.mli b/kernel/term.mli
index ca0bae8385..248d572276 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -41,7 +41,7 @@ type existential_key = int
 type pattern_source = DefaultPat of int | RegularPat
 type case_style = PrintLet | PrintIf | PrintCases
 type case_printing =
-    inductive_path * identifier array * int
+    inductive * identifier array * int
     * case_style option * pattern_source array
 (* the integer is the number of real args, needed for reduction *)
 type case_info = int * case_printing
@@ -52,9 +52,6 @@ sig
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type 'constr existential = existential_key * 'constr array
-type 'constr constant = constant_path * 'constr array
-type 'constr constructor = constructor_path * 'constr array
-type 'constr inductive = inductive_path * 'constr array
 type ('constr, 'types) rec_declaration =
     name array * 'types array * 'constr array
 type ('constr, 'types) fixpoint =
@@ -71,9 +68,9 @@ end
 
 type global_reference =
   | VarRef of section_path
-  | ConstRef of constant_path
-  | IndRef of inductive_path
-  | ConstructRef of constructor_path
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
 
 (*s*******************************************************************)
 (* The type of constructions *)
@@ -121,17 +118,14 @@ type ('constr, 'types) kind_of_term =
   | IsLetIn        of name * 'constr * 'types * 'constr
   | IsApp          of 'constr * 'constr array
   | IsEvar         of 'constr existential
-  | IsConst        of 'constr constant
-  | IsMutInd       of 'constr inductive
-  | IsMutConstruct of 'constr constructor
+  | IsConst        of constant
+  | IsMutInd       of inductive
+  | IsMutConstruct of constructor
   | IsMutCase      of case_info * 'constr * 'constr * 'constr array
   | IsFix          of ('constr, 'types) fixpoint
   | IsCoFix        of ('constr, 'types) cofixpoint
 
 type existential = existential_key * constr array
-type constant = constant_path * constr array
-type constructor = constructor_path * constr array
-type inductive = inductive_path * constr array
 type rec_declaration = name array * types array * constr array
 type fixpoint = (int array * int) * rec_declaration
 type cofixpoint = int * rec_declaration
@@ -327,10 +321,8 @@ i*)
 val destApplication : constr -> constr * constr array
 
 (* Destructs a constant *)
-val destConst : constr -> constant_path * constr array
+val destConst : constr -> constant
 val isConst : constr -> bool
-val path_of_const : constr -> constant_path
-val args_of_const : constr -> constr array
 
 (* Destructs an existential variable *)
 val destEvar : constr -> existential_key * constr array
@@ -338,14 +330,10 @@ val num_of_evar : constr -> existential_key
 
 (* Destructs a (co)inductive type *)
 val destMutInd : constr -> inductive
-val op_of_mind : constr -> inductive_path
-val args_of_mind : constr -> constr array
 
 (* Destructs a constructor *)
 val destMutConstruct : constr -> constructor
 val isMutConstruct : constr -> bool
-val op_of_mconstr : constr -> constructor_path
-val args_of_mconstr : constr -> constr array
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 val destCase : constr -> case_info * constr * constr * constr array
@@ -479,14 +467,6 @@ val subst1 : constr -> constr -> constr
 val substl_decl : constr list -> named_declaration -> named_declaration
 val subst1_decl : constr -> named_declaration -> named_declaration
 
-(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
-val global_vars : constr -> identifier list
-
-(* [global_vars_decl d] returns the list of [id]'s occurring as [VAR
-    id] in declaration [d] (type and body if any) *)
-val global_vars_decl : named_declaration -> identifier list
-
-val global_vars_set : constr -> Idset.t
 val replace_vars : (identifier * constr) list -> constr -> constr
 val subst_var : identifier -> constr -> constr
 
@@ -518,25 +498,18 @@ val occur_existential : constr -> bool
 
 (* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs 
    in c, [false] otherwise *)
-val occur_const : constant_path -> constr -> bool
+val occur_const : constant -> constr -> bool
 
 (* [(occur_evar ev c)] returns [true] if existential variable [ev] occurs 
    in c, [false] otherwise *)
 val occur_evar : existential_key -> constr -> bool
 
-(* [(occur_var id c)] returns [true] if variable [id] occurs free
-   in c, [false] otherwise *)
-val occur_var : identifier -> constr -> bool
-
-val occur_var_in_decl : identifier -> named_declaration -> bool
-
 (* [dependent M N] is true iff M is eq\_constr with a subterm of N 
    M is appropriately lifted through abstractions of N *)
 val dependent : constr -> constr -> bool
 
 (* strips head casts and flattens head applications *)
 val strip_head_cast : constr -> constr
-val rename_bound_var : identifier list -> constr -> constr
 val eta_reduce_head : constr -> constr
 val eq_constr : constr -> constr -> bool
 val eta_eq_constr : constr -> constr -> bool
@@ -566,10 +539,10 @@ type constr_operator =
   | OpSort of sorts
   | OpRel of int | OpVar of identifier
   | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
-  | OpApp | OpConst of constant_path
+  | OpApp | OpConst of constant
   | OpEvar of existential_key
-  | OpMutInd of inductive_path
-  | OpMutConstruct of constructor_path
+  | OpMutInd of inductive
+  | OpMutConstruct of constructor
   | OpMutCase of case_info
   | OpRec of fix_kind * name array
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4342b5793e..e8e8f35b94 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -460,7 +460,7 @@ let check_term env mind_recvec f =
 	      Mrec(i) -> crec env' n' ((1,mind_recvec.(i))::lst') (lr,b)
             | Imbr((sp,i) as ind_sp,lrc) ->           
 	        let sprecargs =
-                  mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in
+                  mis_recargs (lookup_mind_specif ind_sp env) in
                 let lc = Array.map
                   (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
                 in crec env' n' ((1,lc)::lst') (lr,b)
@@ -589,7 +589,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	     anomaly "check_subterm_rec_meta: Bad occurrence of recursive call"
        | _ -> raise (FixGuardError NotEnoughAbstractionInFixBody) in
    let (env',c,d) = check_occur env 1 def in
-   let ((sp,tyi),_ as mind, largs) = 
+   let ((sp,tyi) as mind, largs) = 
      try find_inductive env' sigma c 
      with Induc -> raise (FixGuardError RecursionNotOnInductiveType) in
    let mind_recvec = mis_recargs (lookup_mind_specif mind env') in 
@@ -690,17 +690,14 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	| IsLetIn (x,a,b,c) -> 
 	    anomaly "check_rec_call: should have been reduced"
 
-	| IsMutInd (_,la) -> 
-	     (array_for_all (check_rec_call env n lst) la) &&
+	| IsMutInd _ -> 
              (List.for_all (check_rec_call env n lst) l)
 
-	| IsMutConstruct (_,la) -> 
-	     (array_for_all (check_rec_call env n lst) la) &&
+	| IsMutConstruct _ -> 
              (List.for_all (check_rec_call env n lst) l)
 
-	| IsConst (sp,la) as c -> 
+	| IsConst sp -> 
             (try 
-	    (array_for_all (check_rec_call env n lst) la) &&
             (List.for_all (check_rec_call env n lst) l)
 	     with (FixGuardError _ ) as e
 		 -> if evaluable_constant env sp then 
@@ -791,7 +788,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
 	    raise (CoFixGuardError (CodomainNotInductiveType b))
   in
   let (mind, _) = codomain_is_coind env deftype in
-  let ((sp,tyi),_) = mind in
+  let (sp,tyi) = mind in
   let lvlra = mis_recargs (lookup_mind_specif mind env) in
   let vlra = lvlra.(tyi) in  
   let rec check_rec_call env alreadygrd n vlra  t =
@@ -815,9 +812,9 @@ let check_guard_rec_meta env sigma nbfix def deftype =
              else  
 	       error "check_guard_rec_meta: ???"  (* ??? *)
 		 
-	| IsMutConstruct ((_,i as cstr_sp),l)  ->
+	| IsMutConstruct (_,i as cstr_sp)  ->
             let lra =vlra.(i-1) in 
-            let mI = inductive_of_constructor (cstr_sp,l) in
+            let mI = inductive_of_constructor cstr_sp in
 	    let mis = lookup_mind_specif mI env in
             let _,realargs = list_chop (mis_nparams mis) args in
             let rec process_args_of_constr l lra =
@@ -835,8 +832,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
                             (process_args_of_constr lr lrar)
 			    
                        |  (Imbr((sp,i) as ind_sp,lrc)::lrar)  ->
-			    let mis =
-			      lookup_mind_specif (ind_sp,[||]) env in
+			    let mis = lookup_mind_specif ind_sp env in
                             let sprecargs = mis_recargs mis in
                             let lc = (Array.map 
                                         (List.map 
@@ -934,6 +930,9 @@ let control_only_guard env sigma =
   let rec control_rec c = match kind_of_term c with
     | IsRel _ | IsVar _    -> ()
     | IsSort _ | IsMeta _ -> ()
+    | IsMutInd _       -> ()
+    | IsMutConstruct _ -> ()
+    | IsConst _        -> ()
     | IsCoFix (_,(_,tys,bds) as cofix) ->
 	check_cofix env sigma cofix;
 	Array.iter control_rec tys;
@@ -943,9 +942,6 @@ let control_only_guard env sigma =
 	Array.iter control_rec tys;
 	Array.iter control_rec bds;
     | IsMutCase(_,p,c,b) ->control_rec p;control_rec c;Array.iter control_rec b
-    | IsMutInd (_,cl)       -> Array.iter control_rec cl
-    | IsMutConstruct (_,cl) -> Array.iter control_rec cl
-    | IsConst (_,cl)        -> Array.iter control_rec cl
     | IsEvar (_,cl)         -> Array.iter control_rec cl
     | IsApp (_,cl)         -> Array.iter control_rec cl
     | IsCast (c1,c2)       -> control_rec c1; control_rec c2