This big commit addresses two problems:

  1- Management of the name-space in a modular development / sharing of non-logical objects.
  2- Performance of atomic module operations (adding a module to the environment, subtyping ...).

1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P

Module M := P.

Module M.
 Include P.
 ...
End M.

Declare Module K : S with Module M := P.

In this 3 cases we don't want to be bothered by the duplication of names. 
Of course, M.foo delta reduce to P.foo but many non-logical features of coq 
do not work modulo conversion (they use eq_constr or constr_pat object). 
To engender a transparent name-space (ie using P.foo or M.foo is the same thing) 
we quotient the name-space by the equivalence relation on names induced by the 
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of 
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo). 
So:
*************************************************************************************
*  Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values   *
*************************************************************************************

Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free 
(also for a posteriori declaration of them, ex: a notation on M.foo will be 
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.


2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based 
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate 
several functors then we have bigger vo.


Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...



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

13 files changed, 150 insertions, 129 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index e1edeec37..47381f6d8 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -203,7 +203,7 @@ let pop_visible, push_visible, get_visible, subst_mp =
   and push mp o =
     vis := { mp = mp; content = Hashtbl.create 97 } :: !vis;
     let s = List.hd !sub in
-    let s = match o with None -> s | Some msid -> add_msid msid mp s in
+    let s = match o with None -> s | Some msid -> add_mp msid mp empty_delta_resolver s in
     sub := s :: !sub
   and get () = !vis
   and subst mp = subst_mp (List.hd !sub) mp
@@ -278,7 +278,6 @@ let rec mp_renaming_fun mp = match mp with
       let lmp = mp_renaming mp in
       if lmp = [""] then (modfstlev_rename l)::lmp
       else (modular_rename Mod (id_of_label l))::lmp
-  | MPself msid -> [modular_rename Mod (id_of_msid msid)]
   | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)]
   | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
   | MPfile _ ->
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index c401bd059..a68e72d26 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -45,7 +45,7 @@ val pp_global : kind -> global_reference -> string
 val pp_module : module_path -> string
 
 val top_visible_mp : unit -> module_path
-val push_visible : module_path -> mod_self_id option -> unit
+val push_visible : module_path -> module_path option -> unit
 val pop_visible : unit -> unit
 
 val check_duplicate : module_path -> label -> string
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index ba4786d37..37721c9b9 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -32,7 +32,7 @@ let toplevel_env () =
 	let mp,_,l = repr_kn kn in
 	let seb = match Libobject.object_tag o with
 	  | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
-	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn)
+	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn))
 	  | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
 	  | "MODULE TYPE" ->
 	      SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
@@ -41,8 +41,8 @@ let toplevel_env () =
     | _ -> failwith "caught"
   in
   match current_toplevel () with
-    | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg))
-    | _ -> assert false
+    | _ -> SEBstruct (List.rev (map_succeed get_reference seg))
+ 
 
 let environment_until dir_opt =
   let rec parse = function
@@ -69,7 +69,7 @@ module type VISIT = sig
 
   (* Add kernel_name / constant / reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
-  val add_kn : kernel_name -> unit
+  val add_kn : mutual_inductive -> unit
   val add_con : constant -> unit
   val add_ref : global_reference -> unit
   val add_decl_deps : ml_decl -> unit
@@ -77,7 +77,7 @@ module type VISIT = sig
 
   (* Test functions:
      is a particular object a needed dependency for the current extraction ? *)
-  val needed_kn : kernel_name -> bool
+  val needed_kn : mutual_inductive -> bool
   val needed_con : constant -> bool
   val needed_mp : module_path -> bool
 end
@@ -87,17 +87,17 @@ module Visit : VISIT = struct
      (for inductives and modules names) and a Cset for constants
      (and still the remaining MPset) *)
   type must_visit =
-      { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t }
+      { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t }
   (* the imperative internal visit lists *)
-  let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty }
+  let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty }
   (* the accessor functions *)
-  let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
-  let needed_kn kn = KNset.mem kn v.kn
+  let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
+  let needed_kn kn = Mindset.mem kn v.kn
   let needed_con c = Cset.mem c v.con
   let needed_mp mp = MPset.mem mp v.mp
   let add_mp mp =
     check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
-  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
+  let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn)
   let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
   let add_ref = function
     | ConstRef c -> add_con c
@@ -140,29 +140,29 @@ let factor_fix env l cb msb =
     labels, recd, msb''
   end
 
-let build_mb expr typ_opt =
-  { mod_expr = Some expr;
+let build_mb mp expr typ_opt =
+  { mod_mp = mp;
+    mod_expr = Some expr;
     mod_type = typ_opt;
+    mod_type_alg = None;
     mod_constraints = Univ.Constraint.empty;
-    mod_alias = Mod_subst.empty_subst;
+    mod_delta = Mod_subst.empty_delta_resolver;
     mod_retroknowledge = [] }
 
 let my_type_of_mb env mb =
-  match mb.mod_type with
-    | Some mtb -> mtb
-    | None -> Modops.eval_struct env (Option.get mb.mod_expr)
+   mb.mod_type
 
 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
     To check with Elie. *)
 
-let env_for_mtb_with env mtb idl =
-  let msid,sig_b = match Modops.eval_struct env mtb with
-    | SEBstruct(msid,sig_b) -> msid,sig_b
+let env_for_mtb_with env mp mtb idl =
+  let sig_b = match mtb with
+    | SEBstruct(sig_b) -> sig_b
     | _ -> assert false
   in
   let l = label_of_id (List.hd idl) in
   let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in
-  Modops.add_signature (MPself msid) before env
+  Modops.add_signature mp before empty_delta_resolver env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to specifications. *)
@@ -177,20 +177,18 @@ let rec extract_sfb_spec env mp = function
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
       let kn = make_kn mp empty_dirpath l in
-      let s = Sind (kn, extract_inductive env kn) in
+      let mind = mind_of_kn kn in
+      let s = Sind (kn, extract_inductive env mind) in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmodule mb) :: msig ->
       let specs = extract_sfb_spec env mp msig in
-      let spec = extract_seb_spec env (my_type_of_mb env mb) in
+      let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb env mb) in
       (l,Smodule spec) :: specs
   | (l,SFBmodtype mtb) :: msig ->
       let specs = extract_sfb_spec env mp msig in
-      (l,Smodtype (extract_seb_spec env mtb.typ_expr)) :: specs
-  | (l,SFBalias (mp1,typ_opt,_)) :: msig ->
-      let mb = build_mb (SEBident mp1) typ_opt in
-      extract_sfb_spec env mp ((l,SFBmodule mb) :: msig)
+      (l,Smodtype (extract_seb_spec env mtb.typ_mp mtb.typ_expr)) :: specs
 
 (* From [struct_expr_body] to specifications *)
 
@@ -201,34 +199,35 @@ let rec extract_sfb_spec env mp = function
    For instance, [my_type_of_mb] ensures this invariant.
 *)
 
-and extract_seb_spec env = function
+and extract_seb_spec env mp1 = function
   | SEBident mp -> Visit.add_mp mp; MTident mp
   | SEBwith(mtb',With_definition_body(idl,cb))->
-      let env' = env_for_mtb_with env mtb' idl in
-      let mtb''= extract_seb_spec env mtb' in
+      let env' = env_for_mtb_with env  mp1 mtb' idl in
+      let mtb''= extract_seb_spec env mp1 mtb' in
       (match extract_with_type env' cb with (* cb peut contenir des kn  *)
 	 | None ->  mtb''
 	 | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ)))
-  | SEBwith(mtb',With_module_body(idl,mp,_,_))->
+  | SEBwith(mtb',With_module_body(idl,mp))->
       Visit.add_mp mp;
-      MTwith(extract_seb_spec env mtb',
+      MTwith(extract_seb_spec env mp1 mtb',
 	     ML_With_module(idl,mp))
 (* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre:
    | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_))
      when mbid = mbid2 -> extract_seb_spec env m
    (* faudrait alors ajouter un test de non-apparition de mbid dans mb *)
 *)
-  | SEBfunctor (mbid, mtb, mtb') ->
+ | SEBfunctor (mbid, mtb, mtb') ->
       let mp = MPbound mbid in
-      let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
-      MTfunsig (mbid, extract_seb_spec env mtb.typ_expr,
-		extract_seb_spec env' mtb')
-  | SEBstruct (msid, msig) ->
-      let mp = MPself msid in
-      let env' = Modops.add_signature mp msig env in
-      MTsig (msid, extract_sfb_spec env' mp msig)
-  | SEBapply _ as mtb ->
-      extract_seb_spec env (Modops.eval_struct env mtb)
+      let env' = Modops.add_module (Modops.module_body_of_type mp mtb) 
+	env in
+      MTfunsig (mbid, extract_seb_spec env mp mtb.typ_expr,
+		extract_seb_spec env' mp1 mtb')
+  | SEBstruct (msig) ->
+      let env' = Modops.add_signature mp1 msig empty_delta_resolver env in
+	MTsig (mp1, extract_sfb_spec env' mp1 msig)
+  | SEBapply _ ->
+      assert false
+
 
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
@@ -263,9 +262,10 @@ let rec extract_sfb env mp all = function
   | (l,SFBmind mib) :: msb ->
       let ms = extract_sfb env mp all msb in
       let kn = make_kn mp empty_dirpath l in
-      let b = Visit.needed_kn kn in
+      let mind = mind_of_kn kn in
+      let b = Visit.needed_kn mind in
       if all || b then
-	let d = Dind (kn, extract_inductive env kn) in
+	let d = Dind (kn, extract_inductive env mind) in
 	if (not b) && (logical_decl d) then ms
 	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
@@ -279,40 +279,34 @@ let rec extract_sfb env mp all = function
       let ms = extract_sfb env mp all msb in
       let mp = MPdot (mp,l) in
        if all || Visit.needed_mp mp then
-	(l,SEmodtype (extract_seb_spec env mtb.typ_expr)) :: ms
+	(l,SEmodtype (extract_seb_spec env mp mtb.typ_expr)) :: ms
       else ms
-  | (l,SFBalias (mp1,typ_opt,_)) :: msb ->
-      let mb = build_mb (SEBident mp1) typ_opt in
-      extract_sfb env mp all ((l,SFBmodule mb) :: msb)
 
 (* From [struct_expr_body] to implementations *)
 
-and extract_seb env mpo all = function
+and extract_seb env mp all = function
   | SEBident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
       Visit.add_mp mp; MEident mp
   | SEBapply (meb, meb',_) ->
-      MEapply (extract_seb env None true meb,
-	       extract_seb env None true meb')
+      MEapply (extract_seb env mp true meb,
+	       extract_seb env mp true meb')
   | SEBfunctor (mbid, mtb, meb) ->
-      let mp = MPbound mbid in
-      let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
-      MEfunctor (mbid, extract_seb_spec env mtb.typ_expr,
-		 extract_seb env' None true meb)
-  | SEBstruct (msid, msb) ->
-      let mp,msb = match mpo with
-	| None -> MPself msid, msb
-	| Some mp -> mp, Modops.subst_structure (map_msid msid mp) msb
-      in
-      let env' = Modops.add_signature mp msb env in
-      MEstruct (msid, extract_sfb env' mp all msb)
+      let mp1 = MPbound mbid in
+      let env' = Modops.add_module (Modops.module_body_of_type  mp1 mtb)
+	env  in
+      MEfunctor (mbid, extract_seb_spec env mp1 mtb.typ_expr,
+		 extract_seb env' mp true meb)
+  | SEBstruct (msb) ->
+      let env' = Modops.add_signature mp msb empty_delta_resolver env in
+      MEstruct (mp,extract_sfb env' mp all msb)
   | SEBwith (_,_) -> anomaly "Not available yet"
 
 and extract_module env mp all mb =
   (* [mb.mod_expr <> None ], since we look at modules from outside. *)
   (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
-  { ml_mod_expr = extract_seb env (Some mp) all (Option.get mb.mod_expr);
-    ml_mod_type = extract_seb_spec env (my_type_of_mb env mb) }
+  { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr);
+    ml_mod_type = extract_seb_spec env mp (my_type_of_mb env mb) }
 
 
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
@@ -324,7 +318,7 @@ let mono_environment refs mpl =
   let env = Global.env () in
   let l = List.rev (environment_until None) in
   List.rev_map
-    (fun (mp,m) -> mp, unpack (extract_seb env (Some mp) false m)) l
+    (fun (mp,m) -> mp, unpack (extract_seb env  mp false m)) l
 
 (**************************************)
 (*S Part II : Input/Output primitives *)
@@ -514,7 +508,7 @@ let extraction_library is_rec m =
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,meb) =
     if Visit.needed_mp mp
-    then (mp, unpack (extract_seb env (Some mp) true meb)) :: l
+    then (mp, unpack (extract_seb env mp true meb)) :: l
     else l
   in
   let struc = List.fold_left select [] l in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3468e8a36..d119dbe8e 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -310,7 +310,15 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
   with Not_found ->
     (* First, if this inductive is aliased via a Module, *)
     (* we process the original inductive. *)
-    Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
+    let equiv = 
+      if (canonical_mind kn) = (user_mind kn) then
+	NoEquiv
+      else
+	begin
+	  ignore (extract_ind env (mind_of_kn (canonical_mind kn)));
+	  Equiv (canonical_mind kn)
+	end
+    in
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in
@@ -333,13 +341,12 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ip_types = t })
 	mib.mind_packets
     in
+
     add_ind kn mib
       {ind_info = Standard;
        ind_nparams = npar;
        ind_packets = packets;
-       ind_equiv = match mib.mind_equiv with
-         | None -> NoEquiv
-	 | Some kn -> Equiv kn
+       ind_equiv = equiv
       };
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
@@ -388,7 +395,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
 	assert (List.length field_names = List.length typ);
 	let projs = ref Cset.empty in
-	let mp,d,_ = repr_kn kn in
+	let mp,d,_ = repr_mind kn in
 	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
 	  | (Name id)::l, typ::typs ->
@@ -424,9 +431,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     let i = {ind_info = ind_info;
 	     ind_nparams = npar;
 	     ind_packets = packets;
-	     ind_equiv = match mib.mind_equiv with
-	       | None -> NoEquiv
-	       | Some kn -> Equiv kn }
+	     ind_equiv = equiv }
     in
     add_ind kn mib i;
     i
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 2c534ea7b..6bcd24763 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -26,7 +26,7 @@ val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) op
 val extract_fixpoint :
   env -> constant array -> (constr, types) prec_declaration -> ml_decl
 
-val extract_inductive : env -> kernel_name -> ml_ind
+val extract_inductive : env -> mutual_inductive -> ml_ind
 
 (*s Is a [ml_decl] or a [ml_spec] logical ? *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 9d45c08b7..6973bb454 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -84,7 +84,7 @@ let rec pp_type par vl t =
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (r,l) ->
-	if r = IndRef (kn_sig,0) then
+	if r = IndRef (mind_of_kn kn_sig,0) then
 	  pp_type true vl (List.hd l)
 	else
 	  pp_par par
@@ -269,8 +269,8 @@ let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
 
 let pp_decl = function
   | Dind (kn,i) when i.ind_info = Singleton ->
-      pp_singleton kn i.ind_packets.(0) ++ fnl ()
-  | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
+      pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl ()
+  | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i)
   | Dtype (r, l, t) ->
       if is_inline_custom r then mt ()
       else
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 55231d766..91c60d205 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -128,7 +128,7 @@ type ml_specif =
 and ml_module_type =
   | MTident of module_path
   | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
-  | MTsig of mod_self_id * ml_module_sig
+  | MTsig of module_path * ml_module_sig
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
@@ -145,7 +145,7 @@ type ml_structure_elem =
 and ml_module_expr =
   | MEident of module_path
   | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr
-  | MEstruct of mod_self_id * ml_module_structure
+  | MEstruct of module_path * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
 and ml_module_structure = (label * ml_structure_elem) list
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 213df31e6..2e9fb8bf2 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -649,9 +649,9 @@ let generalizable_list =
   let datatypes = MPfile (dirpath_of_string "Coq.Init.Datatypes")
   and specif = MPfile (dirpath_of_string "Coq.Init.Specif")
   in
-  [ make_kn datatypes empty_dirpath (mk_label "bool");
-    make_kn specif empty_dirpath (mk_label "sumbool");
-    make_kn specif empty_dirpath (mk_label "sumor") ]
+  [ make_mind datatypes empty_dirpath (mk_label "bool");
+    make_mind specif empty_dirpath (mk_label "sumbool");
+    make_mind specif empty_dirpath (mk_label "sumor") ]
 
 let check_generalizable_case unsafe br =
   if not unsafe then
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 4b6b47ab9..9c5feac82 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -50,7 +50,7 @@ end
 
 (*s Utility functions over ML types without meta *)
 
-val type_mem_kn : kernel_name -> ml_type -> bool
+val type_mem_kn : mutual_inductive -> ml_type -> bool
 
 val type_maxvar : ml_type -> int
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 1b1a39770..9195b747e 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -21,11 +21,7 @@ open Mod_subst
 (*S Functions upon ML modules. *)
 
 let rec msid_of_mt = function
-  | MTident mp -> begin
-      match Modops.eval_struct (Global.env()) (SEBident mp) with
-	| SEBstruct(msid,_) -> MPself msid
-	| _ -> anomaly "Extraction:the With can't be applied to a funsig"
-    end
+  | MTident mp -> mp
   | MTwith(mt,_)-> msid_of_mt mt
   | _ -> anomaly "Extraction:the With operator isn't applied to a name"
 
@@ -101,25 +97,26 @@ let ind_iter_references do_term do_cons do_type kn ind =
     do_type (IndRef ip);
     if lang () = Ocaml then
       (match ind.ind_equiv with
-	 | Equiv kne -> do_type (IndRef (kne, snd ip));
+	 | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip));
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
   if lang () = Ocaml then record_iter_references do_term ind.ind_info;
-  Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
+    Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
 
 let decl_iter_references do_term do_cons do_type =
   let type_iter = type_iter_references do_type
   and ast_iter = ast_iter_references do_term do_cons do_type in
   function
-    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
+    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type 
+	(mind_of_kn kn) ind
     | Dtype (r,_,t) -> do_type r; type_iter t
     | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
     | Dfix(rv,c,t) ->
 	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
 
 let spec_iter_references do_term do_cons do_type = function
-  | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
+  | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type (mind_of_kn kn) ind
   | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot
   | Sval (r,t) -> do_term r; type_iter_references do_type t
 
@@ -190,7 +187,7 @@ let signature_of_structure s =
 (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
 
 let get_decl_in_structure r struc =
-  try
+  try 
     let base_mp,ll = labels_of_ref r in
     if not (at_toplevel base_mp) then error_not_visible r;
     let sel = List.assoc base_mp struc in
@@ -311,7 +308,7 @@ let reset_needed, add_needed, found_needed, is_needed =
    (fun r -> Refset.mem (base_r r) !needed))
 
 let declared_refs = function
-  | Dind (kn,_) -> [|IndRef (kn,0)|]
+  | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|]
   | Dtype (r,_,_) -> [|r|]
   | Dterm (r,_,_) -> [|r|]
   | Dfix (rv,_,_) -> rv
@@ -322,7 +319,7 @@ let declared_refs = function
 let compute_deps_decl = function
   | Dind (kn,ind) ->
       (* Todo Later : avoid dependencies when Extract Inductive *)
-      ind_iter_references add_needed add_needed add_needed kn ind
+      ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind
   | Dtype (r,ids,t) ->
       if not (is_custom r) then type_iter_references add_needed t
   | Dterm (r,u,t) ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 93fc2c2dc..107b5368f 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -122,7 +122,7 @@ let find_projections = function Record l -> l | _ -> raise NoRecord
 
 let kn_sig =
   let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
-  make_kn specif empty_dirpath (mk_label "sig")
+  make_mind specif empty_dirpath (mk_label "sig")
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
@@ -380,7 +380,7 @@ let pp_Dfix (rv,c,t) =
 let pp_equiv param_list name = function
   | NoEquiv, _ -> mt ()
   | Equiv kn, i ->
-      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i))
+      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i))
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
@@ -408,7 +408,7 @@ let pp_logical_ind packet =
   fnl ()
 
 let pp_singleton kn packet =
-  let name = pp_global Type (IndRef (kn,0)) in
+  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -416,7 +416,7 @@ let pp_singleton kn packet =
 		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn projs ip_equiv packet =
-  let name = pp_global Type (IndRef (kn,0)) in
+  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
   let projnames = List.map (pp_global Term) projs in
   let l = List.combine projnames packet.ip_types.(0) in
   let pl = rename_tvars keywords packet.ip_vars in
@@ -438,20 +438,20 @@ let pp_ind co kn ind =
   let init= ref (str "type ") in
   let names =
     Array.mapi (fun i p -> if p.ip_logical then mt () else
-		  pp_global Type (IndRef (kn,i)))
+		  pp_global Type (IndRef (mind_of_kn kn,i)))
       ind.ind_packets
   in
   let cnames =
     Array.mapi
       (fun i p -> if p.ip_logical then [||] else
-	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
+	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1)))
 	   p.ip_types)
       ind.ind_packets
   in
   let rec pp i =
     if i >= Array.length ind.ind_packets then mt ()
     else
-      let ip = (kn,i) in
+      let ip = (mind_of_kn kn,i) in
       let ip_equiv = ind.ind_equiv, i in
       let p = ind.ind_packets.(i) in
       if is_custom (IndRef ip) then pp (i+1)
@@ -601,12 +601,12 @@ and pp_module_type ol = function
       let name = pp_modname (MPbound mbid) in
       let def = pp_module_type None mt' in
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
-  | MTsig (msid, sign) ->
+  | MTsig (mp1, sign) ->
       let tvm = top_visible_mp () in
-      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+      let mp = match ol with None -> mp1 | Some l -> MPdot (tvm,l) in
       (* References in [sign] are in short form (relative to [msid]).
 	 In push_visible, [msid-->mp] is added to the current subst. *)
-      push_visible mp (Some msid);
+      push_visible mp (Some mp1);
       let l = map_succeed pp_specif sign in
       pop_visible ();
       str "sig " ++ fnl () ++
@@ -684,9 +684,9 @@ and pp_module_expr ol = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEapply (me, me') ->
       pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")"
-  | MEstruct (msid, sel) ->
+  | MEstruct (mp, sel) ->
       let tvm = top_visible_mp () in
-      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+      let mp = match ol with None -> mp | Some l -> MPdot (tvm,l) in
       (* No need to update the subst with [Some msid] below : names are
 	 already in long form (see [subst_structure] in [Extract_env]). *)
       push_visible mp None;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 9451188aa..043bf0fe7 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -31,13 +31,13 @@ let occur_kn_in_ref kn = function
 let modpath_of_r = function
   | ConstRef kn -> con_modpath kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> modpath kn
+  | ConstructRef ((kn,_),_) -> mind_modpath kn
   | VarRef _ -> assert false
 
 let label_of_r = function
   | ConstRef kn -> con_label kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> label kn
+  | ConstructRef ((kn,_),_) -> mind_label kn
   | VarRef _ -> assert false
 
 let rec base_mp = function
@@ -93,15 +93,34 @@ let rec parse_labels ll = function
 
 let labels_of_mp mp = parse_labels [] mp
 
+let rec parse_labels2 ll mp1 = function
+  | mp when mp1=mp -> mp,ll
+  | MPdot (mp,l) -> parse_labels (l::ll) mp
+  | mp -> mp,ll
+
 let labels_of_ref r =
- let mp,_,l =
+  let mp_top = fst(Lib.current_prefix()) in
+  let mp,_,l =
+    match r with
+	ConstRef con -> repr_con con
+      | IndRef (kn,_)
+      | ConstructRef ((kn,_),_) -> repr_mind kn
+      | VarRef _ -> assert false
+  in
+  parse_labels2 [l] mp_top mp
+
+
+
+
+let labels_of_ref2 r =
+ let mp1,_,l =
   match r with
      ConstRef con -> repr_con con
    | IndRef (kn,_)
-   | ConstructRef ((kn,_),_) -> repr_kn kn
+   | ConstructRef ((kn,_),_) -> repr_mind kn
    | VarRef _ -> assert false
- in
-  parse_labels [l] mp
+ in mp1,l
+
 
 let rec add_labels_mp mp = function
   | [] -> mp
@@ -127,10 +146,10 @@ let lookup_type kn = Cmap.find kn !types
 
 (*s Inductives table. *)
 
-let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
-let init_inductives () = inductives := KNmap.empty
-let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = KNmap.find kn !inductives
+let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t)
+let init_inductives () = inductives := Mindmap.empty
+let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives
+let lookup_ind kn = Mindmap.find kn !inductives
 
 (*s Recursors table. *)
 
@@ -138,7 +157,7 @@ let recursors = ref Cset.empty
 let init_recursors () = recursors := Cset.empty
 
 let add_recursors env kn =
-  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in
+  let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in
   let mib = Environ.lookup_mind kn env in
   Array.iter
     (fun mip ->
@@ -305,7 +324,13 @@ let error_record r =
 
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp -> if not (Library.library_is_loaded dp) then
-      err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+      let mp1 = (fst(Lib.current_prefix())) in
+      let rec find_prefix = function
+	|MPfile dp1 when dp=dp1 -> ()
+	|MPdot(mp,_) -> find_prefix mp
+	|MPbound(_) -> ()
+	| _ -> err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+      in find_prefix mp1 
   | _ -> ()
 
 let info_file f =
@@ -450,7 +475,7 @@ let (inline_extraction,_) =
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        classify_function = (fun o -> Substitute o);
        subst_function =
-        (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
+        (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
 
 let _ = declare_summary "Extraction Inline"
@@ -528,7 +553,7 @@ let (blacklist_extraction,_) =
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
        classify_function = (fun o -> Libobject.Keep o);
-       subst_function = (fun (_,_,x) -> x)
+       subst_function = (fun (_,x) -> x)
     }
 
 let _ = declare_summary "Extraction Blacklist"
@@ -585,7 +610,7 @@ let (in_customs,_) =
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
        classify_function = (fun o -> Substitute o);
        subst_function =
-        (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
+        (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
 
 let _ = declare_summary "ML extractions"
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 42ed6eef0..512ecca74 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -38,7 +38,7 @@ val info_file : string -> unit
 
 (*s utilities about [module_path] and [kernel_names] and [global_reference] *)
 
-val occur_kn_in_ref : kernel_name -> global_reference -> bool
+val occur_kn_in_ref : mutual_inductive -> global_reference -> bool
 val modpath_of_r : global_reference -> module_path
 val label_of_r : global_reference -> label
 val current_toplevel : unit -> module_path
@@ -56,6 +56,7 @@ val common_prefix_from_list : module_path -> module_path list -> module_path
 val add_labels_mp : module_path -> label list -> module_path
 val get_nth_label_mp : int -> module_path -> label
 val labels_of_ref : global_reference -> module_path * label list
+val labels_of_ref2 : global_reference -> module_path * label
 
 (*s Some table-related operations *)
 
@@ -65,10 +66,10 @@ val lookup_term : constant -> ml_decl
 val add_type : constant -> ml_schema -> unit
 val lookup_type : constant -> ml_schema
 
-val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit
-val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind
+val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit
+val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind
 
-val add_recursors : Environ.env -> kernel_name -> unit
+val add_recursors : Environ.env -> mutual_inductive -> unit
 val is_recursor : global_reference -> bool
 
 val add_projection : int -> constant -> unit