Modules dans COQ\!\!\!\!

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

35 files changed, 2203 insertions, 408 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index ace0ed39d..463f6f21d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -55,10 +55,10 @@ type evaluable_global_reference =
   | EvalVarRef of identifier
   | EvalConstRef of constant
 
-type transparent_state = Idpred.t * Sppred.t
+type transparent_state = Idpred.t * KNpred.t
 
-let all_opaque = (Idpred.empty, Sppred.empty)
-let all_transparent = (Idpred.full, Sppred.full)
+let all_opaque = (Idpred.empty, KNpred.empty)
+let all_transparent = (Idpred.full, KNpred.full)
 
 module type RedFlagsSig = sig
   type reds
@@ -98,7 +98,7 @@ module RedFlags = (struct
   let fDELTA = DELTA
   let fIOTA = IOTA
   let fZETA = ZETA
-  let fCONST sp  = CONST sp
+  let fCONST kn  = CONST kn
   let fVAR id  = VAR id
   let no_red = {
     r_beta = false;
@@ -111,9 +111,9 @@ module RedFlags = (struct
   let red_add red = function
     | BETA -> { red with r_beta = true }
     | DELTA -> { red with r_delta = true; r_const = all_transparent }
-    | CONST sp ->
+    | CONST kn ->
 	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Sppred.add sp l2 }
+	{ red with r_const = l1, KNpred.add kn l2 }
     | IOTA -> { red with r_iota = true }
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
@@ -123,9 +123,9 @@ module RedFlags = (struct
   let red_sub red = function
     | BETA -> { red with r_beta = false }
     | DELTA -> { red with r_delta = false }
-    | CONST sp ->
+    | CONST kn ->
  	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Sppred.remove sp l2 }
+	{ red with r_const = l1, KNpred.remove kn l2 }
     | IOTA -> { red with r_iota = false }
     | ZETA -> { red with r_zeta = false }
     | VAR id ->
@@ -139,11 +139,11 @@ module RedFlags = (struct
 
   let red_set red = function
     | BETA -> incr_cnt red.r_beta beta
-    | CONST sp -> 
+    | CONST kn -> 
 	let (_,l) = red.r_const in
-	let c = Sppred.mem sp l in
+	let c = KNpred.mem kn l in
 	incr_cnt c delta
-    | VAR id -> (* En attendant d'avoir des sp pour les Var *)
+    | VAR id -> (* En attendant d'avoir des kn pour les Var *)
 	let (l,_) = red.r_const in
 	let c = Idpred.mem id l in
 	incr_cnt c delta
@@ -155,7 +155,7 @@ module RedFlags = (struct
   let red_get_const red =
     let p1,p2 = red.r_const in
     let (b1,l1) = Idpred.elements p1 in
-    let (b2,l2) = Sppred.elements p2 in
+    let (b2,l2) = KNpred.elements p2 in
     if b1=b2 then
       let l1' = List.map (fun x -> EvalVarRef x) l1 in
       let l2' = List.map (fun x -> EvalConstRef x) l2 in
@@ -171,10 +171,10 @@ let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
 let betaiota = mkflags [fBETA;fIOTA]
 let beta = mkflags [fBETA]
 let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
-let unfold_red sp = 
-  let flag = match sp with
+let unfold_red kn = 
+  let flag = match kn with
     | EvalVarRef id -> fVAR id
-    | EvalConstRef sp -> fCONST sp
+    | EvalConstRef kn -> fCONST kn
   in (* Remove fZETA for finer behaviour ? *)
   mkflags [fBETA;flag;fIOTA;fZETA]
 
@@ -223,10 +223,10 @@ let betaiotazeta_red = {
   r_evar = false;
   r_iota = true }
 
-let unfold_red sp =
-  let c = match sp with
+let unfold_red kn =
+  let c = match kn with
     | EvalVarRef id -> false,[],[id]
-    | EvalConstRef sp -> false,[sp],[]
+    | EvalConstRef kn -> false,[kn],[]
   in {
   r_beta = true;
   r_const = c;
@@ -236,7 +236,7 @@ let unfold_red sp =
 
 (* Sets of reduction kinds.
    Main rule: delta implies all consts (both global (= by
-   section_path) and local (= by Rel or Var)), all evars, and zeta (= letin's).
+   kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's).
    Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
    a LetIn expression is Letin reduction *)
 
@@ -284,11 +284,11 @@ let red_local_const = red_delta_set
 (* to know if a redex is allowed, only a subset of red_kind is used ... *)
 let red_set red = function
   | BETA -> incr_cnt red.r_beta beta
-  | CONST [sp] -> 
+  | CONST [kn] -> 
       let (b,l,_) = red.r_const in
-      let c = List.mem sp l in
+      let c = List.mem kn l in
       incr_cnt ((b & not c) or (c & not b)) delta
-  | VAR id -> (* En attendant d'avoir des sp pour les Var *)
+  | VAR id -> (* En attendant d'avoir des kn pour les Var *)
      let (b,_,l) = red.r_const in
       let c = List.mem id l in
       incr_cnt ((b & not c) or (c & not b)) delta
@@ -584,8 +584,8 @@ let rec mk_clos e t =
     | Rel i -> clos_rel e i
     | Var x -> { norm = Red; term = FFlex (VarKey x) }
     | Meta _ | Sort _ ->  { norm = Norm; term = FAtom t }
-    | Ind sp -> { norm = Norm; term = FInd sp }
-    | Construct sp -> { norm = Cstr; term = FConstruct sp }
+    | Ind kn -> { norm = Norm; term = FInd kn }
+    | Construct kn -> { norm = Cstr; term = FConstruct kn }
     | Evar (ev,args) ->
         { norm = Cstr; term = FEvar (ev,Array.map (mk_clos e) args) }
     | (Fix _|CoFix _|Lambda _|Prod _) ->
@@ -609,9 +609,9 @@ let mk_clos_deep clos_fun env t =
     | App (f,v) ->
         { norm = Red;
 	  term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
-    | Const sp ->
+    | Const kn ->
         { norm = Red;
-	  term = FFlex (ConstKey sp) }
+	  term = FFlex (ConstKey kn) }
     | Case (ci,p,c,v) ->
         { norm = Red;
 	  term = FCases (ci, clos_fun env p, clos_fun env c,
@@ -903,8 +903,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(ConstKey sp) when red_set info.i_flags (fCONST sp) ->
-      (match ref_value_cache info (ConstKey sp) with
+  | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) ->
+      (match ref_value_cache info (ConstKey kn) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
   | FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 1360862c9..826d58fba 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -24,14 +24,14 @@ val with_stats: 'a Lazy.t -> 'a
 
 type evaluable_global_reference =
   | EvalVarRef of identifier
-  | EvalConstRef of section_path
+  | EvalConstRef of kernel_name
 
 (*s Delta implies all consts (both global (= by
-  [section_path]) and local (= by [Rel] or [Var])), all evars, and letin's.
+  [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
   a LetIn expression is Letin reduction *)
 
-type transparent_state = Idpred.t * Sppred.t
+type transparent_state = Idpred.t * KNpred.t
 
 val all_opaque      : transparent_state
 val all_transparent : transparent_state
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 350e1a5a0..ffa7735e7 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -12,36 +12,36 @@ open Names
 open Closure
 
 (* Opaque constants *)
-let cst_transp = ref Sppred.full
+let cst_transp = ref KNpred.full
 
-let set_opaque_const sp = cst_transp := Sppred.remove sp !cst_transp
-let set_transparent_const sp = cst_transp := Sppred.add sp !cst_transp
+let set_opaque_const kn = cst_transp := KNpred.remove kn !cst_transp
+let set_transparent_const kn = cst_transp := KNpred.add kn !cst_transp
 
-let is_opaque_cst sp = not (Sppred.mem sp !cst_transp)
+let is_opaque_cst kn = not (KNpred.mem kn !cst_transp)
 
 (* Unfold the first only if it is not opaque and the second is
    opaque *)
-let const_order sp1 sp2 = is_opaque_cst sp2 & not (is_opaque_cst sp1)
+let const_order kn1 kn2 = is_opaque_cst kn2 & not (is_opaque_cst kn1)
 
 (* Opaque variables *)
 let var_transp = ref Idpred.full
 
-let set_opaque_var sp = var_transp := Idpred.remove sp !var_transp
-let set_transparent_var sp = var_transp := Idpred.add sp !var_transp
+let set_opaque_var kn = var_transp := Idpred.remove kn !var_transp
+let set_transparent_var kn = var_transp := Idpred.add kn !var_transp
 
-let is_opaque_var sp = not (Idpred.mem sp !var_transp)
+let is_opaque_var kn = not (Idpred.mem kn !var_transp)
 
 let var_order id1 id2 = is_opaque_var id2 & not (is_opaque_var id1)
 
 (* *)
 let oracle_order k1 k2 =
   match (k1,k2) with
-      (ConstKey sp1, ConstKey sp2) -> const_order sp1 sp2
+      (ConstKey kn1, ConstKey kn2) -> const_order kn1 kn2
     | (VarKey id1, VarKey id2) -> var_order id1 id2
     | _ -> false
 
 (* summary operations *)
 
-let init() = (cst_transp := Sppred.full; var_transp := Idpred.full)
+let init() = (cst_transp := KNpred.full; var_transp := Idpred.full)
 let freeze () = (!var_transp, !cst_transp)
 let unfreeze (vo,co) = (cst_transp := co; var_transp := vo)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 20ec5239e..da2bbfa23 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -12,14 +12,14 @@ open Names
 open Closure
 
 (* Order on section paths for unfolding.
-   If [oracle_order sp1 sp2] is true, then unfold sp1 first.
+   If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
 val oracle_order : table_key -> table_key -> bool
 
 (* Changing the oracle *)
-val set_opaque_const      : section_path -> unit
-val set_transparent_const : section_path -> unit
+val set_opaque_const      : kernel_name -> unit
+val set_transparent_const : kernel_name -> unit
 
 val set_opaque_var      : identifier -> unit
 val set_transparent_var : identifier -> unit
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0313d4d46..616be45f1 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -81,13 +81,13 @@ let modify_opers replfun (constl,indl,cstrl) =
 	   with 
 	     | Not_found -> c')
 
-      | Const sp ->
+      | Const kn ->
 	  (try
-	     (match List.assoc sp constl with
+	     (match List.assoc kn constl with
 		| NOT_OCCUR -> failure ()
 		| DO_ABSTRACT (oper',abs_vars) ->
 		    mkApp (mkConst oper', abs_vars)
-		| DO_REPLACE cb -> substrec (replfun (sp,cb)))
+		| DO_REPLACE cb -> substrec (replfun (kn,cb)))
 	   with 
 	     | Not_found -> c')
   
@@ -98,11 +98,11 @@ let modify_opers replfun (constl,indl,cstrl) =
 let expmod_constr modlist c =
   let simpfun = 
     if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
-  let expfun (sp,cb) = 
+  let expfun (kn,cb) = 
     if cb.const_opaque then
       errorlabstrm "expmod_constr"
 	(str"Cannot unfold the value of " ++
-        str(string_of_path sp) ++ spc () ++
+        str(string_of_kn kn) ++ spc () ++
         str"You cannot declare local lemmas as being opaque" ++ spc () ++
         str"and then require that theorems which use them" ++ spc () ++
         str"be transparent");
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index fca3e0a50..67c0cb998 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
 open Names
 open Univ
 open Term
@@ -35,6 +36,11 @@ type recarg =
   | Mrec of int 
   | Imbr of inductive
 
+let subst_recarg sub r = match r with
+  | Norec | Mrec _  -> r
+  | Imbr (kn,i) -> let kn' = subst_kn 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 [||]
@@ -49,6 +55,8 @@ let dest_subterms p =
   let (_,cstrs) = Rtree.dest_node p in
   Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
 
+let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+
 (* [mind_typename] is the name of the inductive; [mind_arity] is
    the arity generalized over global parameters; [mind_lc] is the list
    of types of constructors generalized over global parameters and
@@ -77,3 +85,78 @@ type mutual_inductive_body = {
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option }
+
+(* TODO: should be changed to non-coping after Term.subst_mps *)
+let subst_const_body sub cb = 
+  { const_body = option_app (Term.subst_mps sub) cb.const_body;
+    const_type = type_app (Term.subst_mps sub) cb.const_type;
+    const_hyps = (assert (cb.const_hyps=[]); []);
+    const_constraints = cb.const_constraints;
+    const_opaque = cb.const_opaque}
+  
+let subst_mind_packet sub mbp = 
+  { mind_consnames = mbp.mind_consnames;
+    mind_typename = mbp.mind_typename;
+    mind_nf_lc = 
+      array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_nf_lc;
+    mind_nf_arity = type_app (Term.subst_mps sub) mbp.mind_nf_arity;
+    mind_user_lc = 
+      array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_user_lc;
+    mind_user_arity = type_app (Term.subst_mps sub) mbp.mind_user_arity;
+    mind_sort = mbp.mind_sort;
+    mind_nrealargs = mbp.mind_nrealargs;
+    mind_kelim = mbp.mind_kelim;
+    mind_nparams = mbp.mind_nparams;
+    mind_params_ctxt = 
+      map_rel_context (Term.subst_mps sub) mbp.mind_params_ctxt;
+    mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
+}
+
+let subst_mind sub mib = 
+  { mind_finite = mib.mind_finite ;
+    mind_ntypes = mib.mind_ntypes ;
+    mind_hyps = (assert (mib.mind_hyps=[]); []) ;
+    mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
+    mind_constraints = mib.mind_constraints ;
+    mind_singl = option_app (Term.subst_mps sub) mib.mind_singl;
+}
+
+
+(*s Modules: signature component specifications, module types, and
+  module declarations *)
+
+type specification_body = 
+  | SPBconst of constant_body
+  | SPBmind of mutual_inductive_body
+  | SPBmodule of module_specification_body
+  | SPBmodtype of module_type_body
+
+and module_signature_body = (label * specification_body) list
+
+and module_type_body = 
+  | MTBident of kernel_name
+  | MTBfunsig of mod_bound_id * module_type_body * module_type_body
+  | MTBsig of mod_self_id * module_signature_body
+
+and module_expr_body =
+  | MEBident of module_path
+  | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
+  | MEBstruct of mod_self_id * module_structure_body
+  | MEBapply of module_expr_body * module_expr_body
+      * constraints
+
+and module_specification_body = module_type_body * module_path option
+
+and structure_elem_body = 
+  | SEBconst of constant_body
+  | SEBmind of mutual_inductive_body
+  | SEBmodule of module_body
+  | SEBmodtype of module_type_body
+
+and module_structure_body = (label * structure_elem_body) list
+
+and module_body = 
+    { mod_expr : module_expr_body option;
+      mod_user_type : (module_type_body * constraints) option;
+      mod_type : module_type_body;
+      mod_equiv : module_path option }
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 8a03e1cda..9ea7e20f8 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -15,10 +15,11 @@ open Term
 open Sign
 (*i*)
 
-(* This module defines the types of global declarations. This includes
-   global constants/axioms and mutual inductive definitions *)
+(* This module defines the internal representation of global
+   declarations. This includes global constants/axioms, mutual
+   inductive definitions, modules and module types *)
 
-(*s Constants (internal representation) (Definition/Axiom) *)
+(*s Constants (Definition/Axiom) *)
 
 type constant_body = {
   const_hyps : section_context; (* New: younger hyp at top *)
@@ -27,6 +28,8 @@ type constant_body = {
   const_constraints : constraints;
   const_opaque : bool }
 
+val subst_const_body : substitution -> constant_body -> constant_body
+
 (*s Inductive types (internal representation with redundant
     information). *)
 
@@ -35,6 +38,8 @@ type recarg =
   | Mrec of int 
   | Imbr of inductive
 
+val subst_recarg : substitution -> recarg -> recarg
+
 type wf_paths = recarg Rtree.t
 
 val mk_norec : wf_paths
@@ -42,6 +47,8 @@ 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 subst_wf_paths : substitution -> wf_paths -> wf_paths
+
 (* [mind_typename] is the name of the inductive; [mind_arity] is
    the arity generalized over global parameters; [mind_lc] is the list
    of types of constructors generalized over global parameters and
@@ -70,3 +77,51 @@ type mutual_inductive_body = {
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option }
+
+
+val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
+
+
+(*s Modules: signature component specifications, module types, and
+  module declarations *)
+
+type specification_body = 
+  | SPBconst of constant_body
+  | SPBmind of mutual_inductive_body
+  | SPBmodule of module_specification_body
+  | SPBmodtype of module_type_body
+
+and module_signature_body = (label * specification_body) list
+
+and module_type_body = 
+  | MTBident of kernel_name
+  | MTBfunsig of mod_bound_id * module_type_body * module_type_body
+  | MTBsig of mod_self_id * module_signature_body
+
+and module_expr_body =
+  | MEBident of module_path
+  | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
+  | MEBstruct of mod_self_id * module_structure_body
+  | MEBapply of module_expr_body * module_expr_body
+      * constraints
+
+and module_specification_body = module_type_body * module_path option
+
+and structure_elem_body = 
+  | SEBconst of constant_body
+  | SEBmind of mutual_inductive_body
+  | SEBmodule of module_body
+  | SEBmodtype of module_type_body
+
+and module_structure_body = (label * structure_elem_body) list
+
+and module_body = 
+    { mod_expr : module_expr_body option;
+      mod_user_type : (module_type_body * constraints) option;
+      mod_type : module_type_body;
+      mod_equiv : module_path option }
+
+
+
+
+
diff --git a/kernel/entries.ml b/kernel/entries.ml
new file mode 100644
index 000000000..4d86d6d2c
--- /dev/null
+++ b/kernel/entries.ml
@@ -0,0 +1,98 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Univ
+open Term
+open Sign
+(*i*)
+
+(* This module defines the entry types for global declarations. This
+   information is entered in the environments. This includes global
+   constants/axioms, mutual inductive definitions, modules and module
+   types *)
+
+
+(*s Local entries *)
+
+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+
+
+(*s Declaration of inductive types. *)
+
+(* Assume the following definition in concrete syntax:
+\begin{verbatim}
+Inductive I1 [x1:X1;...;xn:Xn] : A1 := c11 : T11 | ... | c1n1 : T1n1
+...
+with  Ip [x1:X1;...;xn:Xn] : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
+\end{verbatim}
+then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
+[mind_entry_arity] is [Ai], defined in context [[[x1:X1;...;xn:Xn]];
+[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
+*)
+
+type one_inductive_entry = {
+  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_typename : identifier;
+  mind_entry_arity : constr;
+  mind_entry_consnames : identifier list;
+  mind_entry_lc : constr list }
+
+type mutual_inductive_entry = {
+  mind_entry_finite : bool;
+  mind_entry_inds : one_inductive_entry list }
+
+
+(*s Constants (Definition/Axiom) *)
+
+type definition_entry = {
+  const_entry_body   : constr;
+  const_entry_type   : types option;
+  const_entry_opaque : bool }
+
+type parameter_entry = types
+
+type constant_entry = 
+  | DefinitionEntry of definition_entry
+  | ParameterEntry of parameter_entry
+
+(*s Modules *)
+
+type specification_entry = 
+    SPEconst of constant_entry
+  | SPEmind of mutual_inductive_entry
+  | SPEmodule of module_entry
+  | SPEmodtype of module_type_entry
+
+and module_type_entry = 
+    MTEident of kernel_name
+  | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
+  | MTEsig of mod_self_id * module_signature_entry
+
+and module_signature_entry = (label * specification_entry) list
+
+
+
+and module_expr = 
+    MEident of module_path
+  | MEfunctor of mod_bound_id * module_type_entry * module_expr
+  | MEstruct of mod_self_id * module_structure
+  | MEapply of module_expr * module_expr
+
+and module_structure = (label * specification_entry) list
+
+
+and module_entry = 
+    { mod_entry_type : module_type_entry option;
+      mod_entry_expr : module_expr option}
+
diff --git a/kernel/entries.mli b/kernel/entries.mli
new file mode 100644
index 000000000..4d86d6d2c
--- /dev/null
+++ b/kernel/entries.mli
@@ -0,0 +1,98 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Univ
+open Term
+open Sign
+(*i*)
+
+(* This module defines the entry types for global declarations. This
+   information is entered in the environments. This includes global
+   constants/axioms, mutual inductive definitions, modules and module
+   types *)
+
+
+(*s Local entries *)
+
+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+
+
+(*s Declaration of inductive types. *)
+
+(* Assume the following definition in concrete syntax:
+\begin{verbatim}
+Inductive I1 [x1:X1;...;xn:Xn] : A1 := c11 : T11 | ... | c1n1 : T1n1
+...
+with  Ip [x1:X1;...;xn:Xn] : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
+\end{verbatim}
+then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
+[mind_entry_arity] is [Ai], defined in context [[[x1:X1;...;xn:Xn]];
+[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
+*)
+
+type one_inductive_entry = {
+  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_typename : identifier;
+  mind_entry_arity : constr;
+  mind_entry_consnames : identifier list;
+  mind_entry_lc : constr list }
+
+type mutual_inductive_entry = {
+  mind_entry_finite : bool;
+  mind_entry_inds : one_inductive_entry list }
+
+
+(*s Constants (Definition/Axiom) *)
+
+type definition_entry = {
+  const_entry_body   : constr;
+  const_entry_type   : types option;
+  const_entry_opaque : bool }
+
+type parameter_entry = types
+
+type constant_entry = 
+  | DefinitionEntry of definition_entry
+  | ParameterEntry of parameter_entry
+
+(*s Modules *)
+
+type specification_entry = 
+    SPEconst of constant_entry
+  | SPEmind of mutual_inductive_entry
+  | SPEmodule of module_entry
+  | SPEmodtype of module_type_entry
+
+and module_type_entry = 
+    MTEident of kernel_name
+  | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
+  | MTEsig of mod_self_id * module_signature_entry
+
+and module_signature_entry = (label * specification_entry) list
+
+
+
+and module_expr = 
+    MEident of module_path
+  | MEfunctor of mod_bound_id * module_type_entry * module_expr
+  | MEstruct of mod_self_id * module_structure
+  | MEapply of module_expr * module_expr
+
+and module_structure = (label * specification_entry) list
+
+
+and module_entry = 
+    { mod_entry_type : module_type_entry option;
+      mod_entry_expr : module_expr option}
+
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e4fc5c0e9..d32d232fa 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -24,10 +24,10 @@ type compilation_unit_name = dir_path * checksum
 type global = Constant | Inductive
 
 type globals = {
-  env_constants : constant_body Spmap.t;
-  env_inductives : mutual_inductive_body Spmap.t;
-  env_locals : (global * section_path) list;
-  env_imports : compilation_unit_name list }
+  env_constants : constant_body KNmap.t;
+  env_inductives : mutual_inductive_body KNmap.t;
+  env_modules : module_body MPmap.t;
+  env_modtypes : module_type_body KNmap.t }
 
 type env = {
   env_globals       : globals;
@@ -37,10 +37,10 @@ type env = {
   
 let empty_env = { 
   env_globals = {
-    env_constants = Spmap.empty;
-    env_inductives = Spmap.empty;
-    env_locals = [];
-    env_imports = [] };
+    env_constants = KNmap.empty;
+    env_inductives = KNmap.empty;
+    env_modules = MPmap.empty;
+    env_modtypes = KNmap.empty };
   env_named_context = empty_named_context;
   env_rel_context = empty_rel_context;
   env_universes = initial_universes }
@@ -118,29 +118,27 @@ let fold_named_context_reverse f ~init env =
   Sign.fold_named_context_reverse f ~init:init (named_context env) 
 
 (* Global constants *)
-let lookup_constant sp env =
-  Spmap.find sp env.env_globals.env_constants
+let lookup_constant kn env =
+  KNmap.find kn env.env_globals.env_constants
 
-let add_constant sp cb env =
-  let new_constants = Spmap.add sp cb env.env_globals.env_constants in
-  let new_locals = (Constant,sp)::env.env_globals.env_locals in
+let add_constant kn cb env =
+  let new_constants = KNmap.add kn cb env.env_globals.env_constants in
   let new_globals = 
     { env.env_globals with 
-	env_constants = new_constants; 
-	env_locals = new_locals } in
+	env_constants = new_constants } in 
   { env with env_globals = new_globals }
 
 (* constant_type gives the type of a constant *)
-let constant_type env sp =
-  let cb = lookup_constant sp env in
+let constant_type env kn =
+  let cb = lookup_constant kn env in
   cb.const_type  
 
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
 
-let constant_value env sp =
-  let cb = lookup_constant sp env in
+let constant_value env kn =
+  let cb = lookup_constant kn env in
   if cb.const_opaque then raise (NotEvaluableConst Opaque);
   match cb.const_body with
     | Some body -> body
@@ -156,16 +154,14 @@ let evaluable_constant cst env =
   with Not_found | NotEvaluableConst _ -> false
 
 (* Mutual Inductives *)
-let lookup_mind sp env =
-  Spmap.find sp env.env_globals.env_inductives
+let lookup_mind kn env =
+  KNmap.find kn env.env_globals.env_inductives
 
-let add_mind sp mib env =
-  let new_inds = Spmap.add sp mib env.env_globals.env_inductives in
-  let new_locals = (Inductive,sp)::env.env_globals.env_locals in
+let add_mind kn mib env =
+  let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
   let new_globals = 
     { env.env_globals with 
-	env_inductives = new_inds;
-	env_locals = new_locals } in
+	env_inductives = new_inds } in
   { env with env_globals = new_globals }
 
 (* Universe constraints *)
@@ -183,8 +179,8 @@ let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
   Sign.instance_from_named_context cmap.const_hyps
 
-let lookup_inductive_variables (sp,i) env =
-  let mis = lookup_mind sp env in
+let lookup_inductive_variables (kn,i) env =
+  let mis = lookup_mind kn env in
   Sign.instance_from_named_context mis.mind_hyps
 
 let lookup_constructor_variables (ind,_) env =
@@ -195,9 +191,9 @@ let lookup_constructor_variables (ind,_) env =
 let vars_of_global env constr =
   match kind_of_term constr with
       Var id -> [id]
-    | Const sp ->
+    | Const kn ->
         List.map destVar 
-          (Array.to_list (lookup_constant_variables sp env))
+          (Array.to_list (lookup_constant_variables kn env))
     | Ind ind ->
         List.map destVar 
           (Array.to_list (lookup_inductive_variables ind env))
@@ -241,67 +237,27 @@ let keep_hyps env needed =
     ~init:empty_named_context
 
 
-(* Constants *)
-
-(*s Modules (i.e. compiled environments). *)
-
-type compiled_env = {
-  cenv_stamped_id : compilation_unit_name;
-  cenv_needed : compilation_unit_name list;
-  cenv_constants : (section_path * constant_body) list;
-  cenv_inductives : (section_path * mutual_inductive_body) list }
-
-let exported_objects env =
-  let gl = env.env_globals in
-  let separate (cst,ind) = function
-    | (Constant,sp) -> (sp,Spmap.find sp gl.env_constants)::cst,ind
-    | (Inductive,sp) -> cst,(sp,Spmap.find sp gl.env_inductives)::ind
-  in
-  List.fold_left separate ([],[]) gl.env_locals
-
-let export env id = 
-  let (cst,ind) = exported_objects env in
-  { cenv_stamped_id = (id,0);
-    cenv_needed = env.env_globals.env_imports;
-    cenv_constants = cst;
-    cenv_inductives = ind }
-
-let check_imports env needed =
-  let imports = env.env_globals.env_imports in
-  let check (id,stamp) =
-    try
-      let actual_stamp = List.assoc id imports in
-      if stamp <> actual_stamp then
-	error ("Inconsistent assumptions over module " ^(string_of_dirpath id))
-    with Not_found -> 
-      error ("Reference to unknown module " ^ (string_of_dirpath id))
-  in
-  List.iter check needed
-
-let import_constraints g sp cst =
-  try
-    merge_constraints cst g
-  with UniverseInconsistency ->
-    error "import_constraints: Universe Inconsistency during import"
-
-let import cenv env =
-  check_imports env cenv.cenv_needed;
-  let add_list t = List.fold_left (fun t (sp,x) -> Spmap.add sp x t) t in
-  let gl = env.env_globals in
+(* Modules *)
+
+let add_modtype ln mtb env = 
+  let new_modtypes = KNmap.add ln mtb env.env_globals.env_modtypes in
+  let new_globals = 
+    { env.env_globals with 
+	env_modtypes = new_modtypes } in
+  { env with env_globals = new_globals }
+
+let shallow_add_module mp mb env = 
+  let new_mods = MPmap.add mp mb env.env_globals.env_modules in
   let new_globals = 
-    { env_constants = add_list gl.env_constants cenv.cenv_constants;
-      env_inductives = add_list gl.env_inductives cenv.cenv_inductives;
-      env_locals = gl.env_locals;
-      env_imports = cenv.cenv_stamped_id :: gl.env_imports }
-  in
-  let g = universes env in
-  let g = List.fold_left 
-	    (fun g (sp,cb) -> import_constraints g sp cb.const_constraints) 
-	    g cenv.cenv_constants in
-  let g = List.fold_left 
-	    (fun g (sp,mib) -> import_constraints g sp mib.mind_constraints) 
-	    g cenv.cenv_inductives in
-  { env with env_globals = new_globals; env_universes = g }
+    { env.env_globals with 
+	env_modules = new_mods } in
+  { env with env_globals = new_globals }
+
+let lookup_module mp env = 
+  MPmap.find mp env.env_globals.env_modules
+
+let lookup_modtype ln env = 
+  KNmap.find ln env.env_globals.env_modtypes
 
 (*s Judgments. *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 98f6380c0..2b2be6b6b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -101,6 +101,16 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
 val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 
 (***********************************************************************)
+(*s Modules *)
+val add_modtype : kernel_name -> module_type_body -> env -> env
+
+(* [shallow_add_module] does not add module components *)
+val shallow_add_module : module_path -> module_body -> env -> env
+
+val lookup_module : module_path -> env -> module_body
+val lookup_modtype : kernel_name -> env -> module_type_body
+
+(***********************************************************************)
 (*s Universe constraints *)
 val set_universes   :   Univ.universes -> env -> env
 val add_constraints : Univ.constraints -> env -> env
@@ -116,14 +126,6 @@ val vars_of_global : env -> constr -> identifier list
 val keep_hyps : env -> Idset.t -> section_context
 
 (***********************************************************************)
-(*s Modules. *)
-
-type compiled_env
-
-val export : env -> dir_path -> compiled_env
-val import : compiled_env -> env -> env
-
-(***********************************************************************)
 (*s Unsafe judgments. We introduce here the pre-type of judgments, which is
   actually only a datatype to store a term with its type and the type of its
   type. *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 96c2eaf98..036bce60b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -18,25 +18,13 @@ open Sign
 open Environ
 open Reduction
 open Typeops
+open Entries
 
 (* [check_constructors_names id s cl] checks that all the constructors names
    appearing in [l] are not present in the set [s], and returns the new set
    of names. The name [id] is the name of the current inductive type, used
    when reporting the error. *)
 
-(*s Declaration. *)
-
-type one_inductive_entry = {
-  mind_entry_params : (identifier * local_entry) list;
-  mind_entry_typename : identifier;
-  mind_entry_arity : constr;
-  mind_entry_consnames : identifier list;
-  mind_entry_lc : constr list }
-
-type mutual_inductive_entry = {
-  mind_entry_finite : bool;
-  mind_entry_inds : one_inductive_entry list }
-
 (***********************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
@@ -48,6 +36,7 @@ type inductive_error =
   | NonPar of env * constr * int * constr * constr
   | SameNamesTypes of identifier
   | SameNamesConstructors of identifier * identifier
+  | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
   (* These are errors related to recursors building in Indrec *)
@@ -356,11 +345,11 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
                 if not (List.for_all (noccur_between n ntypes) largs)
 	        then raise (IllFormedInd (LocalNonPos n)));
           rarg
-      | Ind ind_sp ->
+      | Ind ind_kn ->
           (* If the inductive type being defined appears in a
              parameter, then we have an imbricated type *)
           if List.for_all (noccur_between n ntypes) largs then mk_norec
-          else check_positive_imbr ienv (ind_sp, largs)
+          else check_positive_imbr ienv (ind_kn, largs)
       | err -> 
 	  if noccur_between n ntypes x &&
              List.for_all (noccur_between n ntypes) largs 
@@ -548,3 +537,4 @@ let check_inductive env mie =
   let recargs = check_positivity env_arities inds in
   (* Build the inductive packets *)
   build_inductive env env_arities mie.mind_entry_finite inds recargs cst
+
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 532471ebc..4e0f9012c 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,6 +14,7 @@ open Univ
 open Term
 open Declarations
 open Environ
+open Entries
 open Typeops
 (*i*)
 
@@ -29,6 +30,7 @@ type inductive_error =
   | NonPar of env * constr * int * constr * constr
   | SameNamesTypes of identifier
   | SameNamesConstructors of identifier * identifier
+  | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
   (* These are errors related to recursors building in Indrec *)
@@ -38,30 +40,6 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
-(*s Declaration of inductive types. *)
-
-(* Assume the following definition in concrete syntax:
-\begin{verbatim}
-Inductive I1 [x1:X1;...;xn:Xn] : A1 := c11 : T11 | ... | c1n1 : T1n1
-...
-with  Ip [x1:X1;...;xn:Xn] : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
-\end{verbatim}
-then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
-[mind_entry_arity] is [Ai], defined in context [[[x1:X1;...;xn:Xn]];
-[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
-*)
-
-type one_inductive_entry = {
-  mind_entry_params : (identifier * local_entry) list;
-  mind_entry_typename : identifier;
-  mind_entry_arity : constr;
-  mind_entry_consnames : identifier list;
-  mind_entry_lc : constr list }
-
-type mutual_inductive_entry = {
-  mind_entry_finite : bool;
-  mind_entry_inds : one_inductive_entry list }
-
 (*s The following function does checks on inductive declarations. *)
 
 val check_inductive :
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8fe4fa032..cc2c37790 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -19,8 +19,8 @@ open Reduction
 open Type_errors
 
 (* raise Not_found if not an inductive type *)
-let lookup_mind_specif env (sp,tyi) =
-  let mib = Environ.lookup_mind sp env in
+let lookup_mind_specif env (kn,tyi) =
+  let mib = Environ.lookup_mind kn env in
   if tyi >= Array.length mib.mind_packets then
     error "Inductive.lookup_mind_specif: invalid inductive index";
   (mib, mib.mind_packets.(tyi))
@@ -109,10 +109,12 @@ let type_of_constructor env cstr =
   if i > nconstr then error "Not enough constructors in the type";
   constructor_instantiate (fst ind) mib specif.(i-1)
 
-let arities_of_constructors env ind = 
-  let (mib,mip) = lookup_mind_specif env ind in
+let arities_of_specif kn (mib,mip) = 
   let specif = mip.mind_nf_lc in
-  Array.map (constructor_instantiate (fst ind) mib) specif
+  Array.map (constructor_instantiate kn mib) specif
+
+let arities_of_constructors env ind = 
+  arities_of_specif (fst ind) (lookup_mind_specif env ind)
 
 
 
@@ -337,8 +339,8 @@ type guard_env =
     genv    : subterm_spec list;
   }
 
-let make_renv env minds recarg (sp,tyi) =
-  let mib = Environ.lookup_mind sp env in
+let make_renv env minds recarg (kn,tyi) =
+  let mib = Environ.lookup_mind kn env in
   let mind_recvec =
     Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
   { env = env;
@@ -586,12 +588,12 @@ let check_one_fix renv recpos def =
                 bodies in
             array_for_all (fun b -> b) ok_vect
 
-      | Const sp as c -> 
+      | Const kn as c -> 
           (try List.for_all (check_rec_call renv) l
            with (FixGuardError _ ) as e ->
-             if evaluable_constant sp renv.env then 
+             if evaluable_constant kn renv.env then 
 	       check_rec_call renv
-                 (applist(constant_value renv.env sp, l))
+                 (applist(constant_value renv.env kn, l))
 	     else raise e)
 
       (* The cases below simply check recursively the condition on the
@@ -734,9 +736,9 @@ let check_one_cofix env nbfix def deftype =
              else  
 	       error "check_one_cofix: ???"  (* ??? *)
 		 
-	| Construct (_,i as cstr_sp)  ->
+	| Construct (_,i as cstr_kn)  ->
             let lra =vlra.(i-1) in 
-            let mI = inductive_of_constructor cstr_sp in
+            let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
             let _,realargs = list_chop mip.mind_nparams args in
             let rec process_args_of_constr = function
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 79900a84e..f279eb79a 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -43,6 +43,10 @@ val type_of_constructor  : env -> constructor -> types
 (* Return constructor types in normal form *)
 val arities_of_constructors : env -> inductive -> types array
 
+(* Transforms inductive specification into types (in nf) *)
+val arities_of_specif : 
+  kernel_name -> mutual_inductive_body * one_inductive_body -> types array 
+
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
       <p>Cases (c :: (I args)) of b1..bn end
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
new file mode 100644
index 000000000..5c4b00d94
--- /dev/null
+++ b/kernel/mod_typing.ml
@@ -0,0 +1,206 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Util
+open Names
+open Univ
+open Declarations
+open Entries
+open Environ
+open Term_typing
+open Modops
+open Subtyping
+
+exception Not_path
+
+let path_of_mexpr = function
+  | MEident mb -> mb
+  | _ -> raise Not_path
+
+
+let rec list_fold_map2 f e = function 
+  |  []  -> (e,[],[])
+  |  h::t -> 
+       let e',h1',h2' = f e h in
+       let e'',t1',t2' = list_fold_map2 f e' t in
+	 e'',h1'::t1',h2'::t2'
+
+
+let rec translate_modtype env mte =
+  match mte with
+    | MTEident ln -> MTBident ln
+    | MTEfunsig (arg_id,arg_e,body_e) -> 
+	let arg_b = translate_modtype env arg_e in
+	let env' = 
+	  add_module (MPbound arg_id) (module_body_of_type arg_b) env in
+	let body_b = translate_modtype env' body_e in
+	  MTBfunsig (arg_id,arg_b,body_b)
+    | MTEsig (msid,sig_e) ->
+	let str_b,sig_b = translate_entry_list env msid false sig_e in
+	  MTBsig (msid,sig_b)
+
+and translate_entry_list env msid is_definition sig_e = 
+  let mp = MPself msid in
+  let do_entry env (l,e) = 
+    let kn = make_kn mp empty_dirpath l in
+    match e with
+      | SPEconst ce ->
+	  let cb = translate_constant env ce in
+	    add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb)
+      | SPEmind mie -> 
+	  let mib = translate_mind env mie in
+	    add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib)
+      | SPEmodule me ->
+	  let mb = translate_module env is_definition me in
+	  let mspec = mb.mod_type, mb.mod_equiv in
+	  let mp' = MPdot (mp,l) in
+	    add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec)
+      | SPEmodtype mte ->
+	  let mtb = translate_modtype env mte in
+	    add_modtype kn mtb env, (l, SEBmodtype mtb), (l, SPBmodtype mtb)
+  in
+  let _,str_b,sig_b = list_fold_map2 do_entry env sig_e
+  in
+    str_b,sig_b
+
+(* if [is_definition=true], [mod_entry_expr] may be any expression.
+   Otherwise it must be a path *)
+
+and translate_module env is_definition me =
+  match me.mod_entry_expr, me.mod_entry_type with
+    | None, None -> 
+	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
+    | None, Some mte -> 
+	let mtb = translate_modtype env mte in
+	{ mod_expr = None;
+	  mod_user_type = Some (mtb, Constraint.empty);
+	  mod_type = mtb;
+	  mod_equiv = None }
+    | Some mexpr, _ -> 
+	let meq_o = (* do we have a transparent module ? *)
+	  try       (* TODO: transparent field in module_entry *)
+	    Some (path_of_mexpr mexpr)
+	  with 
+	    | Not_path -> None
+	in
+	let meb,mtb1 = 
+	  if is_definition then
+	    translate_mexpr env mexpr
+	  else 
+	    let mp = 
+	      try 
+		path_of_mexpr mexpr 
+	      with 
+		| Not_path -> error_declaration_not_path mexpr
+	    in
+	      MEBident mp, (lookup_module mp env).mod_type
+	in
+	let mtb,mod_user_type =
+	  match me.mod_entry_type with
+	    | None -> mtb1, None
+	    | Some mte -> 
+		let mtb2 = translate_modtype env mte in
+		  mtb2, Some (mtb2, check_subtypes env mtb1 mtb2)
+	in
+	  { mod_type = mtb;
+	    mod_user_type = mod_user_type;
+	    mod_expr = Some meb;
+	    mod_equiv = meq_o }
+
+(* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
+and translate_mexpr env mexpr = match mexpr with
+  | MEident mp -> 
+      MEBident mp,
+      (lookup_module mp env).mod_type
+  | MEfunctor (arg_id, arg_e, body_expr) ->
+      let arg_b = translate_modtype env arg_e in
+      let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in
+      let (body_b,body_tb) = translate_mexpr env' body_expr in
+	MEBfunctor (arg_id, arg_b, body_b), 
+	MTBfunsig (arg_id, arg_b, body_tb)
+  | MEapply (fexpr,mexpr) ->
+      let feb,ftb = translate_mexpr env fexpr in
+      let ftb = scrape_modtype env ftb in
+      let farg_id, farg_b, fbody_b = destr_functor ftb in
+      let meb,mtb = translate_mexpr env mexpr in
+      let cst = check_subtypes env mtb farg_b in
+      let mp = 
+	try
+	  path_of_mexpr mexpr 
+	with
+	  | Not_path -> error_application_to_not_path mexpr
+	      (* place for nondep_supertype *)
+      in
+	MEBapply(feb,meb,cst),
+	subst_modtype (map_mbid farg_id mp) fbody_b
+  | MEstruct (msid,structure) ->
+      let structure,signature = translate_entry_list env msid true structure in
+	MEBstruct (msid,structure),
+	MTBsig (msid,signature)
+
+
+(* is_definition is true - me.mod_entry_expr may be any expression *)
+let translate_module env me = translate_module env true me
+
+let rec add_module_expr_constraints env = function
+  | MEBident _ -> env
+
+  | MEBfunctor (_,mtb,meb) -> 
+      add_module_expr_constraints (add_modtype_constraints env mtb) meb
+
+  | MEBstruct (_,mod_struct_body) ->
+      List.fold_left 
+        (fun env (l,item) -> add_struct_elem_constraints env item)
+        env
+        mod_struct_body
+
+  | MEBapply (meb1,meb2,cst) ->
+      Environ.add_constraints cst 
+        (add_module_expr_constraints 
+	  (add_module_expr_constraints env meb1) 
+	  meb2)
+
+and add_struct_elem_constraints env = function 
+  | SEBconst cb -> Environ.add_constraints cb.const_constraints env
+  | SEBmind mib -> Environ.add_constraints mib.mind_constraints env
+  | SEBmodule mb -> add_module_constraints env mb
+  | SEBmodtype mtb -> add_modtype_constraints env mtb
+
+and add_module_constraints env mb = 
+  let env = match mb.mod_expr with
+    | None -> env
+    | Some meb -> add_module_expr_constraints env meb
+  in
+  let env = match mb.mod_user_type with
+    | None -> env
+    | Some (mtb,cst) -> 
+	Environ.add_constraints cst (add_modtype_constraints env mtb)
+  in
+    env
+
+and add_modtype_constraints env = function
+  | MTBident _ -> env
+  | MTBfunsig (_,mtb1,mtb2) ->
+      add_modtype_constraints
+        (add_modtype_constraints env mtb1)
+        mtb2
+  | MTBsig (_,mod_sig_body) ->
+      List.fold_left 
+        (fun env (l,item) -> add_sig_elem_constraints env item)
+        env
+        mod_sig_body
+
+and add_sig_elem_constraints env = function 
+  | SPBconst cb -> Environ.add_constraints cb.const_constraints env
+  | SPBmind mib -> Environ.add_constraints mib.mind_constraints env
+  | SPBmodule (mtb,_) -> add_modtype_constraints env mtb
+  | SPBmodtype mtb -> add_modtype_constraints env mtb
+
+
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
new file mode 100644
index 000000000..7d17d4823
--- /dev/null
+++ b/kernel/mod_typing.mli
@@ -0,0 +1,25 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Declarations
+open Environ
+open Entries
+(*i*)
+
+
+val translate_modtype : env -> module_type_entry -> module_type_body
+
+val translate_module : env -> module_entry -> module_body
+
+val add_modtype_constraints : env -> module_type_body -> env
+
+val add_module_constraints : env -> module_body -> env
+
diff --git a/kernel/modops.ml b/kernel/modops.ml
new file mode 100644
index 000000000..1b0ff8ace
--- /dev/null
+++ b/kernel/modops.ml
@@ -0,0 +1,151 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Declarations
+open Environ
+open Entries
+(*i*)
+
+let error_existing_label l = 
+  error ("The label "^string_of_label l^" is already declared")
+
+let error_declaration_not_path _ = error "Declaration is not a path"
+
+let error_application_to_not_path _ = error "Application to not path"
+
+let error_not_a_functor _ = error "Application of not a functor"
+
+let error_incompatible_modtypes _ _ = error "Incompatible module types"
+
+let error_not_equal _ _ = error "Not equal modules"
+
+let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match")
+
+let error_no_such_label l = error ("No such label "^string_of_label l)
+
+let error_incompatible_labels l l' = 
+  error ("Opening and closing labels are not the same: "
+	 ^string_of_label l^" <> "^string_of_label l'^" !")
+
+let error_result_must_be_signature mtb = 
+  error "The result module type must be a signature"
+
+let error_no_module_to_end _ = 
+  error "No open module to end"
+
+let error_no_modtype_to_end _ =
+  error "No open module type to end"
+
+let error_not_a_modtype s = 
+  error ("\""^s^"\" is not a module type")
+
+let error_not_a_module s = 
+  error ("\""^s^"\" is not a module")
+
+
+let rec scrape_modtype env = function
+  | MTBident ln -> scrape_modtype env (lookup_modtype ln env)
+  | mtb -> mtb
+
+
+let module_body_of_spec spec = 
+  { mod_type = fst spec;
+    mod_equiv = snd spec;
+    mod_expr = None;
+    mod_user_type = None}
+
+let module_body_of_type mtb = 
+  { mod_type = mtb;
+    mod_equiv = None;
+    mod_expr = None;
+    mod_user_type = None}
+
+let module_spec_of_body mb = mb.mod_type, mb.mod_equiv
+
+let destr_functor = function
+  | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
+  | mtb -> error_not_a_functor mtb
+ 
+
+let rec check_modpath_equiv env mp1 mp2 = 
+  if mp1=mp2 then ();
+  let mb1 = lookup_module mp1 env in
+    match mb1.mod_equiv with
+      | None ->
+	  let mb2 = lookup_module mp2 env in
+	    (match mb2.mod_equiv with
+	      | None -> error_not_equal mp1 mp2
+	      | Some mp2' -> check_modpath_equiv env mp2' mp1)
+      | Some mp1' -> check_modpath_equiv env mp2 mp1'
+
+
+let rec subst_modtype sub = function
+  | MTBident ln -> MTBident (subst_kn sub ln)
+  | MTBfunsig (arg_id, arg_b, body_b) ->
+      assert (not (occur_mbid arg_id sub));
+      MTBfunsig (arg_id, 
+		 subst_modtype sub arg_b, 
+		 subst_modtype sub body_b)
+  | MTBsig (sid1, msb) -> 
+      assert (not (occur_msid sid1 sub));
+      MTBsig (sid1, subst_signature sub msb)
+
+and subst_signature sub sign = 
+  let subst_body = function
+      SPBconst cb -> 
+	SPBconst (subst_const_body sub cb)
+    | SPBmind mib -> 
+	SPBmind (subst_mind sub mib)
+    | SPBmodule mb -> 
+	SPBmodule (subst_module sub mb)
+    | SPBmodtype mtb -> 
+	SPBmodtype (subst_modtype sub mtb)
+  in
+    List.map (fun (l,b) -> (l,subst_body b)) sign
+
+and subst_module sub (mtb,mpo as mb) =
+  let mtb' = subst_modtype sub mtb in
+  let mpo' = option_smartmap (subst_mp sub) mpo in
+    if mtb'==mtb && mpo'==mpo then mb else
+      (mtb',mpo')
+
+let subst_signature_msid msid mp = 
+  subst_signature (map_msid msid mp)
+
+(* we assume that the substitution of "mp" into "msid" is already done
+(or unnecessary) *)
+let rec add_signature mp sign env = 
+  let add_one env (l,elem) =
+    let kn = make_kn mp empty_dirpath l in
+      match elem with
+	| SPBconst cb -> Environ.add_constant kn cb env
+	| SPBmind mib -> Environ.add_mind kn mib env
+	| SPBmodule mb -> 
+	    add_module (MPdot (mp,l)) (module_body_of_spec mb) env 
+	    (* adds components as well *)
+	| SPBmodtype mtb -> Environ.add_modtype kn mtb env
+  in
+    List.fold_left add_one env sign
+
+
+and add_module mp mb env = 
+  let env = Environ.shallow_add_module mp mb env in
+    match scrape_modtype env mb.mod_type with
+      | MTBident _ -> anomaly "scrape_modtype does not work!"
+      | MTBsig (msid,sign) -> 
+	  add_signature mp (subst_signature_msid msid mp sign) env
+
+      | MTBfunsig _ -> env
+
+
diff --git a/kernel/modops.mli b/kernel/modops.mli
new file mode 100644
index 000000000..240144785
--- /dev/null
+++ b/kernel/modops.mli
@@ -0,0 +1,79 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Univ
+open Environ
+open Declarations
+open Entries
+(*i*)
+
+(* Various operations on modules and module types *)
+
+(* recursively unfold MTBdent module types *)
+val scrape_modtype : env -> module_type_body -> module_type_body
+
+(* make the environment entry out of type *)
+val module_body_of_type : module_type_body -> module_body
+
+val module_body_of_spec : module_specification_body -> module_body 
+
+val module_spec_of_body : module_body -> module_specification_body
+
+
+val destr_functor : 
+  module_type_body -> mod_bound_id * module_type_body * module_type_body
+
+
+val subst_modtype : substitution -> module_type_body -> module_type_body
+
+val subst_signature_msid :
+  mod_self_id -> module_path -> 
+  module_signature_body -> module_signature_body
+
+(* [add_signature mp sign env] assumes that the substitution [msid]
+   \mapsto [mp] has already been performed (or is not necessary, like
+   when [mp = MPself msid]) *)
+val add_signature : 
+  module_path -> module_signature_body -> env -> env
+
+(* adds a module and its components, but not the constraints *)
+val add_module :
+  module_path -> module_body -> env -> env
+
+val check_modpath_equiv : env -> module_path -> module_path -> unit
+
+val error_existing_label : label -> 'a
+
+val error_declaration_not_path : module_expr -> 'a
+
+val error_application_to_not_path : module_expr -> 'a
+
+val error_not_a_functor : module_expr -> 'a
+
+val error_incompatible_modtypes : 
+  module_type_body -> module_type_body -> 'a
+
+val error_not_match : label -> specification_body -> 'a
+  
+val error_incompatible_labels : label -> label -> 'a
+
+val error_no_such_label : label -> 'a
+
+val error_result_must_be_signature : module_type_body -> 'a
+
+val error_no_module_to_end : unit -> 'a 
+
+val error_no_modtype_to_end : unit -> 'a
+
+val error_not_a_modtype : string -> 'a 
+
+val error_not_a_module : string -> 'a 
diff --git a/kernel/names.ml b/kernel/names.ml
index a92adc607..0209d1c33 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -61,55 +61,203 @@ module ModIdmap = Map.Make(ModIdOrdered)
 let make_dirpath x = x
 let repr_dirpath x = x
 
+let empty_dirpath = []
+
 let string_of_dirpath = function
   | [] -> "<empty>"
   | sl ->
       String.concat "." (List.map string_of_id (List.rev sl))
 
-(*s Section paths are absolute names *)
 
-type section_path = {
-  dirpath : dir_path ;
-  basename : identifier }
+let u_number = ref 0 
+type uniq_ident = int * string * dir_path
+let make_uid dir s = incr u_number;(!u_number,s,dir)
+let string_of_uid (i,s,p) = 
+  "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
 
-let make_path pa id = { dirpath = pa; basename = id }
-let repr_path { dirpath = pa; basename = id } = (pa,id)
+module Umap = Map.Make(struct 
+			 type t = uniq_ident 
+			 let compare = Pervasives.compare
+		       end)
 
-(* parsing and printing of section paths *)
-let string_of_path sp =
-  let (sl,id) = repr_path sp in
-  if sl = [] then string_of_id id
-  else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
 
-let sp_ord sp1 sp2 =
-  let (p1,id1) = repr_path sp1
-  and (p2,id2) = repr_path sp2 in
-  let p_bit = compare p1 p2 in
-  if p_bit = 0 then id_ord id1 id2 else p_bit
+type mod_self_id = uniq_ident
+let make_msid = make_uid
+let string_of_msid = string_of_uid
+
+type mod_bound_id = uniq_ident
+let make_mbid = make_uid
+let string_of_mbid = string_of_uid
+
+type label = string
+let mk_label l = l
+let string_of_label l = l
+
+let id_of_label l = l
+let label_of_id id = id
+
+module Labset = Idset
+module Labmap = Idmap
+
+type module_path =
+  | MPfile of dir_path
+  | MPbound of mod_bound_id
+  | MPself of mod_self_id 
+  | MPdot of module_path * label
+
+let rec string_of_mp = function
+  | MPfile sl -> string_of_dirpath sl
+  | MPbound uid -> string_of_uid uid
+  | MPself uid -> string_of_uid uid
+  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+
+(* we compare labels first if two MPdot's *)
+let rec mp_ord mp1 mp2 = match (mp1,mp2) with
+    MPdot(mp1,l1), MPdot(mp2,l2) -> 
+      let c = Pervasives.compare l1 l2 in
+	if c<>0 then
+	  c
+	else
+	  mp_ord mp1 mp2
+  |  _,_ -> Pervasives.compare mp1 mp2
+
+module MPord = struct
+  type t = module_path
+  let compare = mp_ord
+end
+
+module MPmap = Map.Make(MPord)
+
+
+(* this is correct under the condition that bound and struct
+   identifiers can never be identical (i.e. get the same stamp)! *) 
+
+type substitution = module_path Umap.t
+
+let empty_subst = Umap.empty
+
+let add_msid = Umap.add 
+let add_mbid = Umap.add
+
+let map_msid msid mp = add_msid msid mp empty_subst
+let map_mbid mbid mp = add_msid mbid mp empty_subst
+
+let join subst = 
+  Umap.fold Umap.add subst
+
+let list_contents sub = 
+  let one_pair uid mp l =
+    (string_of_uid uid, string_of_mp mp)::l
+  in
+    Umap.fold one_pair sub []
+
+let debug_string_of_subst sub = 
+  let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in
+    "{" ^ String.concat "; " l ^ "}"
+
+let debug_pr_subst sub = 
+  let l = list_contents sub in
+  let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) 
+  in
+    str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" 
+
+let rec subst_mp sub mp = (* 's like subst *)
+  match mp with
+    | MPself sid -> 
+	(try Umap.find sid sub with Not_found -> mp)
+    | MPbound bid ->
+	(try Umap.find bid sub with Not_found -> mp)
+    | MPdot (mp1,l) -> 
+	let mp1' = subst_mp sub mp1 in
+	  if mp1==mp1' then 
+	    mp
+	  else
+	    MPdot (mp1',l)
+    | _ -> mp
+
+
+let rec occur_in_path uid = function
+  | MPself sid -> sid = uid
+  | MPbound bid -> bid = uid
+  | MPdot (mp1,_) -> occur_in_path uid mp1
+  | _ -> false
+    
+let occur_uid uid sub = 
+  let check_one uid' mp =
+    if uid = uid' || occur_in_path uid mp then raise Exit
+  in
+    try 
+      Umap.iter check_one sub;
+      false
+    with Exit -> true
+
+let occur_msid = occur_uid
+let occur_mbid = occur_uid
+
+
+
+(* Kernel names *)
+
+type kernel_name = module_path * dir_path * label
+
+let make_kn mp dir l = (mp,dir,l)
+let repr_kn kn = kn
+
+let modpath kn = 
+  let mp,_,_ = repr_kn kn in mp
+
+let label kn = 
+  let _,_,l = repr_kn kn in l
+
+let string_of_kn (mp,dir,l) = 
+  string_of_mp mp ^ "#" ^ string_of_dirpath dir ^ "#" ^ string_of_label l
+
+let pr_kn kn = str (string_of_kn kn)
+
+
+let subst_kn sub (mp,dir,l as kn) = 
+  let mp' = subst_mp sub mp in
+    if mp==mp' then kn else (mp',dir,l)
+
+
+let kn_ord kn1 kn2 = 
+    let mp1,dir1,l1 = kn1 in
+    let mp2,dir2,l2 = kn2 in
+    let c = Pervasives.compare l1 l2 in
+      if c <> 0 then
+	c
+      else 
+	let c = Pervasives.compare dir1 dir2 in
+	  if c<>0 then
+	    c 
+	  else
+	    MPord.compare mp1 mp2
+
+
+module KNord = struct
+  type t = kernel_name
+  let compare =kn_ord
+end
+
+module KNmap = Map.Make(KNord)
+module KNpred = Predicate.Make(KNord)
+module KNset = Set.Make(KNord)
 
-module SpOrdered =
-  struct
-    type t = section_path
-    let compare = sp_ord
-  end
 
-module Spset = Set.Make(SpOrdered)
-module Sppred = Predicate.Make(SpOrdered)
-module Spmap = Map.Make(SpOrdered)
+let initial_msid = (make_msid [] "TOP")
+let initial_path = MPself initial_msid
 
-(*s********************************************************************)
-(* type of global reference *)
 
 type variable = identifier
-type constant = section_path
-type inductive = section_path * int
+type constant = kernel_name
+type mutual_inductive = kernel_name
+type inductive = mutual_inductive * int
 type constructor = inductive * int
-type mutual_inductive = section_path
 
-let ith_mutual_inductive (sp,_) i = (sp,i)
-let ith_constructor_of_inductive ind_sp i = (ind_sp,i)
-let inductive_of_constructor (ind_sp,i) = ind_sp
-let index_of_constructor (ind_sp,i) = i
+let ith_mutual_inductive (kn,_) i = (kn,i)
+let ith_constructor_of_inductive ind i = (ind,i)
+let inductive_of_constructor (ind,i) = ind
+let index_of_constructor (ind,i) = i
 
 (* Hash-consing of name objects *)
 module Hname = Hashcons.Make(
@@ -136,16 +284,12 @@ module Hdir = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-module Hsp = Hashcons.Make(
+module Hkn = Hashcons.Make(
   struct 
-    type t = section_path
+    type t = kernel_name
     type u = identifier -> identifier
-    let hash_sub hident sp =
-      { dirpath = List.map hident sp.dirpath;
-        basename = hident sp.basename }
-    let equal sp1 sp2 =
-      (List.length sp1.dirpath = List.length sp2.dirpath) &&
-      (List.for_all2 (==) sp1.dirpath sp2.dirpath)
+    let hash_sub hident kn = Util.todo "hash_cons"; kn
+    let equal kn1 kn2 = kn1==kn2
     let hash = Hashtbl.hash
   end)
 
@@ -154,5 +298,5 @@ let hcons_names () =
   let hident = Hashcons.simple_hcons Hident.f hstring in
   let hname = Hashcons.simple_hcons Hname.f hident in
   let hdir = Hashcons.simple_hcons Hdir.f hident in
-  let hspcci = Hashcons.simple_hcons Hsp.f hident in
-  (hspcci,hdir,hname,hident,hstring)
+  let hkn = Hashcons.simple_hcons Hkn.f hident in
+  (hkn,hdir,hname,hident,hstring)
diff --git a/kernel/names.mli b/kernel/names.mli
index 08d2db357..b1bcc0b83 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -16,6 +16,8 @@ type name = Name of identifier | Anonymous
 val string_of_id : identifier -> string
 val id_of_string : string -> identifier
 
+val id_ord : identifier -> identifier -> int
+
 (* Identifiers sets and maps *)
 module Idset  : Set.S with type elt = identifier
 module Idpred : Predicate.S with type elt = identifier
@@ -32,44 +34,129 @@ type dir_path
 val make_dirpath : module_ident list -> dir_path
 val repr_dirpath : dir_path -> module_ident list
 
+val empty_dirpath : dir_path
+
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 
 
-(*s Section paths are {\em absolute} names *)
-type section_path
+(*s Unique identifier to be used as "self" in structures and 
+  signatures - invisible for users *)
+  
+type mod_self_id
+
+(* The first argument is a file name - to prevent conflict between 
+   different files *)
+val make_msid : dir_path -> string -> mod_self_id
+val string_of_msid : mod_self_id -> string
+
+(*s Unique names for bound modules *)
+type mod_bound_id
+
+val make_mbid : dir_path -> string -> mod_bound_id
+val string_of_mbid : mod_bound_id -> string
+
+(*s Names of structure elements *)
+type label
+val mk_label : string -> label
+val string_of_label : label -> string
+
+val label_of_id : identifier -> label
+val id_of_label : label -> identifier
+
+module Labset : Set.S with type elt = label
+module Labmap : Map.S with type key = label
+
+(*s The module part of the kernel name *)
+type module_path =
+  | MPfile of dir_path
+  | MPbound of mod_bound_id
+  | MPself of mod_self_id 
+  | MPdot of module_path * label
+(*i  | MPapply of module_path * module_path    in the future (maybe) i*)
+
+
+val string_of_mp : module_path -> string
+
+module MPmap : Map.S with type key = module_path
+
+
+(*s Substitutions *)
+
+type substitution
 
-(* Constructors of [section_path] *)
-val make_path : dir_path -> identifier -> section_path
+val empty_subst : substitution
 
-(* Destructors of [section_path] *)
-val repr_path : section_path -> dir_path * identifier
+val add_msid : 
+  mod_self_id -> module_path -> substitution -> substitution
+val add_mbid : 
+  mod_bound_id -> module_path -> substitution -> substitution
 
-(* Parsing and printing of section path as ["coq_root.module.id"] *)
-val string_of_path : section_path -> string
+val map_msid : mod_self_id -> module_path -> substitution
+val map_mbid : mod_bound_id -> module_path -> substitution
 
-module Spset  : Set.S with type elt = section_path
-module Sppred : Predicate.S with type elt = section_path
-module Spmap  : Map.S with type key = section_path
+val join : substitution -> substitution -> substitution
 
-(*s********************************************************************)
-(* type of global reference *)
+(*i debugging *)
+val debug_string_of_subst : substitution -> string
+val debug_pr_subst : substitution -> Pp.std_ppcmds
+(*i*)
+
+(* [subst_mp sub mp] guarantees that whenever the result of the
+   substitution is structutally equal [mp], it is equal by pointers 
+   as well [==] *) 
+
+val subst_mp : 
+  substitution -> module_path -> module_path
+
+(* [occur_*id id sub] returns true iff [id] occurs in [sub] 
+   on either side *)
+
+val occur_msid : mod_self_id -> substitution -> bool
+val occur_mbid : mod_bound_id -> substitution -> bool
+     
+
+(* Name of the toplevel structure *)
+val initial_msid : mod_self_id
+val initial_path : module_path (* [= MPself initial_msid] *)
+
+(*s The absolute names of objects seen by kernel *)
+
+type kernel_name
+
+(* Constructor and destructor *)
+val make_kn : module_path -> dir_path -> label -> kernel_name
+val repr_kn : kernel_name -> module_path * dir_path * label
+
+val modpath : kernel_name -> module_path
+val label : kernel_name -> label
+
+val string_of_kn : kernel_name -> string
+val pr_kn : kernel_name -> Pp.std_ppcmds
+val subst_kn : substitution -> kernel_name -> kernel_name
+
+
+module KNset  : Set.S with type elt = kernel_name
+module KNpred : Predicate.S with type elt = kernel_name
+module KNmap  : Map.S with type key = kernel_name
+
+
+(*s Specific paths for declarations *)
 
 type variable = identifier
-type constant = section_path
+type constant = kernel_name
+type mutual_inductive = kernel_name
 (* Beware: first inductive has index 0 *)
-type inductive = section_path * int
+type inductive = mutual_inductive * int
 (* Beware: first constructor has index 1 *)
 type constructor = inductive * int
-type mutual_inductive = section_path
 
 val ith_mutual_inductive : inductive -> int -> inductive
-
 val ith_constructor_of_inductive : inductive -> int -> constructor
 val inductive_of_constructor : constructor -> inductive
 val index_of_constructor : constructor -> int
 
 (* Hash-consing *)
 val hcons_names : unit ->
-  (section_path -> section_path) * (dir_path -> dir_path) *
+  (kernel_name -> kernel_name) * (dir_path -> dir_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a5b773c24..4512546ae 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -143,6 +143,11 @@ let sort_cmp pb s0 s1 cuniv =
     | (_, _) -> raise NotConvertible
 
 
+let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty
+
+let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty
+
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = 
   eqappr cv_pb infos
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 50371e85f..63949ceb2 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -29,6 +29,9 @@ exception NotConvertible
 exception NotConvertibleVect of int
 type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
 
+val conv_sort      : sorts conversion_function
+val conv_sort_leq  : sorts conversion_function
+
 val conv           : types conversion_function
 val conv_leq       : types conversion_function
 val conv_leq_vecti : types array conversion_function
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 74e33cdfb..909b12704 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -17,43 +17,75 @@ open Sign
 open Declarations
 open Inductive
 open Environ
+open Entries
+open Typeops
 open Type_errors
 open Indtypes
+open Term_typing
+open Modops
+open Subtyping
+open Mod_typing
 
-type judgment = unsafe_judgment
-let j_val = j_val
-let j_type = j_type
+type modvariant = 
+  | NONE 
+  | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
+  | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
+      * (* optional result type *) module_type_body option
+  | LIBRARY of dir_path
+
+type module_info = 
+    { msid : mod_self_id;
+      modpath : module_path;
+      label : label;
+      variant : modvariant}
 
-(* Exported machines. *)
+let check_label l labset = 
+  if Labset.mem l labset then error_existing_label l
 
-let safe_infer = Typeops.infer
-let safe_infer_type = Typeops.infer_type
+type library_info = dir_path * Digest.t
 
-(*s Safe environments. *)
+type safe_environment = 
+    { old : safe_environment;
+      env : env;
+      modinfo : module_info;
+      labset : Labset.t;
+      revsign : module_signature_body;
+      revstruct : module_structure_body;
+      imports : library_info list;
+      loads : (module_path * module_body) list }
 
-type safe_environment = env
+(*
+  { old = senv.old;
+    env = ;
+    modinfo = senv.modinfo;
+    labset = ;
+    revsign = ;
+    imports = senv.imports ;
+    loads = senv.loads }
+*)
 
-let empty_environment = empty_env
 
-(* Insertion of variables (named and de Bruijn'ed). They are now typed before
-   being added to the environment. *)
+(* a small hack to avoid variants and an unused case in all functions *)
+let rec empty_environment = 
+  { old = empty_environment; 
+    env = empty_env;
+    modinfo = {
+      msid = initial_msid;
+      modpath = initial_path;
+      label = mk_label "_";
+      variant = NONE};
+    labset = Labset.empty;
+    revsign = [];
+    revstruct = [];
+    imports = [];
+    loads = [] }
 
-let constrain_type env j cst1 = function
-  | None -> j.uj_type, cst1
-  | Some t -> 
-      let (tj,cst2) = safe_infer_type env t in
-      let cst3 =
-	try conv_leq env j.uj_type tj.utj_val
-	with NotConvertible -> error_actual_type env j tj.utj_val in
-      tj.utj_val, Constraint.union (Constraint.union cst1 cst2) cst3
+let env_of_safe_env senv = senv.env
+let env_of_senv = env_of_safe_env
 
-let push_rel_or_named_def push (id,b,topt) env =
-  let (j,cst) = safe_infer env b in
-  let (typ,cst) = constrain_type env j cst topt in
-  let env' = add_constraints cst env in
-  let env'' = push (id,Some j.uj_val,typ) env' in
-  (cst,env'')
 
+(* Insertion of section variables. They are now typed before being
+   added to the environment. *)
 
 (* Same as push_named, but check that the variable is not already
    there. Should *not* be done in Environ because tactics add temporary
@@ -65,90 +97,401 @@ let safe_push_named (id,_,_ as d) env =
       let _ = lookup_named id env in 
       error ("identifier "^string_of_id id^" already defined")
     with Not_found -> () in
-  push_named d env
+  Environ.push_named d env
 
-let push_named_def = push_rel_or_named_def safe_push_named
-let push_rel_def = push_rel_or_named_def push_rel
+let push_named_def (id,b,topt) senv =
+  let (c,typ,cst) = translate_local_def senv.env (b,topt) in
+  let env' = add_constraints cst senv.env in
+  let env'' = safe_push_named (id,Some c,typ) env' in
+  (cst, {senv with env=env''})
 
-let push_rel_or_named_assum push (id,t) env =
-  let (j,cst) = safe_infer env t in
-  let t = Typeops.assumption_of_judgment env j in
-  let env' = add_constraints cst env in
-  let env'' = push (id,None,t) env' in
-  (cst,env'')
+let push_named_assum (id,t) senv =
+  let (t,cst) = translate_local_assum senv.env t in
+  let env' = add_constraints cst senv.env in
+  let env'' = safe_push_named (id,None,t) env' in
+  (cst, {senv with env=env''})
 
-let push_named_assum = push_rel_or_named_assum push_named
-let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env)
-
-let push_rels_with_univ vars env =
-  List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
 
 (* Insertion of constants and parameters in environment. *)
-type constant_entry = {
-  const_entry_body   : constr;
-  const_entry_type   : types option;
-  const_entry_opaque : bool }
 
 type global_declaration = 
   | ConstantEntry of constant_entry
-  | ParameterEntry of types
   | GlobalRecipe of Cooking.recipe
 
-(* Definition always declared transparent *)
-let safe_infer_declaration env dcl =
-  match dcl with
-  | ConstantEntry c ->
-      let (j,cst) = safe_infer env c.const_entry_body in
-      let (typ,cst) = constrain_type env j cst c.const_entry_type in
-      Some j.uj_val, typ, cst, c.const_entry_opaque
-  | ParameterEntry t ->
-      let (j,cst) = safe_infer env t in
-      None, Typeops.assumption_of_judgment env j, cst, false
-  | GlobalRecipe r ->
-      Cooking.cook_constant env r
-
-let add_global_declaration sp env (body,typ,cst,op) =
-  let env' = add_constraints cst env in
-  let ids = match body with 
-    | 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 in
-  let cb = {
-    const_body = body;
-    const_type = typ;
-    const_hyps = hyps;
-    const_constraints = cst;
-    const_opaque = op } in
-  Environ.add_constant sp cb env'
-
-(*s Global and local constant declaration. *)
-
-let add_constant sp ce env =
-  let _ =
-    try
-      let _ = lookup_constant sp env in
-      error ("constant "^string_of_path sp^" already declared")
-    with Not_found -> () in
-  add_global_declaration sp env (safe_infer_declaration env ce)
+let add_constant dir l decl senv =
+  check_label l senv.labset;
+  let cb = match decl with 
+      ConstantEntry ce -> translate_constant senv.env ce
+    | GlobalRecipe r -> translate_recipe senv.env r
+  in
+  let env' = Environ.add_constraints cb.const_constraints senv.env in
+  let kn = make_kn senv.modinfo.modpath dir l in
+  let env'' = Environ.add_constant kn cb env' in
+  kn, { old = senv.old;
+	env = env'';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;
+	revsign = (l,SPBconst cb)::senv.revsign;
+	revstruct = (l,SEBconst cb)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+    
 
 (* Insertion of inductive types. *)
 
-let add_mind sp mie env =
-  let _ =
-    try 
-      let _ = lookup_mind sp env in
-      error ("inductive "^string_of_path sp^" already declared")
-    with Not_found -> () in
-  let mib = check_inductive env mie in
-  let cst = mib.mind_constraints in
-  Environ.add_mind sp mib (add_constraints cst env)
+let add_mind dir l mie senv =
+  if mie.mind_entry_inds = [] then 
+    anomaly "empty inductive types declaration"; 
+            (* this test is repeated by translate_mind *)
+  let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
+  if l <> label_of_id id then
+    anomaly ("the label of inductive packet and its first inductive"^
+	     " type do not match");
+  check_label l senv.labset; 
+    (* TODO: when we will allow reorderings we will have to verify 
+       all labels *)
+  let mib = translate_mind senv.env mie in
+  let env' = Environ.add_constraints mib.mind_constraints senv.env in
+  let kn = make_kn senv.modinfo.modpath dir l in
+  let env'' = Environ.add_mind kn mib env' in
+  kn, { old = senv.old;
+	env = env'';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;  (* TODO: the same as above *)
+	revsign = (l,SPBmind mib)::senv.revsign;
+	revstruct = (l,SEBmind mib)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+
+
+(* Insertion of module types *)
+
+let add_modtype l mte senv = 
+  check_label l senv.labset; 
+  let mtb = translate_modtype senv.env mte in
+  let env' = add_modtype_constraints senv.env mtb in
+  let kn = make_kn senv.modinfo.modpath empty_dirpath l in
+  let env'' = Environ.add_modtype kn mtb env' in
+  kn, { old = senv.old;
+	env = env'';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;
+	revsign = (l,SPBmodtype mtb)::senv.revsign;
+	revstruct = (l,SEBmodtype mtb)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+
+
+
+(* full_add_module adds module with universes and constraints *)
+let full_add_module mp mb env =
+  let env = add_module_constraints env mb in
+  let env = Modops.add_module mp mb env in
+    env
+
+(* Insertion of modules *)
+
+let add_module l me senv = 
+  check_label l senv.labset; 
+  let mb = translate_module senv.env me in
+  let mspec = module_spec_of_body mb in
+  let mp = MPdot(senv.modinfo.modpath, l) in
+  let env' = full_add_module mp mb senv.env in
+  mp, { old = senv.old;
+	env = env';
+	modinfo = senv.modinfo;
+	labset = Labset.add l senv.labset;
+	revsign = (l,SPBmodule mspec)::senv.revsign;
+	revstruct = (l,SEBmodule mb)::senv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads }
+
+
+(* Interactive modules *)
+
+let start_module dir l params result senv = 
+  check_label l senv.labset; 
+  let rec trans_params env = function 
+    | [] -> env,[] 
+    | (mbid,mte)::rest -> 
+	let mtb = translate_modtype env mte in
+	let env = 
+	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
+	in
+	let env,transrest = trans_params env rest in
+	env, (mbid,mtb)::transrest
+  in
+  let env,params_body = trans_params senv.env params in
+  let check_sig mtb = match scrape_modtype env mtb with
+    | MTBsig _ -> ()
+    | MTBfunsig _ -> error_result_must_be_signature mtb 
+    | _ -> anomaly "start_module: modtype not scraped"
+  in
+  let result_body = option_app (translate_modtype env) result in
+  ignore (option_app check_sig result_body);
+  let msid = make_msid dir (string_of_label l) in
+  let mp = MPself msid in
+  let modinfo = { msid = msid;
+		  modpath = mp;
+		  label = l;
+		  variant = STRUCT(params_body,result_body) }
+  in
+  mp, { old = senv;
+	env = env;
+	modinfo = modinfo;
+	labset = Labset.empty;
+	revsign = [];
+	revstruct = [];
+	imports = senv.imports;
+	loads = [] }
+
+
+
+let end_module l senv = 
+  let oldsenv = senv.old in
+  let modinfo = senv.modinfo in
+  let params, restype = 
+    match modinfo.variant with
+      | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
+      | STRUCT(params,restype) -> (params,restype)
+  in
+  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
+  let functorize_type = 
+    List.fold_right 
+      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
+      params
+  in
+  let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
+  let mtb, mod_user_type = 
+    match restype with
+      | None -> functorize_type auto_tb, None
+      | Some res_tb -> 
+	  let cnstrs = check_subtypes senv.env auto_tb res_tb in
+	  let mtb = functorize_type res_tb in
+	    mtb, Some (mtb, cnstrs)
+  in
+  let mexpr = 
+    List.fold_right
+      (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb))
+      params
+      (MEBstruct (modinfo.msid, List.rev senv.revstruct)) 
+  in
+  let mb = 
+    { mod_expr = Some mexpr;
+      mod_user_type = mod_user_type;
+      mod_type = mtb;
+      mod_equiv = None }
+  in
+  let mspec = mtb , None in
+  let mp = MPdot (oldsenv.modinfo.modpath, l) in
+  let newenv = oldsenv.env in
+  let newenv = 
+    List.fold_left
+      (fun env (mp,mb) -> full_add_module mp mb env) 
+      newenv
+      senv.loads
+  in
+  let newenv = 
+    full_add_module mp mb newenv
+  in 
+  mp, { old = oldsenv.old;
+	env = newenv;
+	modinfo = oldsenv.modinfo;
+	labset = Labset.add l oldsenv.labset;
+	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
+	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads@oldsenv.loads }
+
+
+(* Interactive module types *)
+
+let start_modtype dir l params senv = 
+  check_label l senv.labset; 
+  let rec trans_params env = function 
+    | [] -> env,[] 
+    | (mbid,mte)::rest -> 
+	let mtb = translate_modtype env mte in
+	let env = 
+	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
+	in
+	let env,transrest = trans_params env rest in
+	env, (mbid,mtb)::transrest
+  in
+  let env,params_body = trans_params senv.env params in
+  let msid = make_msid dir (string_of_label l) in
+  let mp = MPself msid in
+  let modinfo = { msid = msid;
+		  modpath = mp;
+		  label = l;
+		  variant = SIG params_body }
+  in
+  mp, { old = senv;
+	env = env;
+	modinfo = modinfo;
+	labset = Labset.empty;
+	revsign = [];
+	revstruct = [];
+	imports = senv.imports;
+	loads = [] }
 
-let add_constraints = Environ.add_constraints
+let end_modtype l senv = 
+  let oldsenv = senv.old in
+  let modinfo = senv.modinfo in
+  let params = 
+    match modinfo.variant with
+      | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end ()
+      | SIG params -> params
+  in
+  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
+  let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
+  let mtb = 
+    List.fold_right 
+      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
+      params
+      res_tb
+  in
+  let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
+  let newenv = oldsenv.env in
+  let newenv = 
+    List.fold_left
+      (fun env (mp,mb) -> full_add_module mp mb env) 
+      newenv
+      senv.loads
+  in
+  let newenv = 
+    add_modtype_constraints newenv mtb 
+  in
+  let newenv = 
+    Environ.add_modtype kn mtb newenv
+  in 
+  kn, { old = oldsenv.old;
+	env = newenv;
+	modinfo = oldsenv.modinfo;
+	labset = Labset.add l oldsenv.labset;
+	revsign = (l,SPBmodtype mtb)::oldsenv.revsign;
+	revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct;
+	imports = senv.imports;
+	loads = senv.loads@oldsenv.loads }
+  
 
-let export = export
-let import = import
+let current_modpath senv = senv.modinfo.modpath
+let current_msid senv = senv.modinfo.msid
+
+
+let add_constraints cst senv = 
+  {senv with env = Environ.add_constraints cst senv.env}
+
+
+
+(* Libraries = Compiled modules *)
+
+type compiled_library = 
+    dir_path * module_body * library_info list
+
+
+(* We check that only initial state Require's were performed before 
+   [start_library] was called *)
+
+let start_library dir senv =
+  if not (senv.revsign = [] &&
+	  senv.modinfo.msid = initial_msid &&
+	  senv.modinfo.variant = NONE)
+  then
+    anomaly "Safe_typing.start_library: environment should be empty";
+  let dir_path,l = 
+    match (repr_dirpath dir) with
+	[] -> anomaly "Empty dirpath in Safe_typing.start_library"
+      | hd::tl ->
+	  make_dirpath tl, label_of_id hd
+  in
+  let msid = make_msid dir_path (string_of_label l) in
+  let mp = MPself msid in
+  let modinfo = { msid = msid;
+		  modpath = mp;
+		  label = l;
+		  variant = LIBRARY dir }
+  in
+  mp, { old = senv;
+	env = senv.env;
+	modinfo = modinfo;
+	labset = Labset.empty;
+	revsign = [];
+	revstruct = [];
+	imports = senv.imports;
+	loads = [] }
+
+
+let export senv dir = 
+  let modinfo = senv.modinfo in
+  begin
+    match modinfo.variant with
+      | LIBRARY dp -> 
+	  if dir <> dp then
+	    anomaly "We are not exporting the right library!"
+      | _ ->
+	  anomaly "We are not exporting the library"
+  end;
+  (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then
+    (* error_export_simple *) (); *)
+  let mb = 
+    { mod_expr = Some (MEBstruct (modinfo.msid, List.rev senv.revstruct));
+      mod_type = MTBsig (modinfo.msid, List.rev senv.revsign);
+      mod_user_type = None;
+      mod_equiv = None }
+  in
+    modinfo.msid, (dir,mb,senv.imports)
+
+
+let import_constraints g kn cst =
+  try
+    merge_constraints cst g
+  with UniverseInconsistency ->
+    error "import_constraints: Universe Inconsistency during import"
+
+
+let check_imports senv needed =
+  let imports = senv.imports in
+  let check (id,stamp) =
+    try
+      let actual_stamp = List.assoc id imports in
+      if stamp <> actual_stamp then
+	error ("Inconsistent assumptions over module " ^(string_of_dirpath id))
+    with Not_found -> 
+      error ("Reference to unknown module " ^ (string_of_dirpath id))
+  in
+  List.iter check needed
+
+
+(* we have an inefficiency: Since loaded files are added to the
+environment every time a module is closed, their components are
+calculated many times. Thic could be avoided in several ways:
+
+1 - for each file create a dummy environment containing only this
+file's components, merge this environment with the global
+environment, and store for the future (instead of just its type)
+
+2 - create "persistent modules" environment table in Environ add put
+loaded by side-effect once and for all (like it is done in OCaml).
+Would this be correct with respect to undo's and stuff ?
+*)
+ 
+let import (dp,mb,depends) digest senv = 
+  check_imports senv depends;
+  let mp = MPfile dp in
+  let env = senv.env in
+  mp, { senv with 
+	  env = full_add_module mp mb env; 
+	  imports = (dp,digest)::senv.imports;
+	  loads = (mp,mb)::senv.loads }
+
+
+
+type judgment = unsafe_judgment
 
-let env_of_safe_env e = e
+let j_val j = j.uj_val
+let j_type j = j.uj_type
 
-let typing = Typeops.typing
+let safe_infer senv = infer (env_of_senv senv)
+    
+let typing senv = Typeops.typing (env_of_senv senv)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 10357f407..2d4d2403c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -12,12 +12,16 @@
 open Names
 open Term
 open Declarations
+open Entries
 (*i*)
 
-(*s Safe environments. Since we are now able to type terms, we can define an
-  abstract type of safe environments, where objects are typed before being
-  added. Internally, the datatype is still [env]. We re-export the
-  functions of [Environ] for the new type [environment]. *)
+(*s Safe environments. Since we are now able to type terms, we can
+  define an abstract type of safe environments, where objects are
+  typed before being added.
+
+  We also add [open_structure] and [close_section], [close_module] to
+  provide functionnality for sections and interactive modules 
+*)
 
 type safe_environment
 
@@ -34,30 +38,69 @@ val push_named_def :
     Univ.constraints * safe_environment
 
 (* Adding global axioms or definitions *)
-type constant_entry = {
-  const_entry_body   : constr;
-  const_entry_type   : types option;
-  const_entry_opaque : bool }
-
 type global_declaration = 
   | ConstantEntry of constant_entry
-  | ParameterEntry of types
   | GlobalRecipe of Cooking.recipe
 
 val add_constant : 
-  constant -> global_declaration -> safe_environment -> safe_environment
+  dir_path -> label -> global_declaration -> safe_environment -> 
+      kernel_name * safe_environment
 
 (* Adding an inductive type *)
 val add_mind : 
-  mutual_inductive -> Indtypes.mutual_inductive_entry -> safe_environment ->
-    safe_environment
+  dir_path -> label -> mutual_inductive_entry -> safe_environment ->
+    mutual_inductive * safe_environment
+
+(* Adding a module *)
+val add_module :
+  label -> module_entry -> safe_environment 
+    -> module_path * safe_environment
+
+(* Adding a module type *)
+val add_modtype :
+  label -> module_type_entry -> safe_environment 
+    -> kernel_name * safe_environment
 
 (* Adding universe constraints *)
-val add_constraints : Univ.constraints -> safe_environment -> safe_environment
+val add_constraints : 
+  Univ.constraints -> safe_environment -> safe_environment
+
+
+(*s Interactive module functions *)
+val start_module : 
+  dir_path -> label -> (mod_bound_id * module_type_entry) list 
+    -> module_type_entry option 
+      -> safe_environment -> module_path * safe_environment
+
+val end_module :
+  label -> safe_environment -> module_path * safe_environment 
+
+
+val start_modtype :
+  dir_path -> label -> (mod_bound_id * module_type_entry) list
+    -> safe_environment -> module_path * safe_environment
+
+val end_modtype :
+  label -> safe_environment -> kernel_name * safe_environment
+
+
+val current_modpath : safe_environment -> module_path
+val current_msid : safe_environment -> mod_self_id
+
+
+(* Loading and saving compilation units *)
+
+(* exporting and importing modules *)
+type compiled_library
+
+val start_library : dir_path -> safe_environment 
+      -> module_path * safe_environment
+
+val export : safe_environment -> dir_path  
+      -> mod_self_id * compiled_library
 
-(* Loading and saving a module *)
-val export : safe_environment -> dir_path -> Environ.compiled_env
-val import : Environ.compiled_env -> safe_environment -> safe_environment
+val import : compiled_library -> Digest.t -> safe_environment 
+      -> module_path * safe_environment
 
 
 (*s Typing judgments *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index f0c275fa3..29e7379e9 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -71,6 +71,15 @@ let rel_context_nhyps hyps =
 let fold_rel_context f l ~init:x = List.fold_right f l x
 let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
 
+let map_rel_context f l = 
+  let map_decl (n, body_o, typ as decl) =
+    let body_o' = option_smartmap f body_o in
+    let typ' = f typ in
+      if body_o' == body_o && typ' == typ then decl else
+	(n, body_o', typ')
+  in
+    list_smartmap map_decl l
+
 (* Push named declarations on top of a rel context *)
 (* Bizarre. Should be avoided. *)
 let push_named_to_rel_context hyps ctxt =
diff --git a/kernel/sign.mli b/kernel/sign.mli
index e5de5613d..d66421fbd 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -56,6 +56,9 @@ val fold_rel_context :
 val fold_rel_context_reverse :
   ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
 
+(*s Map function of [rel_context] *)
+val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+
 (*s Term constructors *)
 
 val it_mkLambda_or_LetIn : constr -> rel_context -> constr
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
new file mode 100644
index 000000000..5a7ce3cb3
--- /dev/null
+++ b/kernel/subtyping.ml
@@ -0,0 +1,241 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Util
+open Names
+open Univ
+open Term
+open Declarations
+open Environ
+open Reduction
+open Inductive
+open Modops
+(*i*)
+
+(* This local type is used to subtype a constant with a constructor or
+   an inductive type. It can also be useful to allow reorderings in
+   inductive types *)
+
+type namedobject = 
+  | Constant of constant_body
+  | Mind of mutual_inductive_body
+  | IndType of inductive * mutual_inductive_body
+  | IndConstr of constructor * mutual_inductive_body
+  | Module of module_specification_body
+  | Modtype of module_type_body
+
+(* adds above information about one mutual inductive: all types and
+   constructors *)
+
+let add_nameobjects_of_mib ln mib map = 
+  let add_nameobjects_of_one j oib map =
+    let ip = (ln,j) in
+    let map = 
+      array_fold_right_i 
+	(fun i id map -> Idmap.add id (IndConstr ((ip,i), mib)) map)
+	oib.mind_consnames
+	map
+    in
+      Idmap.add oib.mind_typename (IndType (ip, mib)) map
+  in
+    array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+
+(* creates namedobject map for the whole signature *)
+
+let make_label_map msid list = 
+  let add_one (l,e) map = 
+    let obj = 
+      match e with
+	| SPBconst cb -> Constant cb
+	| SPBmind mib -> Mind mib
+	| SPBmodule mb -> Module mb
+	| SPBmodtype mtb -> Modtype mtb
+    in
+(*    let map = match obj with
+      | Mind mib -> 
+	  add_nameobjects_of_mib (make_ln (MPself msid) l) mib map
+      | _ -> map
+    in *)
+      Labmap.add l obj map
+  in
+    List.fold_right add_one list Labmap.empty
+
+let check_conv_error error cst f env a1 a2 =
+  try
+    Constraint.union cst (f env a1 a2)
+  with
+      NotConvertible -> error ()
+
+(* for now we do not allow reorderings *)
+let check_inductive cst env msid1 l info1 mib2 spec2 = 
+  let kn = make_kn (MPself msid1) empty_dirpath l in
+  let error () = error_not_match l spec2 in
+  let check_conv cst f = check_conv_error error cst f in
+  let mib1 = 
+    match info1 with
+      | Mind mib -> mib
+    (*  | IndType (_,mib) -> mib   we will enable this later*)
+      | _ -> error ()
+  in
+  let check_packet cst p1 p2 =
+    let check f = if f p1 <> f p2 then error () in
+      check (fun p -> p.mind_consnames);
+      check (fun p -> p.mind_typename);
+      (* nf_lc later *)
+      (* nf_arity later *)
+      (* user_lc ignored *)
+      (* user_arity ignored *)
+      let cst = check_conv cst conv_sort env p1.mind_sort p2.mind_sort in
+      check (fun p -> p.mind_nrealargs);
+      (* kelim ignored *)
+      (* listrec ignored *)
+      (* finite done *)
+      (* nparams done *)
+      (* params_ctxt done *)
+      let cst = check_conv cst conv env p1.mind_nf_arity p2.mind_nf_arity in
+	cst
+  in
+    (* this function uses mis_something and the others do not.
+       Perhaps we should uniformize it at some point... *)
+  let check_cons_types i cst p1 p2 =
+    array_fold_left2 
+      (fun cst t1 t2 -> check_conv cst conv env t1 t2)
+      cst
+      (arities_of_specif kn (mib1,p1))
+      (arities_of_specif kn (mib2,p2))
+  in
+  let check f = if f mib1 <> f mib2 then error () in
+    check (fun mib -> mib.mind_finite);
+    check (fun mib -> mib.mind_ntypes);
+    assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
+    assert (Array.length mib1.mind_packets >= 1 
+	    && Array.length mib2.mind_packets >= 1);
+    check (fun mib -> mib.mind_packets.(0).mind_nparams);
+    check (fun mib -> mib.mind_packets.(0).mind_params_ctxt); 
+         (* TODO: we should allow renaming of parameters at least ! *)
+    let cst = match mib1.mind_singl, mib2.mind_singl with
+	None, None -> cst
+      | Some c1, Some c2 -> check_conv cst conv env c1 c2
+      | _ -> error ()
+    in
+    (* we first check simple things *)
+    let cst = 
+      array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
+    in
+    (* and constructor types in the end *)
+    let cst = 
+      array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
+    in
+      cst
+    
+let check_constant cst env msid1 l info1 cb2 spec2 = 
+  let error () = error_not_match l spec2 in
+  let check_conv cst f = check_conv_error error cst f in
+  let cb1 = 
+    match info1 with
+      | Constant cb -> cb
+      | _ -> error ()
+  in 
+    assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+    let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in
+    match cb1.const_body, cb2.const_body with
+      | None, None -> cst
+      | Some _, None -> cst
+      | Some c1, Some c2 -> 
+	  check_conv cst conv env c1 c2
+      | None, Some c2 ->
+	  check_conv 
+	    cst
+	    conv 
+	    env 
+	    (mkConst (make_kn (MPself msid1) empty_dirpath l)) 
+	    c2
+
+let rec check_modules cst env msid1 l msb1 msb2 =
+  let cst = check_modtypes cst env (fst msb1) (fst msb2) false in
+  begin
+    match (snd msb1), (snd msb2) with
+      | _, None -> ()
+      | None, Some mp2 -> 
+	  check_modpath_equiv env (MPdot(MPself msid1,l)) mp2
+      | Some mp1, Some mp2 ->
+	  check_modpath_equiv env mp1 mp2
+  end;
+  cst
+	
+
+and check_signatures cst env' (msid1,sig1) (msid2,sig2') = 
+  let mp1 = MPself msid1 in
+  let env = add_signature mp1 sig1 env' in 
+  let sig2 = subst_signature_msid msid2 mp1 sig2' in
+  let map1 = make_label_map msid1 sig1 in
+  let check_one_body cst (l,spec2) = 
+    let info1 = 
+      try 
+	Labmap.find l map1 
+      with 
+	  Not_found -> error_no_such_label l 
+    in
+      match spec2 with
+	| SPBconst cb2 ->
+	    check_constant cst env msid1 l info1 cb2 spec2
+	| SPBmind mib2 -> 
+	    check_inductive cst env msid1 l info1 mib2 spec2
+	| SPBmodule msb2 -> 
+	    let msb1 = 
+	      match info1 with
+		| Module msb -> msb
+		| _ -> error_not_match l spec2
+	    in
+	      check_modules cst env msid1 l msb1 msb2
+	| SPBmodtype mtb2 ->
+	    let mtb1 = 
+	      match info1 with
+		| Modtype mtb -> mtb
+		| _ -> error_not_match l spec2
+	    in
+	      check_modtypes cst env mtb1 mtb2 true
+  in
+    List.fold_left check_one_body cst sig2
+    
+and check_modtypes cst env mtb1 mtb2 equiv = 
+  if mtb1==mtb2 then (); (* just in case  :) *)
+  let mtb1' = scrape_modtype env mtb1 in
+  let mtb2' = scrape_modtype env mtb2 in
+    if mtb1'==mtb2' then ();
+    match mtb1', mtb2' with
+      | MTBsig (msid1,list1), 
+	MTBsig (msid2,list2) -> 
+	  let cst = check_signatures cst env (msid1,list1) (msid2,list2) in
+	  if equiv then
+	    check_signatures cst env (msid2,list2) (msid1,list1) 
+	  else
+	    cst
+      | MTBfunsig (arg_id1,arg_t1,body_t1), 
+	MTBfunsig (arg_id2,arg_t2,body_t2) ->
+	  let cst = check_modtypes cst env arg_t2 arg_t1 equiv in 
+	    (* contravariant *)
+	  let env' = 
+	    add_module (MPbound arg_id2) (module_body_of_type arg_t2) env 
+	  in
+	  let body_t1' = 
+	    subst_modtype 
+	      (map_mbid arg_id1 (MPbound arg_id2)) 
+	      body_t1
+	  in
+	  check_modtypes cst env' body_t1' body_t2 equiv
+      | MTBident _ , _ -> anomaly "Subtyping: scrape failed"
+      | _ , MTBident _ -> anomaly "Subtyping: scrape failed"
+      | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+	  
+let check_subtypes env sup super = 
+  check_modtypes Constraint.empty env sup super false
+
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
new file mode 100644
index 000000000..71c111339
--- /dev/null
+++ b/kernel/subtyping.mli
@@ -0,0 +1,19 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Univ
+open Declarations
+open Environ
+(*i*)
+
+val check_subtypes : env -> module_type_body -> module_type_body -> constraints
+
+
diff --git a/kernel/term.ml b/kernel/term.ml
index 95968f6c8..0c5dc2a54 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -147,7 +147,7 @@ let comp_term t1 t2 =
       & array_for_all2 (==) bl1 bl2
   | _ -> false
 
-let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id)) t =
+let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t =
   match t with
   | Rel _ | Meta _ -> t
   | Var x -> Var (sh_id x)
@@ -158,10 +158,10 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id)) t =
   | LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
   | App (c,l) -> App (sh_rec c, Array.map sh_rec l)
   | Evar (e,l) -> Evar (e, Array.map sh_rec l)
-  | Const c -> Const (sh_sp c)
-  | Ind (sp,i) -> Ind (sh_sp sp,i)
-  | Construct ((sp,i),j) -> Construct ((sh_sp sp,i),j)
-  | Case (ci,p,c,bl) -> (* TO DO: extract ind_sp *)
+  | Const c -> Const (sh_kn c)
+  | Ind (kn,i) -> Ind (sh_kn kn,i)
+  | Construct ((kn,i),j) -> Construct ((sh_kn kn,i),j)
+  | Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *)
       Case (ci, sh_rec p, sh_rec c, Array.map sh_rec bl)
   | Fix (ln,(lna,tl,bl)) ->
       Fix (ln,(Array.map sh_na lna,
@@ -177,15 +177,15 @@ module Hconstr =
     struct
       type t = constr
       type u = (constr -> constr) *
-               ((sorts -> sorts) * (section_path -> section_path)
+               ((sorts -> sorts) * (kernel_name -> kernel_name)
 		* (name -> name) * (identifier -> identifier))
       let hash_sub = hash_term
       let equal = comp_term
       let hash = Hashtbl.hash
     end)
 
-let hcons_term (hsorts,hsp,hname,hident) =
-  Hashcons.recursive_hcons Hconstr.f (hsorts,hsp,hname,hident)
+let hcons_term (hsorts,hkn,hname,hident) =
+  Hashcons.recursive_hcons Hconstr.f (hsorts,hkn,hname,hident)
 
 (* Constructs a DeBrujin index with number n *)
 let rels =
@@ -236,12 +236,12 @@ let mkConst c = Const c
 (* Constructs an existential variable *)
 let mkEvar e = Evar e
 
-(* Constructs the ith (co)inductive type of the block named sp *)
+(* Constructs the ith (co)inductive type of the block named kn *)
 (* The array of terms correspond to the variables introduced in the section *)
 let mkInd m = Ind m
 
 (* Constructs the jth constructor of the ith (co)inductive type of the 
-   block named sp. The array of terms correspond to the variables
+   block named kn. The array of terms correspond to the variables
    introduced in the section *)
 let mkConstruct c = Construct c
 
@@ -380,28 +380,28 @@ let isApp c = match kind_of_term c with App _ -> true | _ -> false
 
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
-  | Const sp -> sp
+  | Const kn -> kn
   | _ -> invalid_arg "destConst"
 
 let isConst c = match kind_of_term c with Const _ -> true | _ -> false
 
 (* Destructs an existential variable *)
 let destEvar c = match kind_of_term c with
-  | Evar (sp, a as r) -> r
+  | Evar (kn, a as r) -> r
   | _ -> invalid_arg "destEvar"
 
 let num_of_evar c = match kind_of_term c with
   | Evar (n, _) -> n
   | _ -> anomaly "num_of_evar called with bad args"
 
-(* Destructs a (co)inductive type named sp *)
+(* Destructs a (co)inductive type named kn *)
 let destInd c = match kind_of_term c with
-  | Ind (sp, a as r) -> r
+  | Ind (kn, a as r) -> r
   | _ -> invalid_arg "destInd"
 
 (* Destructs a constructor *)
 let destConstruct c = match kind_of_term c with
-  | Construct (sp, a as r) -> r
+  | Construct (kn, a as r) -> r
   | _ -> invalid_arg "dest"
 
 let isConstruct c = match kind_of_term c with
@@ -813,6 +813,32 @@ let substn_vars p vars =
 
 let subst_vars = substn_vars 1
 
+(* 
+map_kn : (kernel_name -> kernel_name) -> constr -> constr
+
+This should be rewritten to prevent duplication of constr's when not
+necessary.
+For now, it uses map_constr and is rather ineffective
+*)
+
+let rec map_kn f c = 
+  let func = map_kn f in
+    match kind_of_term c with
+      | Const kn -> 
+	  mkConst (f kn)
+      | Ind (kn,i) -> 
+	  mkInd (f kn,i)
+      | Construct ((kn,i),j) -> 
+	  mkConstruct ((f kn,i),j)
+      | Case (ci,p,c,l) ->
+	  let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in
+	  mkCase (ci', func p, func c, array_smartmap func l) 
+      | _ -> map_constr func c
+
+let subst_mps sub = 
+  map_kn (subst_kn sub)
+
+
 (*********************)
 (* Term constructors *)
 (*********************)
@@ -910,12 +936,12 @@ let mkConst = mkConst
 (* Constructs an existential variable *)
 let mkEvar = mkEvar
 
-(* Constructs the ith (co)inductive type of the block named sp *)
+(* Constructs the ith (co)inductive type of the block named kn *)
 (* The array of terms correspond to the variables introduced in the section *)
 let mkInd = mkInd
 
 (* Constructs the jth constructor of the ith (co)inductive type of the 
-   block named sp. The array of terms correspond to the variables
+   block named kn. The array of terms correspond to the variables
    introduced in the section *)
 let mkConstruct = mkConstruct
 
@@ -1169,9 +1195,9 @@ module Hsorts =
 
 let hsort = Hsorts.f
 
-let hcons_constr (hspcci,hdir,hname,hident,hstr) =
+let hcons_constr (hkn,hdir,hname,hident,hstr) =
   let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
-  let hcci = hcons_term (hsortscci,hspcci,hname,hident) in
+  let hcci = hcons_term (hsortscci,hkn,hname,hident) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
   (hcci,htcci)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 643d06443..6da9d1f5f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -127,12 +127,12 @@ val mkConst : constant -> constr
 
 (* Inductive types *)
 
-(* Constructs the ith (co)inductive type of the block named sp *)
+(* Constructs the ith (co)inductive type of the block named kn *)
 (* The array of terms correspond to the variables introduced in the section *)
 val mkInd : inductive -> constr
 
 (* Constructs the jth constructor of the ith (co)inductive type of the 
-   block named sp. The array of terms correspond to the variables
+   block named kn. The array of terms correspond to the variables
    introduced in the section *)
 val mkConstruct : constructor -> constr
 
@@ -439,6 +439,12 @@ val subst_vars : identifier list -> constr -> constr
    if two names are identical, the one of least indice is keeped *)
 val substn_vars : int -> identifier list -> constr -> constr
 
+
+(* [subst_mps sub c] performs the substitution [sub] on all kernel
+   names appearing in [c] *)
+val subst_mps : substitution -> constr -> constr
+
+
 (*s Functionals working on the immediate subterm of a construction *)
 
 (* [fold_constr f acc c] folds [f] on the immediate subterms of [c]
@@ -496,7 +502,7 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 (*********************************************************************)
 
 val hcons_constr:
-  (section_path -> section_path) *
+  (kernel_name -> kernel_name) *
   (dir_path -> dir_path) *
   (name -> name) *
   (identifier -> identifier) *
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
new file mode 100644
index 000000000..1abe65c20
--- /dev/null
+++ b/kernel/term_typing.ml
@@ -0,0 +1,111 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Univ
+open Term
+open Reduction
+open Sign
+open Declarations
+open Inductive
+open Environ
+open Entries
+open Type_errors
+open Indtypes
+open Typeops
+
+let constrain_type env j cst1 = function
+  | None -> j.uj_type, cst1
+  | Some t -> 
+      let (tj,cst2) = infer_type env t in
+      let cst3 =
+	try conv_leq env j.uj_type tj.utj_val
+	with NotConvertible -> error_actual_type env j tj.utj_val in
+      tj.utj_val, Constraint.union (Constraint.union cst1 cst2) cst3
+
+
+let translate_local_def env (b,topt) =
+  let (j,cst) = infer env b in
+  let (typ,cst) = constrain_type env j cst topt in
+    (j.uj_val,typ,cst)
+
+let translate_local_assum env t =
+  let (j,cst) = infer env t in
+  let t = Typeops.assumption_of_judgment env j in
+    (t,cst)
+
+(*
+
+(* Same as push_named, but check that the variable is not already
+   there. Should *not* be done in Environ because tactics add temporary
+   hypothesis many many times, and the check performed here would
+   cost too much. *)
+let safe_push_named (id,_,_ as d) env =
+  let _ =
+    try
+      let _ = lookup_named id env in 
+      error ("identifier "^string_of_id id^" already defined")
+    with Not_found -> () in
+  push_named d env
+
+let push_named_def = push_rel_or_named_def safe_push_named
+let push_rel_def = push_rel_or_named_def push_rel
+
+let push_rel_or_named_assum push (id,t) env =
+  let (j,cst) = safe_infer env t in
+  let t = Typeops.assumption_of_judgment env j in
+  let env' = add_constraints cst env in
+  let env'' = push (id,None,t) env' in
+  (cst,env'')
+
+let push_named_assum = push_rel_or_named_assum push_named
+let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env)
+
+let push_rels_with_univ vars env =
+  List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
+*)
+
+
+(* Insertion of constants and parameters in environment. *)
+
+let infer_declaration env dcl =
+  match dcl with
+  | DefinitionEntry c ->
+      let (j,cst) = infer env c.const_entry_body in
+      let (typ,cst) = constrain_type env j cst c.const_entry_type in
+      Some j.uj_val, typ, cst, c.const_entry_opaque
+  | ParameterEntry t ->
+      let (j,cst) = infer env t in
+      None, Typeops.assumption_of_judgment env j, cst, false
+
+let build_constant_declaration env (body,typ,cst,op) =
+  let ids = match body with 
+    | 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 in
+    { const_body = body;
+      const_type = typ;
+      const_hyps = hyps;
+      const_constraints = cst;
+      const_opaque = op }
+
+(*s Global and local constant declaration. *)
+
+let translate_constant env ce =
+  build_constant_declaration env (infer_declaration env ce)
+
+let translate_recipe env r = 
+  build_constant_declaration env (Cooking.cook_constant env r)
+
+(* Insertion of inductive types. *)
+
+let translate_mind env mie = check_inductive env mie 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
new file mode 100644
index 000000000..4fb104c02
--- /dev/null
+++ b/kernel/term_typing.mli
@@ -0,0 +1,34 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Term
+open Univ
+open Declarations
+open Inductive
+open Environ
+open Entries
+open Typeops
+(*i*)
+
+val translate_local_def : env -> constr * types option -> 
+  constr * types * Univ.constraints
+
+val translate_local_assum : env -> types ->
+  types * Univ.constraints
+
+val translate_constant : env -> constant_entry -> constant_body
+
+val translate_mind : 
+  env -> mutual_inductive_entry -> mutual_inductive_body
+
+val translate_recipe : 
+  env -> Cooking.recipe -> constant_body
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6da58adbc..29b09dde1 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -15,6 +15,7 @@ open Term
 open Declarations
 open Sign
 open Environ
+open Entries
 open Reduction
 open Inductive
 open Type_errors
@@ -242,8 +243,8 @@ let judge_of_cast env cj tj =
 let judge_of_inductive env i =
   let constr = mkInd i in
   let _ =
-    let (sp,_) = i in
-    let mib = lookup_mind sp env in
+    let (kn,_) = i in
+    let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
   make_judge constr (type_of_inductive env i)
 
@@ -258,8 +259,8 @@ let judge_of_inductive env i
 let judge_of_constructor env c =
   let constr = mkConstruct c in
   let _ =
-    let ((sp,_),_) = c in
-    let mib = lookup_mind sp env in
+    let ((kn,_),_) = c in
+    let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
   make_judge constr (type_of_constructor env c)
 
@@ -457,10 +458,6 @@ let infer_v env cv =
  
 (* Typing of several terms. *)
 
-type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
-
 let infer_local_decl env id = function
   | LocalDef c -> 
       let (j,cst) = infer env c in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 94d4e0844..55adf86a2 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -13,6 +13,7 @@ open Names
 open Univ
 open Term
 open Environ
+open Entries
 (*i*)
 
 (*s Typing functions (not yet tagged as safe) *)
@@ -21,10 +22,6 @@ val infer      : env -> constr       -> unsafe_judgment * constraints
 val infer_v    : env -> constr array -> unsafe_judgment array * constraints
 val infer_type : env -> types        -> unsafe_type_judgment * constraints
 
-type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
-
 val infer_local_decls :
   env -> (identifier * local_entry) list
     -> env * Sign.rel_context * constraints