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

10 files changed, 40 insertions, 30 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 899fb64e1c..9406a57d79 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -488,7 +488,7 @@ let check_and_adjust_constructor env ind cstrs = function
   | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
-      if Closure.mind_equiv env ind' ind then
+      if eq_ind ind' ind then
 	(* Check the constructor has the right number of args *)
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 35ffda0a1b..7ec77f7dca 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -156,7 +156,7 @@ let subst_cl_typ subst ct = match ct with
 	if kn' == kn then ct else
          fst (find_class_type (Global.env()) Evd.empty t)
   | CL_IND (kn,i) ->
-      let kn' = subst_kn subst kn in
+      let kn' = subst_ind subst kn in
 	if kn' == kn then ct else
 	  CL_IND (kn',i)
 
@@ -355,7 +355,7 @@ let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
 let cache_coercion o =
   load_coercion 1 o
 
-let subst_coercion (_,subst,(coe,stre,isid,cls,clt,ps as obj)) =
+let subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) =
   let coe' = subst_coe_typ subst coe in
   let cls' = subst_cl_typ subst cls in
   let clt' = subst_cl_typ subst clt in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f9c872f9ed..16520916cd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -70,7 +70,7 @@ module PrintingCasesMake =
     type t = inductive * int array
     let encode = Test.encode
     let subst subst ((kn,i), ints as obj) =
-      let kn' = subst_kn subst kn in
+      let kn' = subst_ind subst kn in
 	if kn' == kn then obj else
 	  (kn',i), ints
     let printer (ind,_) = pr_global_env Idset.empty (IndRef ind)
@@ -566,7 +566,7 @@ let rec subst_cases_pattern subst pat =
   match pat with
   | PatVar _ -> pat
   | PatCstr (loc,((kn,i),j),cpl,n) ->
-      let kn' = subst_kn subst kn
+      let kn' = subst_ind subst kn
       and cpl' = list_smartmap (subst_cases_pattern subst) cpl in
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
@@ -610,7 +610,7 @@ let rec subst_rawconstr subst raw =
         let (n,topt) = x in
         let topt' = Option.smartmap
           (fun (loc,(sp,i),x,y as t) ->
-            let sp' = subst_kn subst sp in
+            let sp' = subst_ind subst sp in
             if sp == sp' then t else (loc,(sp',i),x,y)) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = list_smartmap
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b6e697e4de..10f4db77aa 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -428,12 +428,12 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	         evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
 
 	| Ind sp1, Ind sp2 ->
-	    if sp1=sp2 then
+	    if eq_ind sp1 sp2 then
               ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
             else (evd, false)
 
 	| Construct sp1, Construct sp2 ->
-	    if sp1=sp2 then
+	    if eq_constructor sp1 sp2 then
               ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
             else (evd, false)
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index eed795cdcf..f134614cbc 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -574,15 +574,16 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 let lookup_eliminator ind_sp s =
   let kn,i = ind_sp in
-  let mp,dp,l = repr_kn kn in
+  let mp,dp,l = repr_mind kn in
   let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst = make_con mp dp (label_of_id id) in
+    let cst =Global.constant_of_delta
+      (make_con mp dp (label_of_id id)) in
     let _ = Global.lookup_constant cst in
-    mkConst cst
+      mkConst cst
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bfe1522f9c..1f196f43ef 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -471,5 +471,5 @@ let control_only_guard env c =
   iter env c
 
 let subst_inductive subst (kn,i as ind) =
-  let kn' = Mod_subst.subst_kn subst kn in
+  let kn' = Mod_subst.subst_ind subst kn in
   if kn == kn' then ind else (kn',i)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index be37e6531c..ec4a1260c5 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -101,7 +101,7 @@ let rec pattern_of_constr t =
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
     | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
-    | Const sp         -> PRef (ConstRef sp)
+    | Const sp         -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind sp        -> PRef (IndRef sp)
     | Construct sp -> PRef (ConstructRef sp)
     | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
@@ -212,8 +212,9 @@ let rec pat_of_raw metas vars = function
        with Not_found -> PVar id)
   | RPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
-  | RRef (_,r) ->
-      PRef r
+  | RRef (_,ConstRef con) ->
+      PRef (ConstRef (constant_of_kn(canonical_con con)))
+  | RRef (_,r) -> PRef r
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
   | RApp (_, RPatVar (_,(true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
@@ -295,5 +296,5 @@ and pat_of_raw_branch loc metas vars ind brs i =
 
 let pattern_of_rawconstr c =
   let metas = ref [] in
-  let p = pat_of_raw metas [] c in
+  let p = pat_of_raw metas [] c in	
   (!metas,p)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 057b263948..13f2aef261 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -52,8 +52,8 @@ let load_structure i (_,(ind,id,kl,projs)) =
 let cache_structure o =
   load_structure 1 o
 
-let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
-  let kn' = subst_kn subst kn in
+let subst_structure (subst,((kn,i),id,kl,projs as obj)) = 
+  let kn' = subst_ind subst kn in
   let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
@@ -136,7 +136,7 @@ let (in_method,out_method) =
     { (default_object "RECMETHODS") with
 	load_function = (fun _ -> load_method);
 	cache_function = load_method;
-	subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
+	subst_function = (fun (s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
 	classify_function = (fun x -> Substitute x)
     }
 
@@ -252,7 +252,7 @@ let open_canonical_structure i (_,o) =
 let cache_canonical_structure o =
   open_canonical_structure 1 o
 
-let subst_canonical_structure (_,subst,(cst,ind as obj)) =
+let subst_canonical_structure (subst,(cst,ind as obj)) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
   let cst' = fst (subst_con subst cst) in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f0a7ce4c81..3b6d13d471 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -65,9 +65,9 @@ let rec pr_constr c = match kind_of_term c with
       (str"Evar#" ++ int e ++ str"{" ++
        prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
   | Const c -> str"Cst(" ++ pr_con c ++ str")"
-  | Ind (sp,i) -> str"Ind(" ++ pr_path sp ++ str"," ++ int i ++ str")"
+  | Ind (sp,i) -> str"Ind(" ++ pr_mind sp ++ str"," ++ int i ++ str")"
   | Construct ((sp,i),j) ->
-      str"Constr(" ++ pr_path sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
+      str"Constr(" ++ pr_mind sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
   | Case (ci,p,c,bl) -> v 0
       (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
              pr_constr c ++ str"of") ++ cut() ++
@@ -729,7 +729,7 @@ let hdchar env c =
 	lowercase_first_char (id_of_label (con_label kn))
     | Ind ((kn,i) as x) ->
 	if i=0 then
-	  lowercase_first_char (id_of_label (label kn))
+	  lowercase_first_char (id_of_label (mind_label kn))
 	else
 	  lowercase_first_char (basename_of_global (IndRef x))
     | Construct ((sp,i) as x) ->
@@ -825,15 +825,22 @@ let names_of_rel_context env =
 
 (**** Globality of identifiers *)
 
-let rec is_imported_modpath = function
-  | MPfile dp -> true
-  | p -> false
+let rec is_imported_modpath mp = 
+  let current_mp,_ = Lib.current_prefix() in
+    match mp with
+      | MPfile dp ->
+	  let rec find_prefix = function
+	    |MPfile dp1 -> not (dp1=dp)
+	    |MPdot(mp,_) -> find_prefix mp
+	    |MPbound(_) -> false
+	  in find_prefix current_mp
+      | p -> false
 
 let is_imported_ref = function
   | VarRef _ -> false
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) ->
-      let (mp,_,_) = repr_kn kn in is_imported_modpath mp
+      let (mp,_,_) = repr_mind kn in is_imported_modpath mp
   | ConstRef kn ->
       let (mp,_,_) = repr_con kn in is_imported_modpath mp
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9d35225737..539821403d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -111,7 +111,7 @@ let load_class (_, cl) =
 
 let cache_class = load_class
 
-let subst_class (_,subst,cl) =
+let subst_class (subst,cl) =
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
@@ -187,8 +187,9 @@ let load_instance (_,inst) =
   instances := Gmap.add inst.is_class insts !instances
 
 let cache_instance = load_instance
-let subst_instance (_,subst,inst) =
-  { inst with
+
+let subst_instance (subst,inst) = 
+  { inst with 
       is_class = fst (subst_global subst inst.is_class);
       is_impl = fst (Mod_subst.subst_con subst inst.is_impl) }