- Cleaning phase of the interfaces of libnames.ml and nametab.ml

  (uniformisation of function names, classification). One of the most
  visible change is the renaming of section_path into full_path (the
  use of name section was obsolete due to the module system, but I
  don't know if the new name is the best chosen one - especially it 
  remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.



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

7 files changed, 25 insertions, 47 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 911ded641e..901341e7bc 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -384,7 +384,7 @@ let (inCoercion,_) =
     load_function = load_coercion;
     cache_function = cache_coercion;
     subst_function = subst_coercion;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_coercion;
     export_function = (function x -> Some x)  }
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d43bc07803..2c3de28a5f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -32,7 +32,7 @@ let dl = dummy_loc
 (* Tools for printing of Cases                                              *)
 
 let encode_inductive r =
-  let indsp = inductive_of_reference r in
+  let indsp = global_inductive r in
   let constr_lengths = mis_constr_nargs indsp in
   (indsp,constr_lengths)
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f8dab16cd7..6a4c066ce5 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -579,14 +579,14 @@ let lookup_eliminator ind_sp s =
   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_con mp dp (label_of_id id)) in
-  try 
-    let _ = sp_of_global ref in
-    constr_of_global ref
+  try
+    let cst = make_con mp dp (label_of_id id) in
+    let _ = Global.lookup_constant cst in
+    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") *)
-  try constr_of_global (Nametab.locate (make_short_qualid id))
+  try constr_of_global (Nametab.locate (qualid_of_ident id))
   with Not_found ->
     errorlabstrm "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
@@ -594,25 +594,3 @@ let lookup_eliminator ind_sp s =
        pr_global_env Idset.empty (IndRef ind_sp) ++ 
        strbrk " on sort " ++ pr_sort_family s ++
        strbrk " 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 *)
-  (* inductive type *)
-  try construct_absolute_reference (Names.make_path dir id)
-  with Not_found ->
-  (* Then try to get a user-defined eliminator in some other places *)
-  (* using short name (e.g. for "eq_rec") *)
-    try constr_of_global (Nametab.locate (make_short_qualid 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 base ++ spc () ++ str "on sort " ++ 
-           spc () ++ pr_sort_family s ++
-	   str " is probably not allowed")
-*)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 8bf95ecbfb..c82589b9a6 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -77,7 +77,7 @@ let (inStruc,outStruc) =
     cache_function = cache_structure;
     load_function = load_structure;
     subst_function = subst_structure;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_structure;
     export_function = (function x -> Some x) }
 
@@ -141,7 +141,7 @@ let (in_method,out_method) =
 	cache_function = load_method;
 	subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
 	export_function = (fun x -> Some x);
-	classify_function = (fun (_,x) -> Substitute x) 
+	classify_function = (fun x -> Substitute x) 
     }
 
 let methods_matching c = MethodsDnet.search_pattern !meth_dnet c
@@ -271,7 +271,7 @@ let (inCanonStruc,outCanonStruct) =
     open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;
     subst_function = subst_canonical_structure;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_canonical_structure;
     export_function = (function x -> Some x) }
 
@@ -281,7 +281,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
 let error_not_structure ref =
   errorlabstrm "object_declare"
-    (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object.")
+    (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b7013a7033..024f190f2a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -807,7 +807,7 @@ let unfold env sigma name =
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
-(* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
+(* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
  * Performs a betaiota reduction after unfolding. *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b7a4fc9258..4034d86674 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -34,7 +34,7 @@ let pr_name = function
   | Name id -> pr_id id
   | Anonymous -> str "_"
 
-let pr_sp sp = str(string_of_kn sp)
+let pr_path sp = str(string_of_kn sp)
 let pr_con sp = str(string_of_con sp)
 
 let rec pr_constr c = match kind_of_term c with
@@ -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_sp sp ++ str"," ++ int i ++ str")"
+  | Ind (sp,i) -> str"Ind(" ++ pr_path sp ++ str"," ++ int i ++ str")"
   | Construct ((sp,i),j) ->
-      str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
+      str"Constr(" ++ pr_path 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() ++
@@ -711,7 +711,7 @@ let add_vname vars = function
     Name id -> Idset.add id vars
   | _ -> vars
 
-let id_of_global = Nametab.id_of_global
+let basename_of_global = Nametab.basename_of_global
 
 let sort_hdchar = function
   | Prop(_) -> "P"
@@ -731,9 +731,9 @@ let hdchar env c =
 	if i=0 then 
 	  lowercase_first_char (id_of_label (label kn))
 	else 
-	  lowercase_first_char (id_of_global (IndRef x))
+	  lowercase_first_char (basename_of_global (IndRef x))
     | Construct ((sp,i) as x) ->
-	lowercase_first_char (id_of_global (ConstructRef x))
+	lowercase_first_char (basename_of_global (ConstructRef x))
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar s
     | Rel n ->
@@ -839,14 +839,14 @@ let is_imported_ref = function
 
 let is_global id =
   try 
-    let ref = locate (make_short_qualid id) in
+    let ref = locate (qualid_of_ident id) in
     not (is_imported_ref ref)
   with Not_found -> 
     false
 
 let is_constructor id =
   try 
-    match locate (make_short_qualid id) with 
+    match locate (qualid_of_ident id) with 
       | ConstructRef _ as ref -> not (is_imported_ref ref)
       | _ -> false
   with Not_found -> 
@@ -907,12 +907,12 @@ let occur_rel p env id =
 let occur_id nenv id0 c =
   let rec occur n c = match kind_of_term c with
     | Var id when  id=id0 -> raise Occur
-    | Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur
+    | Const kn when basename_of_global (ConstRef kn) = id0 -> raise Occur
     | Ind ind_sp
-	when id_of_global (IndRef ind_sp) = id0 ->
+	when basename_of_global (IndRef ind_sp) = id0 ->
         raise Occur
     | Construct cstr_sp
-	when id_of_global (ConstructRef cstr_sp) = id0 ->
+	when basename_of_global (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/typeclasses.ml b/pretyping/typeclasses.ml
index 2f2796f1c6..52e2eb24e5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -168,7 +168,7 @@ let (class_input,class_output) =
       cache_function = cache_class;
       load_function = (fun _ -> load_class);
       open_function = (fun _ -> load_class);
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_class a));
       rebuild_function = rebuild_class;
       subst_function = subst_class;
@@ -212,7 +212,7 @@ let (instance_input,instance_output) =
       cache_function = cache_instance;
       load_function = (fun _ -> load_instance);
       open_function = (fun _ -> load_instance);
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_instance a));
       rebuild_function = rebuild_instance;
       subst_function = subst_instance;