Monomorphization (library)

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

12 files changed, 296 insertions, 170 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index bd1292e7a..7d85b362a 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -60,12 +60,12 @@ let modcache = ref (MPmap.empty : structure_body MPmap.t)
 
 let rec search_mod_label lab = function
   | [] -> raise Not_found
-  | (l,SFBmodule mb) :: _ when l = lab -> mb
+  | (l, SFBmodule mb) :: _ when eq_label l lab -> mb
   | _ :: fields -> search_mod_label lab fields
 
 let rec search_cst_label lab = function
   | [] -> raise Not_found
-  | (l,SFBconst cb) :: _ when l = lab -> cb
+  | (l, SFBconst cb) :: _ when eq_label l lab -> cb
   | _ :: fields -> search_cst_label lab fields
 
 let rec lookup_module_in_impl mp =
@@ -91,7 +91,7 @@ and fields_of_mp mp =
   let mb = lookup_module_in_impl mp in
   let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in
   let subs =
-    if inner_mp = mp then subs
+    if mp_eq inner_mp mp then subs
     else add_mp inner_mp mp mb.mod_delta subs
   in
   Modops.subst_signature subs fields
@@ -114,7 +114,7 @@ and fields_of_mb subs mb args =
 
 and fields_of_seb subs mp0 seb args = match seb with
   | SEBstruct l ->
-    assert (args = []);
+    let () = assert (List.is_empty args) in
     l, mp0, subs
   | SEBident mp ->
     let mb = lookup_module_in_impl (subst_mp subs mp) in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index fef95bc61..4adf9d02d 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -155,7 +155,7 @@ let _ = Summary.declare_summary "MODULE-INFO"
 
 let mp_of_kn kn =
   let mp,sec,l = repr_kn kn in
-    if sec=empty_dirpath then
+    if dir_path_eq sec empty_dirpath then
       MPdot (mp,l)
     else
       anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
@@ -230,7 +230,9 @@ let build_subtypes interp_modtype mp args mtys =
 let compute_visibility exists what i dir dirinfo =
   if exists then
     if
-      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
+      try
+        let globref = Nametab.locate_dir (qualid_of_dirpath dir) in
+        eq_global_dir_reference globref dirinfo
       with Not_found -> false
     then
       Nametab.Exactly i
@@ -316,7 +318,7 @@ let load_keep i ((sp,kn),seg) =
     begin
       try
 	let prefix',objects = MPmap.find mp !modtab_objects in
-	  if prefix' <> prefix then
+	  if not (eq_op prefix' prefix) then
 	    anomaly "Two different modules with the same path!";
 	  modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects;
       with
@@ -366,7 +368,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
       | None ->
 	  anomaly "You must not recache interactive module types!"
       | Some (mte,inl) ->
-	  if mp <> Global.add_modtype (basename sp) mte inl then
+	  if not (mp_eq mp (Global.add_modtype (basename sp) mte inl)) then
 	    anomaly "Kernel and Library names do not match"
   in
 
@@ -384,7 +386,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
 
 
 let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
-  assert (entry = None);
+  assert (Option.is_empty entry);
 
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
@@ -396,10 +398,12 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
 
 
 let open_modtype i ((sp,kn),(entry,_,_)) =
-  assert (entry = None);
+  assert (Option.is_empty entry);
 
   if
-    try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn)
+    try
+      let mp = Nametab.locate_modtype (qualid_of_path sp) in
+      not (mp_eq mp (mp_of_kn kn))
     with Not_found -> true
   then
     errorlabstrm ("open_modtype")
@@ -408,7 +412,7 @@ let open_modtype i ((sp,kn),(entry,_,_)) =
   Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
 
 let subst_modtype (subst,(entry,(mbids,mp,objs),_)) =
-  assert (entry = None);
+  assert (Option.is_empty entry);
   (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[])
 
 let classify_modtype (_,substobjs,_) =
@@ -428,17 +432,18 @@ let in_modtype : modtype_obj -> obj =
       classify_function = classify_modtype }
 
 let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
-  if mbids<>[] then anomaly "Unexpected functor objects";
+  let () = match mbids with
+  | [] -> () | _ -> anomaly "Unexpected functor objects" in
   let rec replace_idl = function
     | _,[] -> []
-    | id::idl,(id',obj)::tail when id = id' ->
-      if object_tag obj <> "MODULE" then anomaly "MODULE expected!";
-      let substobjs =
-	if idl = [] then
-	  let mp' = MPdot(mp, label_of_id id) in
-	  mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs
-	else
-	  replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp
+    | id::idl,(id',obj)::tail when id_eq id id' ->
+      if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!";
+      let substobjs = match idl with
+      | [] ->
+        let mp' = MPdot(mp, label_of_id id) in
+        mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs
+      | _ ->
+        replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp
       in
       (id, in_module substobjs)::tail
     | idl,lobj::tail -> lobj::replace_idl (idl,tail)
@@ -611,16 +616,17 @@ let end_module () =
   in
   let node = in_module substobjs in
   let objects =
-    if keep = [] || mbids <> [] then
+    match keep, mbids with
+    | [], _ | _, _ :: _ ->
       special@[node]   (* no keep objects or we are defining a functor *)
-    else
+    | _ ->
       special@[node;in_modkeep keep]   (* otherwise *)
   in
   let newoname = Lib.add_leaves id objects in
 
-    if (fst newoname) <> (fst oldoname) then
+    if not (eq_full_path (fst newoname) (fst oldoname)) then
       anomaly "Names generated on start_ and end_module do not match";
-    if mp_of_kn (snd newoname) <> mp then
+    if not (mp_eq (mp_of_kn (snd newoname)) mp) then
       anomaly "Kernel and Library names do not match";
 
     Lib.add_frozen_state () (* to prevent recaching *);
@@ -652,7 +658,7 @@ let register_library dir cenv objs digest =
     (* if it's in the environment, the cached objects should be correct *)
     Dirmap.find dir !library_cache
   with Not_found ->
-    if mp <> Global.import cenv digest then
+    if not (mp_eq mp (Global.import cenv digest)) then
       anomaly "Unexpected disk module name";
     let mp,substitute,keep = objs in
     let substobjs = [], mp, substitute in
@@ -703,7 +709,7 @@ let subst_import (subst,(export,mp as obj)) =
 let in_import =
   declare_object {(default_object "IMPORT MODULE") with
 		    cache_function = cache_import;
-		    open_function = (fun i o -> if i=1 then cache_import o);
+		    open_function = (fun i o -> if Int.equal i 1 then cache_import o);
 		    subst_function = subst_import;
 		    classify_function = classify_import }
 
@@ -735,10 +741,10 @@ let end_modtype () =
   check_subtypes_mt mp sub_mty_l;
   let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs,[])])
   in
-  if fst oname <> fst oldoname then
+  if not (eq_full_path (fst oname) (fst oldoname)) then
     anomaly
       "Section paths generated on start_ and end_modtype do not match";
-  if (mp_of_kn (snd oname)) <> mp then
+  if not (mp_eq (mp_of_kn (snd oname)) mp) then
     anomaly
       "Kernel and Library names do not match";
 
@@ -833,10 +839,13 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   (* and declare the module as a whole *)
   Summary.unfreeze_summaries fs;
   let mp = mp_of_kn (Lib.make_kn id) in
-  let inl = if inl_expr = None then None else inl_res in (*PLTODO *)
+  let inl = match inl_expr with
+  | None -> None
+  | _ -> inl_res
+  in (* PLTODO *)
   let mp_env,resolver = Global.add_module id entry inl in
 
-  if mp_env <> mp then anomaly "Kernel and Library names do not match";
+  if not (mp_eq mp_env mp) then anomaly "Kernel and Library names do not match";
 
   
   check_subtypes mp subs;
@@ -965,7 +974,7 @@ let declare_one_include_inner annot (me,is_mod) =
     else
       get_modtype_substobjs env mp1 inl me in
   let (mbids,mp,objs) =
-    if mbids <> [] then
+    if not (List.is_empty mbids) then
       get_includeself_substobjs env (mbids,mp,objs) me is_mod inl
     else
       (mbids,mp,objs) in
diff --git a/library/globnames.ml b/library/globnames.ml
index 8d298bc94..81cb241c9 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -27,9 +27,10 @@ let isConstructRef = function ConstructRef _ -> true | _ -> false
 let eq_gr gr1 gr2 =
   match gr1,gr2 with
     | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
-    | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
-    | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
-    | _,_ -> gr1=gr2
+    | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
+    | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
+    | VarRef v1, VarRef v2 -> id_eq v1 v2
+    | _ -> false
 
 let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
 let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
@@ -77,15 +78,16 @@ let reference_of_constr = global_of_constr
 
 let global_ord_gen fc fmi x y =
   let ind_ord (indx,ix) (indy,iy) =
-    let c = Pervasives.compare ix iy in
-    if c = 0 then kn_ord (fmi indx) (fmi indy) else c
+    let c = Int.compare ix iy in
+    if Int.equal c 0 then kn_ord (fmi indx) (fmi indy) else c
   in
   match x, y with
     | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
     | IndRef indx, IndRef indy -> ind_ord indx indy
     | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
-      let c = Pervasives.compare jx jy in
-      if c = 0 then ind_ord indx indy else c
+      let c = Int.compare jx jy in
+      if Int.equal c 0 then ind_ord indx indy else c
+    | VarRef v1, VarRef v2 -> id_ord v1 v2
     | _, _ -> Pervasives.compare x y
 
 let global_ord_can = global_ord_gen canonical_con canonical_mind
diff --git a/library/goptions.ml b/library/goptions.ml
index 2a97f6149..460b153de 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -82,7 +82,7 @@ module MakeTable =
         let cache_options (_,(f,p)) = match f with
           | GOadd -> t := MySet.add p !t
           | GOrmv -> t := MySet.remove p !t in
-        let load_options i o = if i=1 then cache_options o in
+        let load_options i o = if Int.equal i 1 then cache_options o in
 	let subst_options (subst,(f,p as obj)) = 
 	  let p' = A.subst subst p in
 	    if p' == p then obj else
diff --git a/library/heads.ml b/library/heads.ml
index f3bcba770..0d3ed0fdb 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -87,8 +87,13 @@ let kind_of_head env t =
       if b then NotImmediatelyComputableHead else ConstructorHead
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
   | Cast (c,_,_) -> aux k l c b
-  | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b
-  | Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b
+  | Lambda (_,_,c) ->
+    begin match l with
+    | [] ->
+      let () = assert (not b) in
+      aux (k + 1) [] c b
+    | h :: l -> aux (k + 1) l (subst1 h c) b
+    end
   | LetIn _ -> assert false
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
   | App (c,al) -> aux k (Array.to_list al @ l) c b
diff --git a/library/impargs.ml b/library/impargs.ml
index 767e0e73a..8df8420c8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -82,7 +82,8 @@ let with_implicits flags f x =
 
 let set_maximality imps b =
   (* Force maximal insertion on ending implicits (compatibility) *)
-  b || List.for_all ((<>) None) imps
+  let is_set x = match x with None -> false | _ -> true in
+  b || List.for_all is_set imps
 
 (*s Computation of implicit arguments *)
 
@@ -113,6 +114,11 @@ type argument_position =
   | Conclusion
   | Hyp of int
 
+let argument_position_eq p1 p2 = match p1, p2 with
+| Conclusion, Conclusion -> true
+| Hyp h1, Hyp h2 -> Int.equal h1 h2
+| _ -> false
+
 type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
@@ -132,10 +138,10 @@ let update pos rig (na,st) =
       | Some (DepRigid n as x) ->
           if argument_less (pos,n) then DepRigid pos else x
       | Some (DepFlexAndRigid (fpos,rpos) as x) ->
-          if argument_less (pos,fpos) or pos=fpos then DepRigid pos else
+          if argument_less (pos,fpos) || argument_position_eq pos fpos then DepRigid pos else
           if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x
       | Some (DepFlex fpos) ->
-          if argument_less (pos,fpos) or pos=fpos then DepRigid pos
+          if argument_less (pos,fpos) || argument_position_eq pos fpos then DepRigid pos
           else DepFlexAndRigid (fpos,pos)
       | Some Manual -> assert false
   else
@@ -160,7 +166,8 @@ let is_flexible_reference env bound depth f =
         let cb = Environ.lookup_constant kn env in
 	(match cb.const_body with Def _ -> true | _ -> false)
     | Var id ->
-        let (_,value,_) = Environ.lookup_named id env in value <> None
+        let (_, value, _) = Environ.lookup_named id env in
+        begin match value with None -> false | _ -> true end
     | Ind _ | Construct _ -> false
     |  _ -> true
 
@@ -311,7 +318,7 @@ let set_implicit id imp insmax =
   (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
 let rec assoc_by_pos k = function
-    (ExplByPos (k', x), b) :: tl when k = k' -> (x,b), tl
+    (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl
   | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
   | [] -> raise Not_found
 
@@ -352,7 +359,11 @@ let set_manual_implicits env flags enriching autoimps l =
 	  let (id, (b, fi, fo)), l' = assoc_by_pos k l in
 	    l', (Some Manual), (Some (b,fi))
 	with Not_found ->
-	  l,imp, if enriching && imp <> None then Some (flags.maximal,true) else None
+          let m = match enriching, imp with
+          | true, Some _ -> Some (flags.maximal, true)
+          | _ -> None
+          in
+          l, imp, m
       in
       let imps' = merge (k+1) l' imps in
       let m = Option.map (fun (b,f) -> set_maximality imps' b, f) m in
@@ -360,7 +371,7 @@ let set_manual_implicits env flags enriching autoimps l =
   | (Anonymous,imp)::imps ->
       let l', forced = try_forced k l in
 	forced :: merge (k+1) l' imps
-  | [] when l = [] -> []
+  | [] when begin match l with [] -> true | _ -> false end -> []
   | [] ->
       check_correct_manual_implicits autoimps l;
       []
@@ -483,10 +494,15 @@ let subst_implicits (subst,(req,l)) =
   (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
-  List.rev_map
-    (fun (id,impl,_,_) ->
-      if impl = Implicit then Some (id, Manual, (true,true)) else None)
-    (List.filter (fun (_,_,b,_) -> b = None) ctx)
+  let map (id, impl, _, _) = match impl with
+  | Implicit -> Some (id, Manual, (true, true))
+  | _ -> None
+  in
+  let is_set (_, _, b, _) = match b with
+  | None -> true
+  | Some _ -> false
+  in
+  List.rev_map map (List.filter is_set ctx)
 
 let section_segment_of_reference = function
   | ConstRef con -> section_segment_of_constant con
@@ -566,8 +582,9 @@ let rebuild_implicits (req,l) =
 	  else
 	    [ref,oldimpls]
 
-let classify_implicits (req,_ as obj) =
-  if req = ImplLocal then Dispose else Substitute obj
+let classify_implicits (req,_ as obj) = match req with
+| ImplLocal -> Dispose
+| _ -> Substitute obj
 
 type implicits_obj =
     implicit_discharge_request *
@@ -659,8 +676,9 @@ let declare_manual_implicits local ref ?enriching l =
     add_anonymous_leaf (inImplicits (req,[ref,l']))
 
 let maybe_declare_manual_implicits local ref ?enriching l =
-  if l = [] then ()
-  else declare_manual_implicits local ref ?enriching [l]
+  match l with
+  | [] -> ()
+  | _ -> declare_manual_implicits local ref ?enriching [l]
 
 let extract_impargs_data impls =
   let rec aux p = function
@@ -678,7 +696,7 @@ let lift_implicits n =
 let make_implicits_list l = [DefaultImpArgs, l]
 
 let rec drop_first_implicits p l =
-  if p = 0 then l else match l with
+  if Int.equal p 0 then l else match l with
   | _,[] as x -> x
   | DefaultImpArgs,imp::impls ->
       drop_first_implicits (p-1) (DefaultImpArgs,impls)
diff --git a/library/lib.ml b/library/lib.ml
index 212e23578..2653b8418 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -189,16 +189,23 @@ let split_lib_gen test =
       | None -> error "no such entry"
       | Some r -> r
 
-let split_lib sp = split_lib_gen (fun x -> fst x = sp)
+let eq_object_name (fp1, kn1) (fp2, kn2) =
+  eq_full_path fp1 fp2 && Int.equal (Names.kn_ord kn1 kn2) 0
+
+let split_lib sp =
+  let is_sp (nsp, _) = eq_object_name sp nsp in
+  split_lib_gen is_sp
 
 let split_lib_at_opening sp =
-  let is_sp = function
-    | x,(OpenedSection _|OpenedModule _|CompilingLibrary _) -> x = sp
+  let is_sp (nsp, obj) = match obj with
+    | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
+      eq_object_name nsp sp
     | _ -> false
   in
-  let a,s,b = split_lib_gen is_sp in
-  assert (List.tl s = []);
-  (a,List.hd s,b)
+  let a, s, b = split_lib_gen is_sp in
+  match s with
+  | [obj] -> (a, obj, b)
+  | _ -> assert false
 
 (* Adding operations. *)
 
@@ -216,7 +223,8 @@ let add_anonymous_entry node =
   name
 
 let add_leaf id obj =
-  if fst (current_prefix ()) = Names.initial_path then
+  let (path, _) = current_prefix () in
+  if Names.mp_eq path Names.initial_path then
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -292,7 +300,7 @@ let end_mod is_type =
   let oname,fs =
     try match find_entry_p is_opening_node with
       | oname,OpenedModule (ty,_,_,fs) ->
-	if ty = is_type then oname,fs
+	if Pervasives.(=) ty is_type then oname, fs
 	else error_still_opened (module_kind ty) oname
       | oname,OpenedSection _ -> error_still_opened "section" oname
       | _ -> assert false
@@ -318,9 +326,9 @@ let contents_after = function
 
 (* TODO: use check_for_module ? *)
 let start_compilation s mp =
-  if !comp_name <> None then
+  if !comp_name != None then
     error "compilation unit is already started";
-  if snd (snd (!path_prefix)) <> Names.empty_dirpath then
+  if not (Names.dir_path_eq (snd (snd (!path_prefix))) Names.empty_dirpath) then
     error "some sections are already opened";
   let prefix = s, (mp, Names.empty_dirpath) in
   let _ = add_anonymous_entry (CompilingLibrary prefix) in
@@ -348,7 +356,7 @@ let end_compilation dir =
     match !comp_name with
       | None -> anomaly "There should be a module name..."
       | Some m ->
-	  if m <> dir then anomaly
+	  if not (Names.dir_path_eq m dir) then anomaly
 	    ("The current open module has name "^ (Names.string_of_dirpath m) ^
 	       " and not " ^ (Names.string_of_dirpath m));
   in
@@ -379,7 +387,7 @@ let find_opening_node id =
   try
     let oname,entry = find_entry_p is_opening_node in
     let id' = basename (fst oname) in
-    if id <> id' then
+    if not (Names.id_eq id id') then
       error ("Last block to end has name "^(Names.string_of_id id')^".");
     entry
   with Not_found -> error "There is nothing to end."
@@ -412,7 +420,8 @@ let add_section_variable id impl =
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
+    | ((id,impl)::idl,(id',b,t)::hyps) when Names.id_eq id id' ->
+      (id',impl,b,t) :: aux (idl,hyps)
     | (id::idl,hyps) -> aux (idl,hyps)
     | [], _ -> []
   in aux (secs,ohyps)
@@ -574,14 +583,15 @@ let mark_end_of_command, current_command_label, reset_command_label =
   let n = ref (first_command_label-1) in
   (fun () ->
     match !lib_stk with
-        (_,Leaf o)::_ when object_tag o = "DOT" -> ()
+        (_,Leaf o)::_ when String.equal (object_tag o) "DOT" -> ()
       | _ -> incr n;add_anonymous_leaf (inLabel !n)),
   (fun () -> !n),
   (fun x -> n:=x;add_anonymous_leaf (inLabel x))
 
 let is_label_n n x =
   match x with
-    | (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true
+    | (sp, Leaf o) when String.equal (object_tag o) "DOT" &&
+      Int.equal n (outLabel o) -> true
     | _ -> false
 
 (** Reset the label registered by [mark_end_of_command()] with number n,
@@ -599,8 +609,11 @@ let reset_label n =
 let label_before_name (loc,id) =
   let found = ref false in
   let search = function
-    | (_,Leaf o) when !found && object_tag o = "DOT" -> true
-    | (sp,_) -> (if id = snd (repr_path (fst sp)) then found := true); false
+    | (_, Leaf o) when !found && String.equal (object_tag o) "DOT" -> true
+    | ((fp, _),_) ->
+      let (_, name) = repr_path fp in
+      let () = if Names.id_eq id name then found := true in
+      false
   in
   match find_entry_p search with
     | (_,Leaf o) -> outLabel o
@@ -690,11 +703,13 @@ let pop_con con =
 
 let con_defined_in_sec kn =
   let _,dir,_ = Names.repr_con kn in
-  dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+  not (Names.dir_path_eq dir Names.empty_dirpath) &&
+  Names.dir_path_eq (fst (split_dirpath dir)) (snd (current_prefix ()))
 
 let defined_in_sec kn =
   let _,dir,_ = Names.repr_mind kn in
-  dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+  not (Names.dir_path_eq dir Names.empty_dirpath) &&
+  Names.dir_path_eq (fst (split_dirpath dir)) (snd (current_prefix ()))
 
 let discharge_global = function
   | ConstRef kn when con_defined_in_sec kn ->
diff --git a/library/libnames.ml b/library/libnames.ml
index e51e2c81c..a0eff296c 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -82,6 +82,10 @@ type full_path = {
   dirpath : dir_path ;
   basename : identifier }
 
+let eq_full_path p1 p2 =
+  id_eq p1.basename p2.basename &&
+  Int.equal (dir_path_ord p1.dirpath p2.dirpath) 0
+
 let make_path pa id = { dirpath = pa; basename = id }
 
 let repr_path { dirpath = pa; basename = id } = (pa,id)
@@ -130,6 +134,8 @@ type qualid = full_path
 let make_qualid = make_path
 let repr_qualid = repr_path
 
+let qualid_eq = eq_full_path
+
 let string_of_qualid = string_of_path
 let pr_qualid = pr_path
 
@@ -157,6 +163,19 @@ type global_dir_reference =
   | DirClosedSection of dir_path
       (* this won't last long I hope! *)
 
+let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
+  Int.equal (dir_path_ord d1 d2) 0 &&
+  Int.equal (dir_path_ord p1 p2) 0 &&
+  mp_eq mp1 mp2
+
+let eq_global_dir_reference r1 r2 = match r1, r2 with
+| DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
+| DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
+| DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
+| DirModule op1, DirModule op2 -> eq_op op1 op2
+| DirClosedSection dp1, DirClosedSection dp2 -> Int.equal (dir_path_ord dp1 dp2) 0
+| _ -> false
+
 type reference =
   | Qualid of qualid Loc.located
   | Ident of identifier Loc.located
@@ -177,6 +196,11 @@ let loc_of_reference = function
   | Qualid (loc,qid) -> loc
   | Ident (loc,id) -> loc
 
+let eq_reference r1 r2 = match r1, r2 with
+| Qualid (_, q1), Qualid (_, q2) -> qualid_eq q1 q2
+| Ident (_, id1), Ident (_, id2) -> id_eq id1 id2
+| _ -> false
+
 (* Deprecated synonyms *)
 
 let make_short_qualid = qualid_of_ident
diff --git a/library/libnames.mli b/library/libnames.mli
index b83937727..434041f77 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -40,6 +40,8 @@ module Dirmap : Map.S with type key = dir_path
 (** {6 Full paths are {e absolute} paths of declarations } *)
 type full_path
 
+val eq_full_path : full_path -> full_path -> bool
+
 (** Constructors of [full_path] *)
 val make_path : dir_path -> identifier -> full_path
 
@@ -68,6 +70,8 @@ type qualid
 val make_qualid : dir_path -> identifier -> qualid
 val repr_qualid : qualid -> dir_path * identifier
 
+val qualid_eq : qualid -> qualid -> bool
+
 val pr_qualid : qualid -> std_ppcmds
 val string_of_qualid : qualid -> string
 val qualid_of_string : string -> qualid
@@ -87,6 +91,8 @@ type object_name = full_path * kernel_name
 
 type object_prefix = dir_path * (module_path * dir_path)
 
+val eq_op : object_prefix -> object_prefix -> bool
+
 val make_oname : object_prefix -> identifier -> object_name
 
 (** to this type are mapped [dir_path]'s in the nametab *)
@@ -98,6 +104,9 @@ type global_dir_reference =
   | DirClosedSection of dir_path
       (** this won't last long I hope! *)
 
+val eq_global_dir_reference : 
+  global_dir_reference -> global_dir_reference -> bool
+
 (** {6 ... } *)
 (** A [reference] is the user-level notion of name. It denotes either a
     global name (referred either by a qualified name or by a single
@@ -107,6 +116,7 @@ type reference =
   | Qualid of qualid located
   | Ident of identifier located
 
+val eq_reference : reference -> reference -> bool
 val qualid_of_reference : reference -> qualid located
 val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
diff --git a/library/library.ml b/library/library.ml
index 7dfde63a7..ec84a75e8 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -28,7 +28,9 @@ let get_load_paths () = List.map pi1 !load_paths
 
 let find_logical_path phys_dir =
   let phys_dir = CUnix.canonical_path_name phys_dir in
-  match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
+  let filter (p, _, _) = String.equal p phys_dir in
+  let paths = List.filter filter !load_paths in
+  match paths with
   | [_,dir,_] -> dir
   | [] -> Nameops.default_root_prefix
   | l -> anomaly ("Two logical paths are associated to "^phys_dir)
@@ -40,21 +42,22 @@ let is_in_load_paths phys_dir =
     List.exists check_p lp
 
 let remove_load_path dir =
-  load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
+  load_paths := List.filter (fun (p,_,_) -> not (String.equal p dir)) !load_paths
 
 let add_load_path isroot (phys_path,coq_path) =
   let phys_path = CUnix.canonical_path_name phys_path in
-    match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
+  let filter (p, _, _) = String.equal p phys_path in
+    match List.filter filter !load_paths with
       | [_,dir,_] ->
-	  if coq_path <> dir
+	  if not (dir_path_eq coq_path dir)
             (* If this is not the default -I . to coqtop *)
             && not
-            (phys_path = CUnix.canonical_path_name Filename.current_dir_name
-		&& coq_path = Nameops.default_root_prefix)
+            (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name)
+		&& dir_path_eq coq_path (Nameops.default_root_prefix))
 	  then
 	    begin
               (* Assume the user is concerned by library naming *)
-	      if dir <> Nameops.default_root_prefix then
+	      if not (dir_path_eq dir Nameops.default_root_prefix) then
 		Flags.if_warn msg_warning
 		  (str phys_path ++ strbrk " was previously bound to " ++
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
@@ -87,7 +90,7 @@ let root_paths_matching_dir_path dir =
 
 let intersections d1 d2 =
   let rec aux d1 =
-    if d1 = empty_dirpath then [d2] else
+    if dir_path_eq d1 empty_dirpath then [d2] else
       let rest = aux (snd (chop_dirpath 1 d1)) in
       if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
       else rest in
@@ -134,9 +137,7 @@ type library_t = {
 module LibraryOrdered =
   struct
     type t = dir_path
-    let compare d1 d2 =
-      Pervasives.compare
-        (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+    let compare = dir_path_ord
   end
 
 module LibraryMap = Map.Make(LibraryOrdered)
@@ -209,7 +210,7 @@ let library_is_loaded dir =
   with Not_found -> false
 
 let library_is_opened dir =
-  List.exists (fun m -> m.library_name = dir) !libraries_imports_list
+  List.exists (fun m -> dir_path_eq m.library_name dir) !libraries_imports_list
 
 let loaded_libraries () =
   List.map (fun m -> m.library_name) !libraries_loaded_list
@@ -223,7 +224,7 @@ let opened_libraries () =
 let register_loaded_library m =
   let rec aux = function
     | [] -> [m]
-    | m'::_ as l when m'.library_name = m.library_name -> l
+    | m'::_ as l when dir_path_eq m'.library_name m.library_name -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
   libraries_table := LibraryMap.add m.library_name m !libraries_table
@@ -237,7 +238,7 @@ let register_loaded_library m =
 let rec remember_last_of_each l m =
   match l with
   | [] -> [m]
-  | m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m
+  | m'::l' when dir_path_eq m'.library_name m.library_name -> remember_last_of_each l' m
   | m'::l' -> m' :: remember_last_of_each l' m
 
 let register_open_library export m =
@@ -251,7 +252,7 @@ let register_open_library export m =
 (* [open_library export explicit m] opens library [m] if not already
    opened _or_ if explicitly asked to be (re)opened *)
 
-let eq_lib_name m1 m2 = m1.library_name = m2.library_name
+let eq_lib_name m1 m2 = dir_path_eq m1.library_name m2.library_name
 
 let open_library export explicit_libs m =
   if
@@ -287,7 +288,7 @@ let open_libraries export modl =
 (* import and export  -  synchronous operations*)
 
 let open_import i (_,(dir,export)) =
-  if i=1 then
+  if Int.equal i 1 then
     (* even if the library is already imported, we re-import it *)
     (* if not (library_is_opened dir) then *)
       open_libraries export [try_find_library dir]
@@ -327,7 +328,7 @@ let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
   let loadpath = root_paths_matching_dir_path pref in
-  if loadpath = [] then raise LibUnmappedDir;
+  let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
   try
     let name = (string_of_id base)^".vo" in
     let _, file = System.where_in_path ~warn:false loadpath name in
@@ -344,7 +345,7 @@ let locate_qualified_library warn qid =
     (* Search library in loadpath *)
     let dir, base = repr_qualid qid in
     let loadpath = loadpaths_matching_dir_path dir in
-    if loadpath = [] then raise LibUnmappedDir;
+    let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
     let name = string_of_id base ^ ".vo" in
     let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
     let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in
@@ -398,7 +399,7 @@ let fetch_opaque_table (f,pos,digest) =
   try
     let ch = System.with_magic_number_check raw_intern_library f in
     seek_in ch pos;
-    if System.marshal_in ch <> digest then failwith "File changed!";
+    if not (String.equal (System.marshal_in ch) digest) then failwith "File changed!";
     let table = (System.marshal_in ch : LightenLibrary.table) in
     close_in ch;
     table
@@ -427,7 +428,7 @@ let rec intern_library needed (dir, f) =
   with Not_found ->
   (* [dir] is an absolute name which matches [f] which must be in loadpath *)
   let m = intern_from_file f in
-  if dir <> m.library_name then
+  if not (dir_path_eq dir m.library_name) then
     errorlabstrm "load_physical_library"
       (str ("The file " ^ f ^ " contains library") ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
@@ -439,7 +440,7 @@ and intern_library_deps needed dir m =
 
 and intern_mandatory_library caller needed (dir,d) =
   let m,needed = intern_library needed (try_locate_absolute_library dir) in
-  if d <> m.library_digest then
+  if not (String.equal d m.library_digest) then
     errorlabstrm "" (strbrk ("Compiled library "^(string_of_dirpath caller)^
 	   ".vo makes inconsistent assumptions over library "
 	   ^(string_of_dirpath dir)));
@@ -449,7 +450,7 @@ let rec_intern_library needed mref =
   let _,needed = intern_library needed mref in needed
 
 let check_library_short_name f dir = function
-  | Some id when id <> snd (split_dirpath dir) ->
+  | Some id when not (id_eq id (snd (split_dirpath dir))) ->
       errorlabstrm "check_library_short_name"
       (str ("The file " ^ f ^ " contains library") ++ spc () ++
       pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
@@ -596,7 +597,8 @@ let import_module export (loc,qid) =
 
 let check_coq_overwriting p id =
   let l = repr_dirpath p in
-  if not !Flags.boot && l <> [] && string_of_id (List.last l) = "Coq" then
+  let is_empty = match l with [] -> true | _ -> false in
+  if not !Flags.boot && not is_empty && String.equal (string_of_id (List.last l)) "Coq" then
     errorlabstrm ""
       (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^
       ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
diff --git a/library/nameops.ml b/library/nameops.ml
index 62665e8af..461e7a405 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -33,7 +33,7 @@ let cut_ident skip_quote s =
       slen
     else
       let c = Char.code (String.get s (n-1)) in
-      if Int.equal c code_of_0 && n <> slen then
+      if Int.equal c code_of_0 && not (Int.equal n slen) then
 	numpart (n-1) n'
       else if code_of_0 <= c && c <= code_of_9 then
 	numpart (n-1) (n-1)
diff --git a/library/nametab.ml b/library/nametab.ml
index 871381530..7c1100165 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -46,10 +46,16 @@ type visibility = Until of int | Exactly of int
 (* The [repr] function is assumed to return the reversed list of idents. *)
 module type UserName = sig
   type t
+  val equal : t -> t -> bool
   val to_string : t -> string
   val repr : t -> identifier * module_ident list
 end
 
+module type EqualityType =
+sig
+  type t
+  val equal : t -> t -> bool
+end
 
 (* A ['a t] is a map from [user_name] to ['a], with possible lookup by
    partially qualified names of type [qualid]. The mapping of
@@ -61,39 +67,41 @@ end
    the same object.
 *)
 module type NAMETREE = sig
-  type 'a t
+  type elt
+  type t
   type user_name
 
-  val empty : 'a t
-  val push : visibility -> user_name -> 'a -> 'a t -> 'a t
-  val locate : qualid -> 'a t -> 'a
-  val find : user_name -> 'a t -> 'a
-  val exists : user_name -> 'a t -> bool
-  val user_name : qualid -> 'a t -> user_name
-  val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid
-  val find_prefixes : qualid -> 'a t -> 'a list
+  val empty : t
+  val push : visibility -> user_name -> elt -> t -> t
+  val locate : qualid -> t -> elt
+  val find : user_name -> t -> elt
+  val exists : user_name -> t -> bool
+  val user_name : qualid -> t -> user_name
+  val shortest_qualid : Idset.t -> user_name -> t -> qualid
+  val find_prefixes : qualid -> t -> elt list
 end
 
-module Make(U:UserName) : NAMETREE with type user_name = U.t
-				     =
+module Make (U : UserName) (E : EqualityType) : NAMETREE
+  with type user_name = U.t and type elt = E.t =
 struct
+  type elt = E.t
 
   type user_name = U.t
 
-  type 'a path_status =
+  type path_status =
       Nothing
-    | Relative of user_name * 'a
-    | Absolute of user_name * 'a
+    | Relative of user_name * elt
+    | Absolute of user_name * elt
 
   (* Dictionaries of short names *)
-  type 'a nametree =
-      { path : 'a path_status;
-	map : 'a nametree ModIdmap.t }
+  type nametree =
+      { path : path_status;
+	map : nametree ModIdmap.t }
 
   let mktree p m = { path=p; map=m }
   let empty_tree = mktree Nothing ModIdmap.empty
 
-  type 'a t = 'a nametree Idmap.t
+  type t = nametree Idmap.t
 
   let empty = Idmap.empty
 
@@ -125,8 +133,8 @@ struct
     | [] ->
 	match tree.path with
 	  | Absolute (uname',o') ->
-	      if o'=o then begin
-		assert (uname=uname');
+	      if E.equal o' o then begin
+		assert (U.equal uname uname');
 		tree
 		  (* we are putting the same thing for the second time :) *)
 	      end
@@ -146,7 +154,7 @@ let rec push_exactly uname o level tree = function
 	try ModIdmap.find modid tree.map
 	with Not_found -> empty_tree
       in
-        if level = 0 then
+        if Int.equal level 0 then
 	  let this =
 	    match tree.path with
 	      | Absolute (n,_) ->
@@ -219,9 +227,10 @@ let shortest_qualid ctx uname tab =
   let id,dir = U.repr uname in
   let hidden = Idset.mem id ctx in
   let rec find_uname pos dir tree =
+    let is_empty = match pos with [] -> true | _ -> false in
     match tree.path with
     | Absolute (u,_) | Relative (u,_)
-          when u=uname && not(pos=[] && hidden) -> List.rev pos
+          when U.equal u uname && not (is_empty && hidden) -> List.rev pos
     | _ ->
 	match dir with
 	    [] -> raise Not_found
@@ -256,36 +265,68 @@ end
 
 (* Global name tables *************************************************)
 
-module SpTab = Make (struct
-		       type t = full_path
-		       let to_string = string_of_path
-		       let repr sp =
-			 let dir,id = repr_path sp in
-			   id, (repr_dirpath dir)
-		     end)
+module FullPath =
+struct
+  type t = full_path
+  let equal = eq_full_path
+  let to_string = string_of_path
+  let repr sp =
+    let dir,id = repr_path sp in
+      id, (repr_dirpath dir)
+end
 
+module ExtRefEqual =
+struct
+  type t = extended_global_reference
+  let equal e1 e2 = Int.equal (ExtRefOrdered.compare e1 e2) 0
+end
 
-type ccitab = extended_global_reference SpTab.t
-let the_ccitab = ref (SpTab.empty : ccitab)
+module KnEqual =
+struct
+  type t = kernel_name
+  let equal kn1 kn2 = Int.equal (kn_ord kn1 kn2) 0
+end
 
-type kntab = kernel_name SpTab.t
-let the_tactictab = ref (SpTab.empty : kntab)
+module MPEqual =
+struct
+  type t = module_path
+  let equal = mp_eq
+end
+
+module ExtRefTab = Make(FullPath)(ExtRefEqual)
+module KnTab = Make(FullPath)(KnEqual)
+module MPTab = Make(FullPath)(MPEqual)
+
+type ccitab = ExtRefTab.t
+let the_ccitab = ref (ExtRefTab.empty : ccitab)
 
-type mptab = module_path SpTab.t
-let the_modtypetab = ref (SpTab.empty : mptab)
+type kntab = KnTab.t
+let the_tactictab = ref (KnTab.empty : kntab)
 
+type mptab = MPTab.t
+let the_modtypetab = ref (MPTab.empty : mptab)
+
+module DirPath =
+struct
+  type t = dir_path
+  let equal d1 d2 = Int.equal (dir_path_ord d1 d2) 0
+  let to_string = string_of_dirpath
+  let repr dir = match repr_dirpath dir with
+    | [] -> anomaly "Empty dirpath"
+    | id :: l -> (id, l)
+end
+
+module GlobDir =
+struct
+  type t = global_dir_reference
+  let equal = eq_global_dir_reference
+end
 
-module DirTab = Make(struct
-		       type t = dir_path
-		       let to_string = string_of_dirpath
-		       let repr dir = match repr_dirpath dir with
-			 | [] -> anomaly "Empty dirpath"
-			 | id::l -> (id,l)
-		     end)
+module DirTab = Make(DirPath)(GlobDir)
 
 (* If we have a (closed) module M having a submodule N, than N does not
    have the entry in [the_dirtab]. *)
-type dirtab = global_dir_reference DirTab.t
+type dirtab = DirTab.t
 let the_dirtab = ref (DirTab.empty : dirtab)
 
 
@@ -317,19 +358,19 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab)
 let push_xref visibility sp xref =
   match visibility with
     | Until _ ->
-	the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	the_globrevtab := Globrevtab.add xref sp !the_globrevtab
     | _ ->
 	begin
-	  if SpTab.exists sp !the_ccitab then
-	    match SpTab.find sp !the_ccitab with
+	  if ExtRefTab.exists sp !the_ccitab then
+	    match ExtRefTab.find sp !the_ccitab with
 	      | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
 		    TrueGlobal( ConstructRef _) as xref ->
-		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+		  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	      | _ -> 
-		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+		  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	    else
-	      the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	      the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
 	end
 
 let push_cci visibility sp ref =
@@ -342,13 +383,13 @@ let push_syndef visibility sp kn =
 let push = push_cci
 
 let push_modtype vis sp kn =
-  the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
+  the_modtypetab := MPTab.push vis sp kn !the_modtypetab;
   the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab
 
 (* This is for tactic definition names *)
 
 let push_tactic vis sp kn =
-  the_tactictab := SpTab.push vis sp kn !the_tactictab;
+  the_tactictab := KnTab.push vis sp kn !the_tactictab;
   the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab
 
 
@@ -364,22 +405,22 @@ let push_dir vis dir dir_ref =
 
 
 (* This should be used when syntactic definitions are allowed *)
-let locate_extended qid = SpTab.locate qid !the_ccitab
+let locate_extended qid = ExtRefTab.locate qid !the_ccitab
 
 (* This should be used when no syntactic definitions is expected *)
 let locate qid = match locate_extended qid with
   | TrueGlobal ref -> ref
   | SynDef _ -> raise Not_found
-let full_name_cci qid = SpTab.user_name qid !the_ccitab
+let full_name_cci qid = ExtRefTab.user_name qid !the_ccitab
 
 let locate_syndef qid = match locate_extended qid with
   | TrueGlobal _ -> raise Not_found
   | SynDef kn -> kn
 
-let locate_modtype qid = SpTab.locate qid !the_modtypetab
-let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
+let locate_modtype qid = MPTab.locate qid !the_modtypetab
+let full_name_modtype qid = MPTab.user_name qid !the_modtypetab
 
-let locate_tactic qid = SpTab.locate qid !the_tactictab
+let locate_tactic qid = KnTab.locate qid !the_tactictab
 
 let locate_dir qid = DirTab.locate qid !the_dirtab
 
@@ -401,9 +442,9 @@ let locate_section qid =
 
 let locate_all qid =
   List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l)
-    (SpTab.find_prefixes qid !the_ccitab) []
+    (ExtRefTab.find_prefixes qid !the_ccitab) []
 
-let locate_extended_all qid = SpTab.find_prefixes qid !the_ccitab
+let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab
 
 (* Derived functions *)
 
@@ -413,11 +454,11 @@ let locate_constant qid =
     | _ -> raise Not_found
 
 let global_of_path sp =
-  match SpTab.find sp !the_ccitab with
+  match ExtRefTab.find sp !the_ccitab with
     | TrueGlobal ref -> ref
     | _ -> raise Not_found
 
-let extended_global_of_path sp = SpTab.find sp !the_ccitab
+let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab
 
 let global r =
   let (loc,qid) = qualid_of_reference r in
@@ -432,7 +473,7 @@ let global r =
 
 (* Exists functions ********************************************************)
 
-let exists_cci sp = SpTab.exists sp !the_ccitab
+let exists_cci sp = ExtRefTab.exists sp !the_ccitab
 
 let exists_dir dir = DirTab.exists dir !the_dirtab
 
@@ -440,7 +481,7 @@ let exists_section = exists_dir
 
 let exists_module = exists_dir
 
-let exists_modtype sp = SpTab.exists sp !the_modtypetab
+let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
 (* Reverse locate functions ***********************************************)
 
@@ -471,11 +512,11 @@ let shortest_qualid_of_global ctx ref =
     | VarRef id -> make_qualid empty_dirpath id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
-        SpTab.shortest_qualid ctx sp !the_ccitab
+        ExtRefTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_syndef ctx kn =
   let sp = path_of_syndef kn in
-    SpTab.shortest_qualid ctx sp !the_ccitab
+    ExtRefTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_module mp =
   let dir = MPmap.find mp !the_modrevtab in
@@ -483,11 +524,11 @@ let shortest_qualid_of_module mp =
 
 let shortest_qualid_of_modtype kn =
   let sp = MPmap.find kn !the_modtyperevtab in
-    SpTab.shortest_qualid Idset.empty sp !the_modtypetab
+    MPTab.shortest_qualid Idset.empty sp !the_modtypetab
 
 let shortest_qualid_of_tactic kn =
   let sp = KNmap.find kn !the_tacticrevtab in
-    SpTab.shortest_qualid Idset.empty sp !the_tactictab
+    KnTab.shortest_qualid Idset.empty sp !the_tactictab
 
 let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
@@ -513,10 +554,10 @@ type frozen = ccitab * dirtab * mptab * kntab
     * globrevtab * mprevtab * mptrevtab * knrevtab
 
 let init () =
-  the_ccitab := SpTab.empty;
+  the_ccitab := ExtRefTab.empty;
   the_dirtab := DirTab.empty;
-  the_modtypetab := SpTab.empty;
-  the_tactictab := SpTab.empty;
+  the_modtypetab := MPTab.empty;
+  the_tactictab := KnTab.empty;
   the_globrevtab := Globrevtab.empty;
   the_modrevtab := MPmap.empty;
   the_modtyperevtab := MPmap.empty;