kernel/declarations becomes a pure mli

 - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
 - the functions that were in declarations.ml (mostly substitution utilities
   and hashcons) are now in kernel/declareops.ml

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

20 files changed, 406 insertions, 557 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d0751475b..0f3636632 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -719,7 +719,7 @@ let compile env c =
 let compile_constant_body env = function
   | Undef _ | OpaqueDef _ -> BCconstant
   | Def sb ->
-      let body = Declarations.force sb in
+      let body = Lazyconstr.force sb in
       match kind_of_term body with
 	| Const kn' ->
 	    (* we use the canonical name of the constant*)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index fb3303687..e8e35ee85 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -121,14 +121,14 @@ type recipe = {
 
 let on_body f = function
   | Undef inl -> Undef inl
-  | Def cs -> Def (Declarations.from_val (f (Declarations.force cs)))
+  | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
   | OpaqueDef lc ->
-    OpaqueDef (Declarations.opaque_from_val (f (Declarations.force_opaque lc)))
+    OpaqueDef (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))
 
 let constr_of_def = function
   | Undef _ -> assert false
-  | Def cs -> Declarations.force cs
-  | OpaqueDef lc -> Declarations.force_opaque lc
+  | Def cs -> Lazyconstr.force cs
+  | OpaqueDef lc -> Lazyconstr.force_opaque lc
 
 let cook_constant env r =
   let cb = r.d_from in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
deleted file mode 100644
index 62a3170f2..000000000
--- a/kernel/declarations.ml
+++ /dev/null
@@ -1,430 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* This file is a late renaming in May 2000 of constant.ml which
-   itself was made for V7.0 in Aug 1999 out of a dispatch by
-   Jean-Christophe Filliâtre of Chet Murthy's constants.ml in V5.10.5
-   into cooking.ml, declare.ml and constant.ml, ...; renaming done
-   because the new contents exceeded in extent what the name
-   suggested *)
-(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
-(* Declarations for the module systems added by Jacek Chrzaszcz, Aug 2002 *)
-(* Miscellaneous extensions, cleaning or restructurations by Bruno
-   Barras, Hugo Herbelin, Jean-Christophe Filliâtre, Pierre Letouzey *)
-
-(* This module defines the types of global declarations. This includes
-   global constants/axioms, mutual inductive definitions and the
-   module system *)
-
-open Util
-open Names
-open Univ
-open Term
-open Sign
-open Mod_subst
-
-type engagement = ImpredicativeSet
-
-(*s Constants (internal representation) (Definition/Axiom) *)
-
-type polymorphic_arity = {
-  poly_param_levels : universe option list;
-  poly_level : universe;
-}
-
-type constant_type =
-  | NonPolymorphicType of types
-  | PolymorphicArity of rel_context * polymorphic_arity
-
-type constr_substituted = constr substituted
-
-let from_val = from_val
-
-let force = force subst_mps
-
-let subst_constr_subst = subst_substituted
-
-(** Opaque proof terms are not loaded immediately, but are there
-    in a lazy form. Forcing this lazy may trigger some unmarshal of
-    the necessary structure. The ['a substituted] type isn't really great
-    here, so we store "manually" a substitution list, the younger one at top.
-*)
-
-type lazy_constr = constr_substituted Lazy.t * substitution list
-
-let force_lazy_constr (c,l) =
-  List.fold_right subst_constr_subst l (Lazy.force c)
-
-let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c
-
-let make_lazy_constr c = (c, [])
-
-let force_opaque lc = force (force_lazy_constr lc)
-
-let opaque_from_val c = (Lazy.lazy_from_val (from_val c), [])
-
-let subst_lazy_constr sub (c,l) = (c,sub::l)
-
-(** Inlining level of parameters at functor applications.
-    None means no inlining *)
-
-type inline = int option
-
-(** A constant can have no body (axiom/parameter), or a
-    transparent body, or an opaque one *)
-
-type constant_def =
-  | Undef of inline
-  | Def of constr_substituted
-  | OpaqueDef of lazy_constr
-
-type native_name =
-  | Linked of string
-  | LinkedLazy of string
-  | LinkedInteractive of string
-  | NotLinked
-
-type constant_body = {
-    const_hyps : section_context; (* New: younger hyp at top *)
-    const_body : constant_def;
-    const_type : constant_type;
-    const_body_code : Cemitcodes.to_patch_substituted;
-    const_constraints : constraints;
-    const_native_name : native_name ref;
-    const_inline_code : bool }
-
-let body_of_constant cb = match cb.const_body with
-  | Undef _ -> None
-  | Def c -> Some c
-  | OpaqueDef lc -> Some (force_lazy_constr lc)
-
-let constant_has_body cb = match cb.const_body with
-  | Undef _ -> false
-  | Def _ | OpaqueDef _ -> true
-
-let is_opaque cb = match cb.const_body with
-  | OpaqueDef _ -> true
-  | Undef _ | Def _ -> false
-
-(* Substitutions of [constant_body] *)
-
-let subst_rel_declaration sub (id,copt,t as x) =
-  let copt' = Option.smartmap (subst_mps sub) copt in
-  let t' = subst_mps sub t in
-  if copt == copt' & t == t' then x else (id,copt',t')
-
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
-
-(* TODO: these substitution functions could avoid duplicating things
-   when the substitution have preserved all the fields *)
-
-let subst_const_type sub arity =
-  if is_empty_subst sub then arity
-  else match arity with
-    | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
-    | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
-
-let subst_const_def sub = function
-  | Undef inl -> Undef inl
-  | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
-
-let subst_const_body sub cb = {
-  const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
-  const_body = subst_const_def sub cb.const_body;
-  const_type = subst_const_type sub cb.const_type;
-  const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
-  const_constraints = cb.const_constraints;
-  const_native_name = ref NotLinked;
-  const_inline_code = cb.const_inline_code }
-
-(* Hash-consing of [constant_body] *)
-
-let hcons_rel_decl ((n,oc,t) as d) =
-  let n' = Name.hcons n
-  and oc' = Option.smartmap hcons_constr oc
-  and t' = hcons_types t
-  in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
-
-let hcons_rel_context l = List.smartmap hcons_rel_decl l
-
-let hcons_polyarity ar =
-  { poly_param_levels =
-      List.smartmap (Option.smartmap hcons_univ) ar.poly_param_levels;
-    poly_level = hcons_univ ar.poly_level }
-
-let hcons_const_type = function
-  | NonPolymorphicType t ->
-    NonPolymorphicType (hcons_constr t)
-  | PolymorphicArity (ctx,s) ->
-    PolymorphicArity (hcons_rel_context ctx, hcons_polyarity s)
-
-let hcons_const_def = function
-  | Undef inl -> Undef inl
-  | Def l_constr ->
-    let constr = force l_constr in
-    Def (from_val (hcons_constr constr))
-  | OpaqueDef lc ->
-    if lazy_constr_is_val lc then
-      let constr = force_opaque lc in
-      OpaqueDef (opaque_from_val (hcons_constr constr))
-    else OpaqueDef lc
-
-let hcons_const_body cb =
-  { cb with
-    const_body = hcons_const_def cb.const_body;
-    const_type = hcons_const_type cb.const_type;
-    const_constraints = hcons_constraints cb.const_constraints }
-
-
-(*s Inductive types (internal representation with redundant
-    information). *)
-
-type recarg =
-  | Norec
-  | Mrec of inductive
-  | Imbr of inductive
-
-let eq_recarg r1 r2 = match r1, r2 with
-| Norec, Norec -> true
-| Mrec i1, Mrec i2 -> eq_ind i1 i2
-| Imbr i1, Imbr i2 -> eq_ind i1 i2
-| _ -> false
-
-let subst_recarg sub r = match r with
-  | Norec -> r
-  | Mrec (kn,i) -> let kn' = subst_ind sub kn in
-      if kn==kn' then r else Mrec (kn',i)
-  | Imbr (kn,i) -> let kn' = subst_ind sub kn in
-      if kn==kn' then r else Imbr (kn',i)
-
-type wf_paths = recarg Rtree.t
-
-let mk_norec = Rtree.mk_node Norec [||]
-
-let mk_paths r recargs =
-  Rtree.mk_node r
-    (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs)
-
-let dest_recarg p = fst (Rtree.dest_node p)
-
-(* dest_subterms returns the sizes of each argument of each constructor of
-   an inductive object of size [p]. This should never be done for Norec,
-   because the number of sons does not correspond to the number of
-   constructors.
- *)
-let dest_subterms p =
-  let (ra,cstrs) = Rtree.dest_node p in
-  assert (match ra with Norec -> false | _ -> true);
-  Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
-
-let recarg_length p j =
-  let (_,cstrs) = Rtree.dest_node p in
-  Array.length (snd (Rtree.dest_node cstrs.(j-1)))
-
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
-
-(**********************************************************************)
-(* Representation of mutual inductive types in the kernel             *)
-(*
-   Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1
-   ...
-   with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
-*)
-
-type monomorphic_inductive_arity = {
-  mind_user_arity : constr;
-  mind_sort : sorts;
-}
-
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
-
-type one_inductive_body = {
-
-(* Primitive datas *)
-
- (* Name of the type: [Ii] *)
-    mind_typename : Id.t;
-
- (* Arity context of [Ii] with parameters: [forall params, Ui] *)
-    mind_arity_ctxt : rel_context;
-
- (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *)
-    mind_arity : inductive_arity;
-
- (* Names of the constructors: [cij] *)
-    mind_consnames : Id.t array;
-
- (* Types of the constructors with parameters: [forall params, Tij],
-    where the Ik are replaced by de Bruijn index in the context
-    I1:forall params, U1 ..  In:forall params, Un *)
-    mind_user_lc : types array;
-
-(* Derived datas *)
-
- (* Number of expected real arguments of the type (no let, no params) *)
-    mind_nrealargs : int;
-
- (* Length of realargs context (with let, no params) *)
-    mind_nrealargs_ctxt : int;
-
- (* List of allowed elimination sorts *)
-    mind_kelim : sorts_family list;
-
- (* Head normalized constructor types so that their conclusion is atomic *)
-    mind_nf_lc : types array;
-
- (* Length of the signature of the constructors (with let, w/o params) *)
-    mind_consnrealdecls : int array;
-
- (* Signature of recursive arguments in the constructors *)
-    mind_recargs : wf_paths;
-
-(* Datas for bytecode compilation *)
-
- (* number of constant constructor *)
-    mind_nb_constant : int;
-
- (* number of no constant constructor *)
-    mind_nb_args : int;
-
-    mind_reloc_tbl :  Cbytecodes.reloc_table;
-  }
-
-type mutual_inductive_body = {
-
-  (* The component of the mutual inductive block *)
-    mind_packets : one_inductive_body array;
-
-  (* Whether the inductive type has been declared as a record *)
-    mind_record : bool;
-
-  (* Whether the type is inductive or coinductive *)
-    mind_finite : bool;
-
-  (* Number of types in the block *)
-    mind_ntypes : int;
-
-  (* Section hypotheses on which the block depends *)
-    mind_hyps : section_context;
-
-  (* Number of expected parameters *)
-    mind_nparams : int;
-
-  (* Number of recursively uniform (i.e. ordinary) parameters *)
-    mind_nparams_rec : int;
-
-  (* The context of parameters (includes let-in declaration) *)
-    mind_params_ctxt : rel_context;
-
-  (* Universes constraints enforced by the inductive declaration *)
-    mind_constraints : constraints;
-
-  (* Data for native compilation *)
-  (* Status of the code (linked or not, and where) *)
-    mind_native_name : native_name ref;
-
-  }
-
-let subst_indarity sub = function
-| Monomorphic s ->
-    Monomorphic {
-      mind_user_arity = subst_mps sub s.mind_user_arity;
-      mind_sort = s.mind_sort;
-    }
-| Polymorphic s as x -> x
-
-let subst_mind_packet sub mbp =
-  { mind_consnames = mbp.mind_consnames;
-    mind_consnrealdecls = mbp.mind_consnrealdecls;
-    mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
-    mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
-    mind_arity = subst_indarity sub mbp.mind_arity;
-    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
-    mind_nrealargs = mbp.mind_nrealargs;
-    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
-    mind_kelim = mbp.mind_kelim;
-    mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
-    mind_nb_constant = mbp.mind_nb_constant;
-    mind_nb_args = mbp.mind_nb_args;
-    mind_reloc_tbl = mbp.mind_reloc_tbl }
-
-let subst_mind sub mib =
-  { mind_record = mib.mind_record ;
-    mind_finite = mib.mind_finite ;
-    mind_ntypes = mib.mind_ntypes ;
-    mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
-    mind_nparams = mib.mind_nparams;
-    mind_nparams_rec = mib.mind_nparams_rec;
-    mind_params_ctxt =
-      map_rel_context (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
-    mind_constraints = mib.mind_constraints;
-    mind_native_name = ref NotLinked }
-
-let hcons_indarity = function
-  | Monomorphic a ->
-    Monomorphic { mind_user_arity = hcons_constr a.mind_user_arity;
-		  mind_sort = hcons_sorts a.mind_sort }
-  | Polymorphic a -> Polymorphic (hcons_polyarity a)
-
-let hcons_mind_packet oib =
- { oib with
-   mind_typename = Id.hcons oib.mind_typename;
-   mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
-   mind_arity = hcons_indarity oib.mind_arity;
-   mind_consnames = Array.smartmap Id.hcons oib.mind_consnames;
-   mind_user_lc = Array.smartmap hcons_types oib.mind_user_lc;
-   mind_nf_lc = Array.smartmap hcons_types oib.mind_nf_lc }
-
-let hcons_mind mib =
-  { mib with
-    mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
-    mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
-    mind_constraints = hcons_constraints mib.mind_constraints }
-
-(*s Modules: signature component specifications, module types, and
-  module declarations *)
-
-type structure_field_body =
-  | SFBconst of constant_body
-  | SFBmind of mutual_inductive_body
-  | SFBmodule of module_body
-  | SFBmodtype of module_type_body
-
-and structure_body = (Label.t * structure_field_body) list
-
-and struct_expr_body =
-  | SEBident of module_path
-  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * constraints
-  | SEBstruct of structure_body
-  | SEBwith of struct_expr_body * with_declaration_body
-
-and with_declaration_body =
-    With_module_body of Id.t list * module_path
-  | With_definition_body of  Id.t list * constant_body
-
-and module_body =
-    { mod_mp : module_path;
-      mod_expr : struct_expr_body option; 
-      mod_type : struct_expr_body;
-      mod_type_alg : struct_expr_body option;
-      mod_constraints : constraints;
-      mod_delta : delta_resolver;
-      mod_retroknowledge : Retroknowledge.action list}
-
-and module_type_body =
-    { typ_mp : module_path;
-      typ_expr : struct_expr_body;
-      typ_expr_alg : struct_expr_body option ;
-      typ_constraints : constraints;
-      typ_delta :delta_resolver}
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 5b5e1750c..3a05f9309 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -7,11 +7,7 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Term
-open Cemitcodes
-open Sign
-open Mod_subst
 
 (** This module defines the internal representation of global
    declarations. This includes global constants/axioms, mutual
@@ -22,33 +18,14 @@ type engagement = ImpredicativeSet
 (** {6 Representation of constants (Definition/Axiom) } *)
 
 type polymorphic_arity = {
-  poly_param_levels : universe option list;
-  poly_level : universe;
+  poly_param_levels : Univ.universe option list;
+  poly_level : Univ.universe;
 }
 
 type constant_type =
   | NonPolymorphicType of types
   | PolymorphicArity of rel_context * polymorphic_arity
 
-type constr_substituted
-
-val from_val : constr -> constr_substituted
-val force : constr_substituted -> constr
-
-(** Opaque proof terms are not loaded immediately, but are there
-    in a lazy form. Forcing this lazy may trigger some unmarshal of
-    the necessary structure. *)
-
-type lazy_constr
-
-val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
-val force_lazy_constr : lazy_constr -> constr_substituted
-val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr
-val lazy_constr_is_val : lazy_constr -> bool
-
-val force_opaque : lazy_constr -> constr
-val opaque_from_val : constr -> lazy_constr
-
 (** Inlining level of parameters at functor applications.
     None means no inlining *)
 
@@ -59,8 +36,8 @@ type inline = int option
 
 type constant_def =
   | Undef of inline
-  | Def of constr_substituted
-  | OpaqueDef of lazy_constr
+  | Def of Lazyconstr.constr_substituted
+  | OpaqueDef of Lazyconstr.lazy_constr
 
 type native_name =
   | Linked of string
@@ -69,27 +46,14 @@ type native_name =
   | NotLinked
 
 type constant_body = {
-    const_hyps : section_context; (** New: younger hyp at top *)
+    const_hyps : Sign.section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
-    const_body_code : to_patch_substituted;
-    const_constraints : constraints;
+    const_body_code : Cemitcodes.to_patch_substituted;
+    const_constraints : Univ.constraints;
     const_native_name : native_name ref;
     const_inline_code : bool }
 
-val subst_const_def : substitution -> constant_def -> constant_def
-val subst_const_body : substitution -> constant_body -> constant_body
-
-(** Is there a actual body in const_body or const_body_opaque ? *)
-
-val constant_has_body : constant_body -> bool
-
-(** Accessing const_body_opaque or const_body *)
-
-val body_of_constant : constant_body -> constr_substituted option
-
-val is_opaque : constant_body -> bool
-
 (** {6 Representation of mutual inductive types in the kernel } *)
 
 type recarg =
@@ -97,20 +61,8 @@ type recarg =
   | Mrec of inductive
   | Imbr of inductive
 
-val eq_recarg : recarg -> recarg -> bool
-
-val subst_recarg : substitution -> recarg -> recarg
-
 type wf_paths = recarg Rtree.t
 
-val mk_norec : wf_paths
-val mk_paths : recarg -> wf_paths list array -> wf_paths
-val dest_recarg : wf_paths -> recarg
-val dest_subterms : wf_paths -> wf_paths list array
-val recarg_length : wf_paths -> int -> int
-
-val subst_wf_paths : substitution -> wf_paths -> wf_paths
-
 (**
 {v
    Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1
@@ -179,7 +131,7 @@ type mutual_inductive_body = {
 
     mind_ntypes : int;  (** Number of types in the block *)
 
-    mind_hyps : section_context;  (** Section hypotheses on which the block depends *)
+    mind_hyps : Sign.section_context;  (** Section hypotheses on which the block depends *)
 
     mind_nparams : int;  (** Number of expected parameters *)
 
@@ -187,7 +139,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_constraints : constraints;  (** Universes constraints enforced by the inductive declaration *)
+    mind_constraints : Univ.constraints;  (** Universes constraints enforced by the inductive declaration *)
 
 (** {8 Data for native compilation } *)
 
@@ -196,8 +148,6 @@ type mutual_inductive_body = {
 
   }
 
-val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
-
 (** {6 Modules: signature component specifications, module types, and
   module declarations } *)
 
@@ -216,7 +166,7 @@ and structure_body = (Label.t * structure_field_body) list
 and struct_expr_body =
   | SEBident of module_path
   | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * constraints
+  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
   | SEBstruct of structure_body
   | SEBwith of struct_expr_body * with_declaration_body
 
@@ -228,36 +178,26 @@ and module_body =
     {  (** absolute path of the module *)
       mod_mp : module_path;
       (** Implementation *)
-      mod_expr : struct_expr_body option; 
+      mod_expr : struct_expr_body option;
       (** Signature *)
       mod_type : struct_expr_body;
-      (** algebraic structure expression is kept 
+      (** algebraic structure expression is kept
 	 if it's relevant for extraction  *)
-      mod_type_alg : struct_expr_body option; 
+      mod_type_alg : struct_expr_body option;
       (** set of all constraint in the module  *)
-      mod_constraints : constraints;
+      mod_constraints : Univ.constraints;
       (** quotiented set of equivalent constant and inductive name  *)
-      mod_delta : delta_resolver;
+      mod_delta : Mod_subst.delta_resolver;
       mod_retroknowledge : Retroknowledge.action list}
-      
+
 and module_type_body =
-    { 
+    {
       (** Path of the module type *)
       typ_mp : module_path;
       typ_expr : struct_expr_body;
-      (** algebraic structure expression is kept 
+      (** algebraic structure expression is kept
 	 if it's relevant for extraction  *)
       typ_expr_alg : struct_expr_body option ;
-      typ_constraints : constraints;
+      typ_constraints : Univ.constraints;
       (** quotiented set of equivalent constant and inductive name  *)
-      typ_delta :delta_resolver}
-
-
-(** Hash-consing *)
-
-(** Here, strictly speaking, we don't perform true hash-consing
-    of the structure, but simply hash-cons all inner constr
-    and other known elements *)
-
-val hcons_const_body : constant_body -> constant_body
-val hcons_mind : mutual_inductive_body -> mutual_inductive_body
+      typ_delta : Mod_subst.delta_resolver}
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
new file mode 100644
index 000000000..90327da6c
--- /dev/null
+++ b/kernel/declareops.ml
@@ -0,0 +1,201 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Declarations
+open Mod_subst
+open Lazyconstr
+open Util
+
+(** Operations concernings types in [Declarations] :
+    [constant_body], [mutual_inductive_body], [module_body] ... *)
+
+(** Constants *)
+
+let body_of_constant cb = match cb.const_body with
+  | Undef _ -> None
+  | Def c -> Some c
+  | OpaqueDef lc -> Some (force_lazy_constr lc)
+
+let constant_has_body cb = match cb.const_body with
+  | Undef _ -> false
+  | Def _ | OpaqueDef _ -> true
+
+let is_opaque cb = match cb.const_body with
+  | OpaqueDef _ -> true
+  | Undef _ | Def _ -> false
+
+(** Constant substitutions *)
+
+let subst_rel_declaration sub (id,copt,t as x) =
+  let copt' = Option.smartmap (subst_mps sub) copt in
+  let t' = subst_mps sub t in
+  if copt == copt' & t == t' then x else (id,copt',t')
+
+let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
+
+(* TODO: these substitution functions could avoid duplicating things
+   when the substitution have preserved all the fields *)
+
+let subst_const_type sub arity =
+  if is_empty_subst sub then arity
+  else match arity with
+    | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
+    | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+
+let subst_const_def sub = function
+  | Undef inl -> Undef inl
+  | Def c -> Def (subst_constr_subst sub c)
+  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+
+let subst_const_body sub cb = {
+  const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
+  const_body = subst_const_def sub cb.const_body;
+  const_type = subst_const_type sub cb.const_type;
+  const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+  const_constraints = cb.const_constraints;
+  const_native_name = ref NotLinked;
+  const_inline_code = cb.const_inline_code }
+
+(** Hash-consing of constants *)
+
+let hcons_rel_decl ((n,oc,t) as d) =
+  let n' = Names.Name.hcons n
+  and oc' = Option.smartmap Term.hcons_constr oc
+  and t' = Term.hcons_types t
+  in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
+
+let hcons_rel_context l = List.smartmap hcons_rel_decl l
+
+let hcons_polyarity ar =
+  { poly_param_levels =
+      List.smartmap (Option.smartmap Univ.hcons_univ) ar.poly_param_levels;
+    poly_level = Univ.hcons_univ ar.poly_level }
+
+let hcons_const_type = function
+  | NonPolymorphicType t ->
+    NonPolymorphicType (Term.hcons_constr t)
+  | PolymorphicArity (ctx,s) ->
+    PolymorphicArity (hcons_rel_context ctx, hcons_polyarity s)
+
+let hcons_const_def = function
+  | Undef inl -> Undef inl
+  | Def l_constr ->
+    let constr = force l_constr in
+    Def (from_val (Term.hcons_constr constr))
+  | OpaqueDef lc ->
+    if lazy_constr_is_val lc then
+      let constr = force_opaque lc in
+      OpaqueDef (opaque_from_val (Term.hcons_constr constr))
+    else OpaqueDef lc
+
+let hcons_const_body cb =
+  { cb with
+    const_body = hcons_const_def cb.const_body;
+    const_type = hcons_const_type cb.const_type;
+    const_constraints = Univ.hcons_constraints cb.const_constraints }
+
+(** Inductive types *)
+
+let eq_recarg r1 r2 = match r1, r2 with
+| Norec, Norec -> true
+| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
+| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
+| _ -> false
+
+let subst_recarg sub r = match r with
+  | Norec -> r
+  | Mrec (kn,i) -> let kn' = subst_ind sub kn in
+      if kn==kn' then r else Mrec (kn',i)
+  | Imbr (kn,i) -> let kn' = subst_ind sub kn in
+      if kn==kn' then r else Imbr (kn',i)
+
+let mk_norec = Rtree.mk_node Norec [||]
+
+let mk_paths r recargs =
+  Rtree.mk_node r
+    (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs)
+
+let dest_recarg p = fst (Rtree.dest_node p)
+
+(* dest_subterms returns the sizes of each argument of each constructor of
+   an inductive object of size [p]. This should never be done for Norec,
+   because the number of sons does not correspond to the number of
+   constructors.
+ *)
+let dest_subterms p =
+  let (ra,cstrs) = Rtree.dest_node p in
+  assert (match ra with Norec -> false | _ -> true);
+  Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
+
+let recarg_length p j =
+  let (_,cstrs) = Rtree.dest_node p in
+  Array.length (snd (Rtree.dest_node cstrs.(j-1)))
+
+let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+
+(** Substitution of inductive declarations *)
+
+let subst_indarity sub = function
+| Monomorphic s ->
+    Monomorphic {
+      mind_user_arity = subst_mps sub s.mind_user_arity;
+      mind_sort = s.mind_sort;
+    }
+| Polymorphic s as x -> x
+
+let subst_mind_packet sub mbp =
+  { mind_consnames = mbp.mind_consnames;
+    mind_consnrealdecls = mbp.mind_consnrealdecls;
+    mind_typename = mbp.mind_typename;
+    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
+    mind_arity = subst_indarity sub mbp.mind_arity;
+    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
+    mind_nrealargs = mbp.mind_nrealargs;
+    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
+    mind_kelim = mbp.mind_kelim;
+    mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
+    mind_nb_constant = mbp.mind_nb_constant;
+    mind_nb_args = mbp.mind_nb_args;
+    mind_reloc_tbl = mbp.mind_reloc_tbl }
+
+let subst_mind sub mib =
+  { mind_record = mib.mind_record ;
+    mind_finite = mib.mind_finite ;
+    mind_ntypes = mib.mind_ntypes ;
+    mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
+    mind_nparams = mib.mind_nparams;
+    mind_nparams_rec = mib.mind_nparams_rec;
+    mind_params_ctxt =
+      Sign.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
+    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
+    mind_constraints = mib.mind_constraints;
+    mind_native_name = ref NotLinked }
+
+(** Hash-consing of inductive declarations *)
+
+let hcons_indarity = function
+  | Monomorphic a ->
+    Monomorphic { mind_user_arity = Term.hcons_constr a.mind_user_arity;
+		  mind_sort = Term.hcons_sorts a.mind_sort }
+  | Polymorphic a -> Polymorphic (hcons_polyarity a)
+
+let hcons_mind_packet oib =
+ { oib with
+   mind_typename = Names.Id.hcons oib.mind_typename;
+   mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
+   mind_arity = hcons_indarity oib.mind_arity;
+   mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
+   mind_user_lc = Array.smartmap Term.hcons_types oib.mind_user_lc;
+   mind_nf_lc = Array.smartmap Term.hcons_types oib.mind_nf_lc }
+
+let hcons_mind mib =
+  { mib with
+    mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
+    mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
+    mind_constraints = Univ.hcons_constraints mib.mind_constraints }
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
new file mode 100644
index 000000000..1616e4639
--- /dev/null
+++ b/kernel/declareops.mli
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Declarations
+open Mod_subst
+open Lazyconstr
+
+(** Operations concerning types in [Declarations] :
+    [constant_body], [mutual_inductive_body], [module_body] ... *)
+
+(** {6 Constants} *)
+
+val subst_const_def : substitution -> constant_def -> constant_def
+val subst_const_body : substitution -> constant_body -> constant_body
+
+(** Is there a actual body in const_body or const_body_opaque ? *)
+
+val constant_has_body : constant_body -> bool
+
+(** Accessing const_body_opaque or const_body *)
+
+val body_of_constant : constant_body -> constr_substituted option
+
+val is_opaque : constant_body -> bool
+
+
+(** {6 Inductive types} *)
+
+val eq_recarg : recarg -> recarg -> bool
+
+val subst_recarg : substitution -> recarg -> recarg
+
+val mk_norec : wf_paths
+val mk_paths : recarg -> wf_paths list array -> wf_paths
+val dest_recarg : wf_paths -> recarg
+val dest_subterms : wf_paths -> wf_paths list array
+val recarg_length : wf_paths -> int -> int
+
+val subst_wf_paths : substitution -> wf_paths -> wf_paths
+
+val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
+
+
+(** {6 Hash-consing} *)
+
+(** Here, strictly speaking, we don't perform true hash-consing
+    of the structure, but simply hash-cons all inner constr
+    and other known elements *)
+
+val hcons_const_body : constant_body -> constant_body
+val hcons_mind : mutual_inductive_body -> mutual_inductive_body
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 20742d341..650c3566d 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -7,9 +7,7 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Term
-open Sign
 
 (** This module defines the entry types for global declarations. This
    information is entered in the environments. This includes global
@@ -52,14 +50,14 @@ type mutual_inductive_entry = {
 
 type definition_entry = {
   const_entry_body   : constr;
-  const_entry_secctx : section_context option;
+  const_entry_secctx : Sign.section_context option;
   const_entry_type        : types option;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
 type inline = int option (* inlining level, None for no inlining *)
 
-type parameter_entry = section_context option * types * inline 
+type parameter_entry = Sign.section_context option * types * inline
 
 type constant_entry =
   | DefinitionEntry of definition_entry
@@ -80,5 +78,3 @@ and with_declaration =
 and module_entry =
     { mod_entry_type : module_struct_entry option;
       mod_entry_expr : module_struct_entry option}
-
-
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a36e2dcf6..0063aa6f2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -174,7 +174,7 @@ exception NotEvaluableConst of const_evaluation_result
 let constant_value env kn =
   let cb = lookup_constant kn env in
   match cb.const_body with
-    | Def l_body -> Declarations.force l_body
+    | Def l_body -> Lazyconstr.force l_body
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d80c69bee..e6faaaa85 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -12,6 +12,7 @@ open Names
 open Univ
 open Term
 open Declarations
+open Declareops
 open Inductive
 open Environ
 open Reduction
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 31d9f48ac..3132b7e79 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -12,6 +12,7 @@ open Names
 open Univ
 open Term
 open Declarations
+open Declareops
 open Environ
 open Reduction
 open Type_errors
@@ -414,8 +415,10 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
+let eq_wf_paths = Rtree.eq_rtree Declareops.eq_recarg
+
 let spec_of_tree t = lazy
-  (if Rtree.eq_rtree eq_recarg (Lazy.force t) mk_norec
+  (if eq_wf_paths (Lazy.force t) mk_norec
    then Not_subterm
    else Subterm(Strict,Lazy.force t))
 
@@ -427,7 +430,7 @@ let subterm_spec_glb =
       | Not_subterm, _ -> Not_subterm
       | _, Not_subterm -> Not_subterm
       | Subterm (a1,t1), Subterm (a2,t2) ->
-          if Rtree.eq_rtree eq_recarg t1 t2 then Subterm (size_glb a1 a2, t1)
+          if eq_wf_paths t1 t2 then Subterm (size_glb a1 a2, t1)
           (* branches do not return objects with same spec *)
           else Not_subterm in
   Array.fold_left glb2 Dead_code
@@ -877,7 +880,7 @@ let check_one_cofix env nbfix def deftype =
             let realargs = List.skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
               | (t::lr), (rar::lrar) ->
-                  if Rtree.eq_rtree eq_recarg rar mk_norec then
+                  if eq_wf_paths rar mk_norec then
                     if noccur_with_meta n nbfix t
                     then process_args_of_constr (lr, lrar)
                     else raise (CoFixGuardError
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 07f24583e..ef3ef6d94 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -8,7 +8,8 @@ Cbytecodes
 Copcodes
 Cemitcodes
 Nativevalues
-Declarations
+Lazyconstr
+Declareops
 Retroknowledge
 Pre_env
 Cbytegen
diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
new file mode 100644
index 000000000..31cb76575
--- /dev/null
+++ b/kernel/lazyconstr.ml
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Mod_subst
+
+(** [constr_substituted] are [constr] with possibly pending
+    substitutions of kernel names. *)
+
+type constr_substituted = constr substituted
+
+let from_val = from_val
+
+let force = force subst_mps
+
+let subst_constr_subst = subst_substituted
+
+(** Opaque proof terms are not loaded immediately, but are there
+    in a lazy form. Forcing this lazy may trigger some unmarshal of
+    the necessary structure. The ['a substituted] type isn't really great
+    here, so we store "manually" a substitution list, the younger one at top.
+*)
+
+type lazy_constr = constr_substituted Lazy.t * substitution list
+
+let force_lazy_constr (c,l) =
+  List.fold_right subst_constr_subst l (Lazy.force c)
+
+let lazy_constr_is_val (c,_) = Lazy.lazy_is_val c
+
+let make_lazy_constr c = (c, [])
+
+let force_opaque lc = force (force_lazy_constr lc)
+
+let opaque_from_val c = (Lazy.lazy_from_val (from_val c), [])
+
+let subst_lazy_constr sub (c,l) = (c,sub::l)
+
diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli
new file mode 100644
index 000000000..17c9bcc76
--- /dev/null
+++ b/kernel/lazyconstr.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Mod_subst
+
+(** [constr_substituted] are [constr] with possibly pending
+    substitutions of kernel names. *)
+
+type constr_substituted
+
+val from_val : constr -> constr_substituted
+val force : constr_substituted -> constr
+val subst_constr_subst :
+  substitution -> constr_substituted -> constr_substituted
+
+(** Opaque proof terms are not loaded immediately, but are there
+    in a lazy form. Forcing this lazy may trigger some unmarshal of
+    the necessary structure. *)
+
+type lazy_constr
+
+val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
+val force_lazy_constr : lazy_constr -> constr_substituted
+val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr
+val lazy_constr_is_val : lazy_constr -> bool
+
+val force_opaque : lazy_constr -> constr
+val opaque_from_val : constr -> lazy_constr
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b566dd8af..b24deb0dc 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -105,12 +105,12 @@ and check_with_def env sign (idl,c) mp equiv =
 			(union_constraints cb.const_constraints cst1)
 			cst2
 		    in
-		    let def = Def (Declarations.from_val j.uj_val) in
+		    let def = Def (Lazyconstr.from_val j.uj_val) in
 		    def,cst
 		| Def cs ->
-		    let cst1 = Reduction.conv env' c (Declarations.force cs) in
+		    let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
 		    let cst = union_constraints cb.const_constraints cst1 in
-		    let def = Def (Declarations.from_val c) in
+		    let def = Def (Lazyconstr.from_val c) in
 		    def,cst
 	      in
 	      let cb' =
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 986118655..c1b5d788d 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -20,6 +20,7 @@ open Util
 open Names
 open Term
 open Declarations
+open Declareops
 open Environ
 open Entries
 open Mod_subst
@@ -287,7 +288,7 @@ let strengthen_const mp_from l cb resolver =
       let kn = KerName.make2 mp_from l in
       let con = constant_of_delta_kn resolver kn in
       { cb with
-	const_body = Def (Declarations.from_val (mkConst con));
+	const_body = Def (Lazyconstr.from_val (mkConst con));
 	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con)
       }
 
@@ -377,7 +378,7 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	  match constant.const_body with
 	    | Undef _ | OpaqueDef _ -> l
 	    | Def body ->
-	      let constr = Declarations.force body in
+	      let constr = Lazyconstr.force body in
 	      add_inline_delta_resolver kn (lev, Some constr) l
 	with Not_found ->
 	  error_no_such_label_sub (con_label con)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 7b878c53e..932b490e3 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1319,7 +1319,7 @@ and compile_named env auxdefs id =
 let compile_constant env prefix con body =
   match body with
   | Def t ->
-      let t = Declarations.force t in
+      let t = Lazyconstr.force t in
       let code = lambda_of_constr env t in
       let code, name =
         if is_lazy t then mk_lazy code, LinkedLazy prefix
@@ -1414,7 +1414,7 @@ let rec compile_deps env prefix ~interactive init t =
       then init
       else
       let comp_stack, (mind_updates, const_updates) = match cb.const_body with
-        | Def t -> compile_deps env prefix ~interactive init (Declarations.force t)
+        | Def t -> compile_deps env prefix ~interactive init (Lazyconstr.force t)
         | _ -> init
       in
       let code, name = compile_constant env prefix c cb.const_body in
@@ -1429,7 +1429,7 @@ let compile_constant_field env prefix con (code, symb, (mupds, cupds)) cb =
   let acc = (code, (mupds, cupds)) in
   match cb.const_body with
   | Def t ->
-    let t = Declarations.force t in
+    let t = Lazyconstr.force t in
     let (code, (mupds, cupds)) = compile_deps env prefix ~interactive:false acc t in
     let (gl, name) = compile_constant env prefix con cb.const_body in
     let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index f530f6e2e..9c400e4c0 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -631,11 +631,13 @@ and lambda_of_app env f args =
       let cb = lookup_constant kn !global_env in
       begin match cb.const_body with
       | Def csubst ->
-          if cb.const_inline_code then lambda_of_app env (force csubst) args
+          if cb.const_inline_code then
+            lambda_of_app env (Lazyconstr.force csubst) args
           else
           let prefix = get_const_prefix !global_env kn in
           let t =
-            if is_lazy (force csubst) then mkLapp Lforce [|Lconst (prefix, kn)|]
+            if is_lazy (Lazyconstr.force csubst) then
+              mkLapp Lforce [|Lconst (prefix, kn)|]
             else Lconst (prefix, kn)
           in
         mkLapp t (lambda_of_args env 0 args)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8a9822b18..932e43163 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -271,7 +271,7 @@ let add_constant dir l decl senv =
     | ConstantEntry ce -> translate_constant senv.env kn ce
     | GlobalRecipe r ->
       let cb = translate_recipe senv.env kn r in
-      if DirPath.is_empty dir then hcons_const_body cb else cb
+      if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
@@ -296,7 +296,8 @@ let add_mind dir l mie senv =
 	     type do not match");
   let kn = make_mind senv.modinfo.modpath dir l in
   let mib = translate_mind senv.env kn mie in
-  let mib = match mib.mind_hyps with [] -> hcons_mind mib | _ -> mib in
+  let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
+  in
   let senv' = add_field (l,SFBmind mib) (I kn) senv in
   kn, senv'
 
@@ -780,9 +781,9 @@ end = struct
      [lightened_compiled_library] is abstract and only meant for writing
      to .vo via Marshal (which doesn't care about types).
   *)
-  type table = constr_substituted array
-  let key_as_lazy_constr (i:int) = (Obj.magic i : lazy_constr)
-  let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int)
+  type table = Lazyconstr.constr_substituted array
+  let key_as_lazy_constr (i:int) = (Obj.magic i : Lazyconstr.lazy_constr)
+  let key_of_lazy_constr (c:Lazyconstr.lazy_constr) = (Obj.magic c : int)
 
   (* To avoid any future misuse of the lightened library that could 
      interpret encoded keys as real [constr_substituted], we hide 
@@ -812,7 +813,7 @@ end = struct
 	    }    
     and traverse_struct struc =
       let traverse_body (l,body) = (l,match body with
-	| SFBconst cb when is_opaque cb ->
+	| SFBconst cb when Declareops.is_opaque cb ->
 	  SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
 	| (SFBconst _ | SFBmind _ ) as x ->
 	  x
@@ -855,7 +856,7 @@ end = struct
       ((* Insert inside the table. *) 
 	(fun def ->
 	  let opaque_definition = match def with
-	    | OpaqueDef lc -> force_lazy_constr lc
+	    | OpaqueDef lc -> Lazyconstr.force_lazy_constr lc
 	    | _ -> assert false
 	  in
 	  incr counter;
@@ -886,10 +887,10 @@ end = struct
 	  match load_proof with
 	    | Flags.Force ->
 	      let lc = Lazy.lazy_from_val (access k) in
-	      OpaqueDef (make_lazy_constr lc)
+	      OpaqueDef (Lazyconstr.make_lazy_constr lc)
 	    | Flags.Lazy ->
 	      let lc = lazy (access k) in
-	      OpaqueDef (make_lazy_constr lc)
+	      OpaqueDef (Lazyconstr.make_lazy_constr lc)
 	    | Flags.Dont ->
 	      Undef None
     in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8f46831b8..e5b81c72f 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -94,10 +94,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   let check_conv why cst f = check_conv_error error why cst f in
   let mib1 =
     match info1 with
-      | IndType ((_,0), mib) -> subst_mind subst1 mib
+      | IndType ((_,0), mib) -> Declareops.subst_mind subst1 mib
       | _ -> error (InductiveFieldExpected mib2)
   in
-  let mib2 =  subst_mind subst2 mib2 in
+  let mib2 =  Declareops.subst_mind subst2 mib2 in
   let check_inductive_type cst name env t1 t2 =
 
     (* Due to sort-polymorphism in inductive types, the conclusions of
@@ -270,8 +270,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
   match info1 with
     | Constant cb1 ->
       let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
-      let cb1 = subst_const_body subst1 cb1 in
-      let cb2 = subst_const_body subst2 cb2 in
+      let cb1 = Declareops.subst_const_body subst1 cb1 in
+      let cb2 = Declareops.subst_const_body subst2 cb2 in
       (* Start by checking types*)
       let typ1 = Typeops.type_of_constant_type env cb1.const_type in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
@@ -290,8 +290,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	    | Def lc1 ->
 	      (* NB: cb1 might have been strengthened and appear as transparent.
 		 Anyway [check_conv] will handle that afterwards. *)
-	      let c1 = Declarations.force lc1 in
-	      let c2 = Declarations.force lc2 in
+	      let c1 = Lazyconstr.force lc1 in
+	      let c2 = Lazyconstr.force lc2 in
 	      check_conv NotConvertibleBodyField cst conv env c1 c2))
    | IndType ((kn,i),mind1) ->
        ignore (Errors.error (
@@ -300,7 +300,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "inductive type and give a definition to map the old name to the new " ^
        "name."));
       let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
-      if constant_has_body cb2 then error DefinitionFieldExpected;
+      if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let error = NotConvertibleTypeField (arity1, typ2) in
@@ -312,7 +312,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name."));
       let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
-      if constant_has_body cb2 then error DefinitionFieldExpected;
+      if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
       let error = NotConvertibleTypeField (ty1, ty2) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 1cd006f25..3ec0da457 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -96,8 +96,8 @@ let infer_declaration env dcl =
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
       let def =
 	if c.const_entry_opaque
-	then OpaqueDef (Declarations.opaque_from_val j.uj_val)
-	else Def (Declarations.from_val j.uj_val)
+	then OpaqueDef (Lazyconstr.opaque_from_val j.uj_val)
+	else Def (Lazyconstr.from_val j.uj_val)
       in
       def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
   | ParameterEntry (ctx,t,nl) ->
@@ -119,9 +119,9 @@ let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) =
       let ids_typ = global_vars_set_constant_type env typ in
       let ids_def = match def with
       | Undef _ -> Id.Set.empty
-      | Def cs -> global_vars_set env (Declarations.force cs)
+      | Def cs -> global_vars_set env (Lazyconstr.force cs)
       | OpaqueDef lc -> 
-          global_vars_set env (Declarations.force_opaque lc) in
+          global_vars_set env (Lazyconstr.force_opaque lc) in
       keep_hyps env (Id.Set.union ids_typ ids_def) in
     let declared = match ctx with
       | None -> inferred