Modules dans COQ\!\!\!\!

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

17 files changed, 307 insertions, 108 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index fb8a6c8a4..bc3b1310a 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -12,6 +12,7 @@ open Util
 open Pp
 open Options
 open Names
+open Libnames
 open Nametab
 open Environ
 open Libobject
@@ -166,6 +167,29 @@ let lookup_pattern_path_between (s,t) =
 	 | Construct sp -> (sp, coe.coe_param)
 	 | _ -> raise Not_found) l
 
+
+let subst_cl_typ subst ct = match ct with
+    CL_SORT
+  | CL_FUN
+  | CL_SECVAR _ -> ct
+  | CL_CONST kn -> 
+      let kn' = subst_kn subst kn in 
+	if kn' == kn then ct else
+	  CL_CONST kn'
+  | CL_IND (kn,i) ->
+      let kn' = subst_kn subst kn in 
+	if kn' == kn then ct else
+	  CL_IND (kn',i)
+
+let subst_coe_typ = subst_global
+
+let subst_coe_info subst info = 
+  let jud = info.coe_value in
+  let val' = subst_mps subst (j_val jud) in
+  let type' = subst_mps subst (j_type jud) in
+    if val' == j_val jud && type' == j_type jud then info else
+      {info with coe_value = make_judge val' type'}
+
 (* library, summary *)
 
 (*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
@@ -173,12 +197,18 @@ let lookup_pattern_path_between (s,t) =
 
 let cache_class (_,x) = add_new_class x
 
+let subst_class (_,subst,(ct,ci as obj)) = 
+  let ct' = subst_cl_typ subst ct in
+    if ct' == ct then obj else
+      (ct',ci)
+
 let (inClass,outClass) =
-  declare_object ("CLASS",
-                  { load_function = cache_class;
-		    open_function = (fun _ -> ());
+  declare_object {(default_object "CLASS") with 
+		    load_function = (fun _ o -> cache_class o);
                     cache_function = cache_class;
-                    export_function = (function x -> Some x) })
+		    subst_function = subst_class;
+		    classify_function = (fun (_,x) -> Substitute x); 
+		    export_function = (function x -> Some x)  }
 
 let declare_class (cl,stre,p) = 
   Lib.add_anonymous_leaf (inClass ((cl,{ cl_strength = stre; cl_param = p })))
@@ -225,7 +255,7 @@ let inductive_class_of ind = fst (class_info (CL_IND ind))
 let class_args_of c = snd (decompose_app c)
 
 let strength_of_cl = function 
-  | CL_CONST sp -> constant_strength sp
+  | CL_CONST kn -> constant_strength (sp_of_global None (ConstRef kn))
   | CL_SECVAR sp -> variable_strength sp
   | _ -> NeverDischarge
 
@@ -233,11 +263,11 @@ let string_of_class = function
   | CL_FUN -> "FUNCLASS"
   | CL_SORT -> "SORTCLASS" 
   | CL_CONST sp ->
-      string_of_qualid (shortest_qualid_of_global (Global.env()) (ConstRef sp))
+      string_of_qualid (shortest_qualid_of_global None (ConstRef sp))
   | CL_IND sp ->
-      string_of_qualid (shortest_qualid_of_global (Global.env()) (IndRef sp))
+      string_of_qualid (shortest_qualid_of_global None (IndRef sp))
   | CL_SECVAR sp ->
-      string_of_qualid (shortest_qualid_of_global (Global.env()) (VarRef sp))
+      string_of_qualid (shortest_qualid_of_global None (VarRef sp))
 
 (* coercion_value : coe_index -> unsafe_judgment * bool *)
 
@@ -316,17 +346,27 @@ let cache_coercion (_,((coe,xf),cls,clt)) =
   let jf = add_new_coercion (coe,xf) in
   add_coercion_in_graph (jf,is,it)
 
+let subst_coercion (_,subst,((coe,xf),cls,clt as obj)) =
+  let coe' = subst_coe_typ subst coe in
+  let xf' = subst_coe_info subst xf in
+  let cls' = subst_cl_typ subst cls in
+  let clt' = subst_cl_typ subst clt in
+    if coe' == coe && xf' == xf && cls' == cls & clt' == clt then obj else
+      ((coe',xf'),cls',clt')
+      
+    
 (* val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ  ->
                     -> Libobject.object 
    val outCoercion : Libobject.object -> (coe_typ * coe_info_typ) 
                          * cl_typ * cl_typ *)
 
 let (inCoercion,outCoercion) =
-  declare_object ("COERCION",
-                  { load_function = cache_coercion;
-		    open_function = (fun _ -> ());
+  declare_object {(default_object "COERCION") with 
+		    load_function = (fun _ o -> cache_coercion o);
                     cache_function = cache_coercion;
-                    export_function = (function x -> Some x) })
+		    subst_function = subst_coercion;
+		    classify_function = (fun (_,x) -> Substitute x); 
+                    export_function = (function x -> Some x)  }
 
 let declare_coercion coef v stre ~isid ~src:cls ~target:clt ~params:ps =
   Lib.add_anonymous_leaf
@@ -353,14 +393,15 @@ let coercion_of_qualid qid =
   let coe = coe_of_reference ref in
   if not (coercion_exists coe) then
     errorlabstrm "try_add_coercion" 
-      (Nametab.pr_global_env (Global.env()) ref ++ str" is not a coercion");
+      (Nametab.pr_global_env None ref ++ str" is not a coercion");
   coe
 
 module CoercionPrinting =
   struct
     type t = coe_typ
     let encode = coercion_of_qualid
-    let printer x = pr_global_env (Global.env()) x
+    let subst = subst_coe_typ
+    let printer x = pr_global_env None x
     let key = Goptions.SecondaryTable ("Printing","Coercion")
     let title = "Explicitly printed coercions: "
     let member_message x b =
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index cd5f31db8..d37588d06 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Libnames
 open Nametab
 open Term
 open Evd
@@ -32,7 +33,7 @@ type cl_info_typ = {
   cl_param : int }
 
 (* This is the type of coercion kinds *)
-type coe_typ = global_reference
+type coe_typ = Libnames.global_reference
 
 (* This is the type of infos for declared coercions *)
 type coe_info_typ 
@@ -46,7 +47,7 @@ type coe_index
 (* This is the type of paths from a class to another *)
 type inheritance_path = coe_index list
 
-val coe_of_reference : global_reference -> coe_typ
+val coe_of_reference : Libnames.global_reference -> coe_typ
 
 (*s [declare_class] adds a class to the set of declared classes *)
 val declare_class : cl_typ * strength * int -> unit
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index faa5e9e46..748c72f4c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -23,6 +23,7 @@ open Impargs
 open Rawterm
 open Nameops
 open Termops
+open Libnames
 open Nametab
 
 (****************************************************************************)
@@ -66,7 +67,11 @@ module PrintingCasesMake =
   struct
     type t = inductive * int array
     let encode = Test.encode
-    let printer (ind,_) = pr_global_env (Global.env()) (IndRef ind)
+    let subst subst ((kn,i), ints as obj) =
+      let kn' = subst_kn subst kn in
+	if kn' == kn then obj else
+	  (kn',i), ints
+    let printer (ind,_) = pr_global_env None (IndRef ind)
     let key = Goptions.SecondaryTable ("Printing",Test.field)
     let title = Test.title
     let member_message x = Test.member_message (printer x)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index ef9db0c44..e0eecf703 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -11,10 +11,12 @@
 open Pp
 open Util
 open Names
+open Libnames
 open Nameops
 open Term
 open Termops
 open Declarations
+open Entries
 open Inductive
 open Inductiveops
 open Instantiate
@@ -500,13 +502,14 @@ let declare_one_elimination ind =
   let (mib,mip) = Global.lookup_inductive ind in 
   let mindstr = string_of_id mip.mind_typename in
   let declare na c t =
-    let sp = Declare.declare_constant (id_of_string na)
-      (ConstantEntry
+    let kn = Declare.declare_constant (id_of_string na)
+      (DefinitionEntry
         { const_entry_body = c;
           const_entry_type = t;
           const_entry_opaque = false }, 
        NeverDischarge) in
-    Options.if_verbose ppnl (str na ++ str " is defined"); sp
+    Options.if_verbose ppnl (str na ++ str " is defined"); 
+    kn
   in
   let env = Global.env () in
   let sigma = Evd.empty in
@@ -519,7 +522,7 @@ let declare_one_elimination ind =
    if List.mem InType kelim then
     let cte =
       declare (mindstr^type_suff) (make_elim (new_sort_in_family InType)) None
-    in let c = mkConst cte and t = constant_type (Global.env ()) cte
+    in let c = mkConst (snd cte) and t = constant_type (Global.env ()) (snd cte)
     in List.iter  
 	 (fun (sort,suff) -> 
             let (t',c') = instanciate_type_indrec_scheme (new_sort_in_family sort) npars c t
@@ -548,8 +551,32 @@ let declare_eliminations sp =
 (* Look up function for the default elimination constant *)
 
 let lookup_eliminator ind_sp s =
-  let env = Global.env() in
-  let path = sp_of_global env (IndRef ind_sp) in
+  let kn,i = ind_sp in
+  let mp,dp,l = repr_kn 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 *)
+  let ref = ConstRef (make_kn mp dp (label_of_id id)) in
+  try 
+    let _ = full_name ref in
+      constr_of_reference ref
+  with Not_found ->
+  (* Then try to get a user-defined eliminator in some other places *)
+  (* using short name (e.g. for "eq_rec") *)
+    try construct_reference None id
+    with Not_found ->
+      errorlabstrm "default_elim"
+	(str "Cannot find the elimination combinator " ++
+           pr_id id ++ spc () ++
+	   str "The elimination of the inductive definition " ++
+           pr_id id ++ spc () ++ str "on sort " ++ 
+           spc () ++ print_sort_family s ++
+	   str " is probably not allowed")
+
+
+(*  let env = Global.env() in
+  let path = sp_of_global None (IndRef ind_sp) in
   let dir, base = repr_path path in
   let id = add_suffix base (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
@@ -558,7 +585,7 @@ let lookup_eliminator ind_sp s =
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-    try construct_reference env id
+    try construct_reference None id
     with Not_found ->
       errorlabstrm "default_elim"
 	(str "Cannot find the elimination combinator " ++
@@ -567,3 +594,4 @@ let lookup_eliminator ind_sp s =
            pr_id base ++ spc () ++ str "on sort " ++ 
            spc () ++ print_sort_family s ++
 	   str " is probably not allowed")
+*)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 85d38ab4d..bde1f31bd 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -10,6 +10,7 @@
 
 open Util
 open Names
+open Libnames
 open Nameops
 open Term
 open Termops
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index cc36b260a..5ff667f90 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -13,6 +13,7 @@ open Names
 open Sign
 open Term
 open Environ
+open Libnames
 open Nametab
 (*i*)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b7d834d6f..91e0acd65 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -143,7 +143,7 @@ let error_unsolvable_implicit (loc,kind) =
 	str "Cannot infer a type of this anonymous abstraction"
     | ImplicitArg (c,n) ->
 	str "Cannot infer the " ++ pr_ord n ++
-	str " implicit argument of " ++ Nametab.pr_global_env (Global.env()) c
+	str " implicit argument of " ++ Nametab.pr_global_env None c
     | InternalHole ->
         str "Cannot infer a term for an internal placeholder"
   in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 9f39a1db9..0f376ae5e 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -13,6 +13,7 @@ open Util
 open Names
 open Sign
 open Term
+open Libnames
 open Nametab
 (*i*)
 
@@ -88,6 +89,91 @@ type rawconstr =
    - boolean in POldCase means it is recursive
 i*)
 
+let rec subst_pat subst pat = 
+  match pat with
+  | PatVar _ -> pat
+  | PatCstr (loc,((kn,i),j),cpl,n) -> 
+      let kn' = subst_kn subst kn 
+      and cpl' = list_smartmap (subst_pat subst) cpl in
+	if kn' == kn && cpl' == cpl then pat else
+	  PatCstr (loc,((kn',i),j),cpl',n)
+	
+let rec subst_raw subst raw = 
+  match raw with
+  | RRef (loc,ref) -> 
+      let ref' = subst_global subst ref in 
+	if ref' == ref then raw else
+	  RRef (loc,ref')
+
+  | RVar _ -> raw
+  | REvar _ -> raw
+  | RMeta _ -> raw
+
+  | RApp (loc,r,rl) -> 
+      let r' = subst_raw subst r 
+      and rl' = list_smartmap (subst_raw subst) rl in
+	if r' == r && rl' == rl then raw else
+	  RApp(loc,r',rl')
+
+  | RLambda (loc,n,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RLambda (loc,n,r1',r2')
+
+  | RProd (loc,n,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RProd (loc,n,r1',r2')
+
+  | RLetIn (loc,n,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RLetIn (loc,n,r1',r2')
+
+  | RCases (loc,cs,ro,rl,branches) -> 
+      let ro' = option_smartmap (subst_raw subst) ro 
+      and rl' = list_smartmap (subst_raw subst) rl
+      and branches' = list_smartmap 
+			(fun (loc,idl,cpl,r as branch) ->
+			   let cpl' = list_smartmap (subst_pat subst) cpl
+			   and r' = subst_raw subst r in
+			     if cpl' == cpl && r' == r then branch else
+			       (loc,idl,cpl',r'))
+			branches
+      in
+	if ro' == ro && rl' == rl && branches' == branches then raw else
+	  RCases (loc,cs,ro',rl',branches')
+
+  | ROldCase (loc,b,ro,r,ra) -> 
+      let ro' = option_smartmap (subst_raw subst) ro
+      and r' = subst_raw subst r 
+      and ra' = array_smartmap (subst_raw subst) ra in
+	if ro' == ro && r' == r && ra' == ra then raw else
+	  ROldCase (loc,b,ro',r',ra')
+
+  | RRec (loc,fix,ida,ra1,ra2) -> 
+      let ra1' = array_smartmap (subst_raw subst) ra1
+      and ra2' = array_smartmap (subst_raw subst) ra2 in
+	if ra1' == ra1 && ra2' == ra2 then raw else
+	  RRec (loc,fix,ida,ra1',ra2')
+
+  | RSort _ -> raw
+
+  | RHole (loc,ImplicitArg (ref,i)) ->
+      let ref' = subst_global subst ref in 
+	if ref' == ref then raw else
+	  RHole (loc,ImplicitArg (ref',i))
+  | RHole (loc, 
+	   (AbstractionType _ | QuestionMark | CasesType | InternalHole)) ->
+      raw
+
+  | RCast (loc,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RCast (loc,r1',r2')
+
+  | RDynamic _ -> raw
+
 let dummy_loc = (0,0)
 
 let loc_of_rawconstr = function
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d6543323e..e8b0726c9 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -12,6 +12,7 @@
 open Names
 open Sign
 open Term
+open Libnames
 open Nametab
 (*i*)
 
@@ -57,7 +58,7 @@ type 'ctxt reference =
   | REVar of int * 'ctxt
 
 type rawconstr = 
-  | RRef of loc * global_reference
+  | RRef of loc * Libnames.global_reference
   | RVar of loc * identifier
   | REvar of loc * existential_key
   | RMeta of loc * int
@@ -93,6 +94,8 @@ val loc_of_rawconstr : rawconstr -> loc
 val set_loc_of_rawconstr : loc -> rawconstr -> rawconstr
 val join_loc : loc -> loc -> loc
 
+val subst_raw : Names.substitution -> rawconstr -> rawconstr
+
 type 'a raw_red_flag = {
   rBeta : bool;
   rIota : bool;
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6617a7a9b..e2d4036f4 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -11,6 +11,7 @@
 open Util
 open Pp
 open Names
+open Libnames
 open Nametab
 open Term
 open Termops
@@ -44,14 +45,22 @@ let structure_table = (ref [] : (inductive * struc_typ) list ref)
 
 let cache_structure (_,x) = structure_table := x :: (!structure_table)
 
+let subst_structure (_,subst,((kn,i),struc as obj)) = 
+  let kn' = subst_kn subst kn in
+  let proj' = list_smartmap 
+		(option_smartmap (subst_kn subst)) 
+		struc.s_PROJ 
+  in
+    if proj' == struc.s_PROJ && kn' == kn then obj else
+      (kn',i),{struc with s_PROJ = proj'}
+
 let (inStruc,outStruc) =
-  declare_object
-    ("STRUCTURE", {
-       load_function = (fun _ -> ());
-       cache_function = cache_structure;
-       open_function = cache_structure;
-       export_function = (function x -> Some x)
-     })
+  declare_object {(default_object "STRUCTURE") with 
+                    cache_function = cache_structure;
+		    open_function = (fun i o -> if i=1 then cache_structure o);
+                    subst_function = subst_structure;
+		    classify_function = (fun (_,x) -> Substitute x);
+		    export_function = (function x -> Some x)  }
 
 let add_new_struc (s,c,n,l) = 
   Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
@@ -81,19 +90,42 @@ type obj_typ = {
   o_TPARAMS : constr list; (* dans l'ordre *)
   o_TCOMPS : constr list } (* dans l'ordre *)
 
+let subst_obj subst obj =
+  let o_DEF' = subst_mps subst obj.o_DEF in
+  let o_TABS' = list_smartmap (subst_mps subst) obj.o_TABS in    
+  let o_TPARAMS' = list_smartmap (subst_mps subst) obj.o_TPARAMS in 
+  let o_TCOMPS' = list_smartmap (subst_mps subst) obj.o_TCOMPS in 
+    if o_DEF' == obj.o_DEF
+      && o_TABS' == obj.o_TABS    
+      && o_TPARAMS' == obj.o_TPARAMS 
+      && o_TCOMPS' == obj.o_TCOMPS 
+    then 
+      obj
+    else
+      { o_DEF = o_DEF' ;
+	o_TABS = o_TABS' ;    
+	o_TPARAMS = o_TPARAMS' ; 
+	o_TCOMPS = o_TCOMPS' }
+
 let object_table =
   (ref [] : ((global_reference * global_reference) * obj_typ) list ref)
 
 let cache_object (_,x) = object_table := x :: (!object_table)
 
-let (inObjDef, outObjDef) =
-  declare_object
-    ("OBJDEF", {
-       load_function = (fun _ -> ());
-       open_function = cache_object;
-       cache_function = cache_object;
-       export_function = (function x -> Some x)
-     })
+let subst_object (_,subst,((r1,r2),o as obj)) = 
+  let r1' = subst_global subst r1 in
+  let r2' = subst_global subst r2 in
+  let o' = subst_obj subst o in
+    if r1' == r1 && r2' == r2 && o' == o then obj else
+      (r1',r2'),o'
+
+let (inObjDef,outObjDef) =
+  declare_object {(default_object "OBJDEF") with 
+		    open_function = (fun i o -> if i=1 then cache_object o);
+                    cache_function = cache_object;
+		    subst_function = subst_object;
+		    classify_function = (fun (_,x) -> Substitute x);
+                    export_function = (function x -> Some x) }
 
 let add_new_objdef (o,c,la,lp,l) =
   try 
@@ -104,14 +136,11 @@ let add_new_objdef (o,c,la,lp,l) =
 
 let cache_objdef1 (_,sp) = ()
 
-let (inObjDef1, outObjDef1) =
-  declare_object
-    ("OBJDEF1", {
-       load_function = (fun _ -> ());
-       open_function = cache_objdef1;
-       cache_function = cache_objdef1;
-       export_function = (function x -> Some x)
-     })
+let (inObjDef1,outObjDef1) =
+  declare_object {(default_object "OBJDEF1") with 
+		    open_function = (fun i o -> if i=1 then cache_objdef1 o);
+                    cache_function = cache_objdef1;
+                    export_function = (function x -> Some x) }
 
 let objdef_info o = List.assoc o !object_table
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index a3dd2f2a3..e5ffe4fd2 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -12,6 +12,7 @@
 open Names
 open Nametab
 open Term
+open Libnames
 open Classops
 open Libobject
 open Library
@@ -27,10 +28,10 @@ val compter : bool ref
 type struc_typ = {
   s_CONST : identifier; 
   s_PARAM : int;
-  s_PROJ : section_path option list }
+  s_PROJ : constant option list }
 
 val add_new_struc : 
-  inductive * identifier * int * section_path option list -> unit
+  inductive * identifier * int * constant option list -> unit
 
 (* [find_structure isp] returns the infos associated to inductive path
    [isp] if it corresponds to a structure, otherwise fails with [Not_found] *)
@@ -50,5 +51,5 @@ val add_new_objdef :
 
 val inStruc : inductive * struc_typ -> obj
 val outStruc : obj -> inductive * struc_typ
-val inObjDef1 : section_path -> obj
-val outObjDef1 : obj -> section_path
+val inObjDef1 : kernel_name -> obj
+val outObjDef1 : obj -> kernel_name
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index f13f31de0..dc5824dc7 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -11,6 +11,7 @@
 open Util
 open Pp
 open Names
+open Libnames
 open Rawterm
 open Libobject
 open Lib
@@ -18,51 +19,50 @@ open Nameops
 
 (* Syntactic definitions. *)
 
-let syntax_table = ref (Spmap.empty : rawconstr Spmap.t)
+let syntax_table = ref (KNmap.empty : rawconstr KNmap.t)
 
 let _ = Summary.declare_summary
 	  "SYNTAXCONSTANT"
 	  { Summary.freeze_function = (fun () -> !syntax_table);
 	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
-	    Summary.init_function = (fun () -> syntax_table := Spmap.empty);
+	    Summary.init_function = (fun () -> syntax_table := KNmap.empty);
 	    Summary.survive_section = false }
 
-let add_syntax_constant sp c =
-  syntax_table := Spmap.add sp c !syntax_table
+let add_syntax_constant kn c =
+  syntax_table := KNmap.add kn c !syntax_table
 
-let cache_syntax_constant (sp,c) =
+let cache_syntax_constant ((sp,kn),c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant sp c;
-  Nametab.push_syntactic_definition sp;
-  Nametab.push_short_name_syntactic_definition sp
+  add_syntax_constant kn c;
+  Nametab.push_syntactic_definition (Nametab.Until 1) sp kn
 
-let load_syntax_constant (sp,c) =
+let load_syntax_constant i ((sp,kn),c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant sp c;
-  Nametab.push_syntactic_definition sp
+  add_syntax_constant kn c;
+  Nametab.push_syntactic_definition (Nametab.Until i) sp kn
 
-let open_syntax_constant (sp,c) =
-  Nametab.push_short_name_syntactic_definition sp
+let open_syntax_constant i ((sp,kn),c) =
+  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
+
+let subst_syntax_constant ((sp,kn),subst,c) =
+  subst_raw subst c
+
+let classify_syntax_constant (_,c) = Substitute c
 
 let (in_syntax_constant, out_syntax_constant) =
-  let od = {
+  declare_object {(default_object "SYNTAXCONSTANT") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
     open_function = open_syntax_constant;
+    subst_function = subst_syntax_constant;
+    classify_function = classify_syntax_constant;
     export_function = (fun x -> Some x) } 
-  in
-  declare_object ("SYNTAXCONSTANT", od)
 
 let declare_syntactic_definition id c =
   let _ = add_leaf id (in_syntax_constant c) in ()
 
-let search_syntactic_definition sp = Spmap.find sp !syntax_table
-
-let locate_syntactic_definition qid =
-  match Nametab.extended_locate qid with
-    | Nametab.SyntacticDef sp -> sp
-    | _ -> raise Not_found
+let search_syntactic_definition kn = KNmap.find kn !syntax_table
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
index 1a884300c..a3e1cad25 100644
--- a/pretyping/syntax_def.mli
+++ b/pretyping/syntax_def.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Libnames
 open Rawterm
 (*i*)
 
@@ -17,8 +18,6 @@ open Rawterm
 
 val declare_syntactic_definition : identifier -> rawconstr -> unit
 
-val search_syntactic_definition : section_path -> rawconstr
-
-val locate_syntactic_definition : Nametab.qualid -> section_path
+val search_syntactic_definition : kernel_name -> rawconstr
 
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b42318a52..f2c185621 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -13,6 +13,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Libnames
 open Termops
 open Declarations
 open Inductive
@@ -32,7 +33,7 @@ let set_transparent_const sp =
   if cb.const_body <> None & cb.const_opaque then
     errorlabstrm "set_transparent_const"
       (str "Cannot make" ++ spc () ++ 
-         Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp) ++
+         Nametab.pr_global_env None (ConstRef sp) ++
          spc () ++ str "transparent because it was declared opaque.");
   Conv_oracle.set_transparent_const sp
 
@@ -48,10 +49,10 @@ let _ =
 
 let is_evaluable env ref =
   match ref with
-      EvalConstRef sp ->
-        let (ids,sps) = Conv_oracle.freeze() in
-        Sppred.mem sp sps &
-        let cb = Environ.lookup_constant sp env in
+      EvalConstRef kn ->
+        let (ids,kns) = Conv_oracle.freeze() in
+        KNpred.mem kn kns &
+        let cb = Environ.lookup_constant kn env in
         cb.const_body <> None & not cb.const_opaque
     | EvalVarRef id ->
         let (ids,sps) = Conv_oracle.freeze() in
@@ -195,8 +196,9 @@ let invert_name labs l na0 env sigma ref = function
 	let refi = match ref with
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
-	  | EvalConst sp ->
-	      Some (EvalConst (make_path (dirpath sp) id)) in
+	  | EvalConst kn ->
+	      let (mp,dp,_) = repr_kn kn in
+	      Some (EvalConst (make_kn mp dp (label_of_id id))) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -365,7 +367,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
   let subbodies = list_tabulate make_Fi nbodies in
   substl subbodies bodies.(bodynum)
 
-let reduce_mind_case_use_function sp env mia =
+let reduce_mind_case_use_function kn env mia =
   match kind_of_term mia.mconstr with 
     | Construct(ind_sp,i as cstr_sp) ->
 	let real_cargs = snd (list_chop mia.mci.ci_npar mia.mcargs) in
@@ -374,10 +376,11 @@ let reduce_mind_case_use_function sp env mia =
 	let build_fix_name i =
 	  match names.(i) with 
 	    | Name id ->
-		let sp = make_path (dirpath sp) id in
-		(match constant_opt_value env sp with
+		let (mp,dp,_) = repr_kn kn in
+		let kn = make_kn mp dp (label_of_id id) in
+		(match constant_opt_value env kn with
 		  | None -> None
-		  | Some _ -> Some (mkConst sp))
+		  | Some _ -> Some (mkConst kn))
 	    | Anonymous -> None in 
 	let cofix_def = contract_cofix_use_function build_fix_name cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
@@ -595,14 +598,14 @@ let nf env sigma c = strong whd_nf env sigma c
  * ol is the occurence list to find. *)
 let rec substlin env name n ol c =
   match kind_of_term c with
-    | Const const when EvalConstRef const = name ->
+    | Const kn when EvalConstRef kn = name ->
         if List.hd ol = n then
           try 
-	    (n+1, List.tl ol, constant_value env const)
+	    (n+1, List.tl ol, constant_value env kn)
           with
 	      NotEvaluableConst _ ->
 		errorlabstrm "substlin"
-		  (pr_sp const ++ str " is not a defined constant")
+		  (pr_kn kn ++ str " is not a defined constant")
         else 
 	  ((n+1), ol, c)
 
@@ -692,7 +695,7 @@ let rec substlin env name n ol c =
 
 let string_of_evaluable_ref = function
   | EvalVarRef id -> string_of_id id
-  | EvalConstRef sp -> string_of_path sp
+  | EvalConstRef kn -> string_of_kn kn
 
 let unfold env sigma name =
   if is_evaluable env name then
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 1d801c5a4..d41161efb 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -79,8 +79,8 @@ val reduction_of_redexp : red_expr -> reduction_function
 val declare_red_expr : string -> reduction_function -> unit
 
 (* Opaque and Transparent commands. *)
-val set_opaque_const      : section_path -> unit
-val set_transparent_const : section_path -> unit
+val set_opaque_const      : constant -> unit
+val set_transparent_const : constant -> unit
 
 val set_opaque_var      : identifier -> unit
 val set_transparent_var : identifier -> unit
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 7f77bcdba..05411c68d 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -15,6 +15,7 @@ open Nameops
 open Term
 open Sign
 open Environ
+open Libnames
 open Nametab
 
 let print_sort = function
@@ -27,15 +28,15 @@ let print_sort_family = function
   | InProp -> (str "Prop")
   | InType -> (str "Type")
 
-let current_module = ref empty_dirpath
+(*let current_module = ref empty_dirpath
 
-let set_module m = current_module := m
+let set_module m = current_module := m*)
 
 let new_univ = 
   let univ_gen = ref 0 in
   (fun sp ->
     incr univ_gen; 
-    Univ.make_univ (!current_module,!univ_gen))
+    Univ.make_univ (Lib.module_dp(),!univ_gen))
 
 let new_sort_in_family = function 
   | InProp -> mk_Prop
@@ -510,7 +511,7 @@ let first_char id =
 
 let lowercase_first_char id = String.lowercase (first_char id)
 
-let id_of_global env ref = basename (sp_of_global env ref)
+let id_of_global env ref = Nametab.id_of_global (Some (named_context env)) ref
 
 let sort_hdchar = function
   | Prop(_) -> "P"
@@ -524,12 +525,12 @@ let hdchar env c =
     | LetIn (_,_,_,c)    -> hdrec (k+1) c
     | Cast (c,_)         -> hdrec k c
     | App (f,l)         -> hdrec k f
-    | Const sp       ->
-	let c = lowercase_first_char (basename sp) in
+    | Const kn       ->
+	let c = lowercase_first_char (id_of_label (label kn)) in
 	if c = "?" then "y" else c
-    | Ind ((sp,i) as x) ->
+    | Ind ((kn,i) as x) ->
 	if i=0 then 
-	  lowercase_first_char (basename sp)
+	  lowercase_first_char (id_of_label (label kn))
 	else 
 	  lowercase_first_char (id_of_global env (IndRef x))
     | Construct ((sp,i) as x) ->
@@ -644,12 +645,12 @@ let occur_rel p env id =
 let occur_id env nenv id0 c =
   let rec occur n c = match kind_of_term c with
     | Var id when  id=id0 -> raise Occur
-    | Const sp when basename sp = id0 -> raise Occur
+    | Const kn when id_of_global env (ConstRef kn) = id0 -> raise Occur
     | Ind ind_sp
-	when basename (path_of_inductive env ind_sp) = id0 ->
+	when id_of_global env (IndRef ind_sp) = id0 ->
         raise Occur
     | Construct cstr_sp
-	when basename (path_of_constructor env cstr_sp) = id0 ->
+	when id_of_global env (ConstructRef cstr_sp) = id0 ->
         raise Occur
     | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
     | _ -> iter_constr_with_binders succ occur n c
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index ebcd93a34..431e69e7f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -16,7 +16,7 @@ open Sign
 open Environ
 
 (* Universes *)
-val set_module : Names.dir_path -> unit
+(*val set_module : Names.dir_path -> unit*)
 val new_univ : unit -> Univ.universe
 val new_sort_in_family : sorts_family -> sorts
 
@@ -104,7 +104,7 @@ val eta_eq_constr : constr -> constr -> bool
 (* finding "intuitive" names to hypotheses *)
 val first_char : identifier -> string
 val lowercase_first_char : identifier -> string
-val id_of_global : env -> Nametab.global_reference -> identifier
+(*val id_of_global : env -> Libnames.global_reference -> identifier*)
 val sort_hdchar : sorts -> string
 val hdchar : env -> types -> string
 val id_of_name_using_hdchar :