- 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

4 files changed, 10 insertions, 10 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 11c3b3b5b6..e1edeec37e 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -303,9 +303,9 @@ let ref_renaming_fun (k,r) =
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
       let globs = Idset.elements (get_global_ids ()) in
-      let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in
+      let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in
       string_of_id id
-    else modular_rename k (safe_id_of_global r)
+    else modular_rename k (safe_basename_of_global r)
   in
   add_global_ids (id_of_string s);
   s::l
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39e2770819..ba4786d37d 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -506,7 +506,7 @@ let simple_extraction r = match locate_ref [r] with
 let extraction_library is_rec m =
   init true;
   let dir_m =
-    let q = make_short_qualid m in
+    let q = qualid_of_ident m in
     try Nametab.full_name_module q with Not_found -> error_unknown_module q
   in
   Visit.add_mp (MPfile dir_m);
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 83a780198a..13a730ac20 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -182,7 +182,7 @@ let modular () = !modular_ref
    WARNING: for inductive objects, an extract_inductive must have been
    done before. *)
 
-let safe_id_of_global = function
+let safe_basename_of_global = function
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
   | ConstructRef ((kn,i),j) ->
@@ -191,7 +191,7 @@ let safe_id_of_global = function
 
 let safe_pr_global r =
  try Printer.pr_global r
- with _ -> pr_id (safe_id_of_global r)
+ with _ -> pr_id (safe_basename_of_global r)
 
 (* idem, but with qualification, and only for constants. *)
 
@@ -207,7 +207,7 @@ let pr_long_mp mp =
   let lid = repr_dirpath (Nametab.dir_of_mp mp) in
   str (String.concat "." (List.map string_of_id (List.rev lid)))
 
-let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
+let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 (*S Warning and Error messages. *)
 
@@ -452,7 +452,7 @@ let (inline_extraction,_) =
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
@@ -535,7 +535,7 @@ let (blacklist_extraction,_) =
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Libobject.Keep o);
+       classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,_,x) -> x)
     }
 
@@ -595,7 +595,7 @@ let (in_customs,_) =
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 6e3f2ec56b..42ed6eef01 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -13,7 +13,7 @@ open Libnames
 open Miniml
 open Declarations
 
-val safe_id_of_global : global_reference -> identifier
+val safe_basename_of_global : global_reference -> identifier
 
 (*s Warning and Error messages. *)