- 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

10 files changed, 35 insertions, 33 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d89306ed2..e4e625205b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -336,11 +336,11 @@ let check_no_explicitation l =
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env args =
-  try match Nametab.extended_locate qid with
+  try match Nametab.locate_extended qid with
   | TrueGlobal ref ->
       Dumpglob.add_glob loc ref;
       RRef (loc, ref), args
-  | SyntacticDef sp ->
+  | SynDef sp ->
       Dumpglob.add_glob_kn loc sp;
       let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
       let nids = List.length ids in
@@ -365,7 +365,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
   | Ident (loc, id) ->
       try intern_var env lvar loc id, args
       with Not_found -> 
-      let qid = make_short_qualid id in
+      let qid = qualid_of_ident id in
       try
 	let r,args2 = intern_non_secvar_qualid loc qid intern env args in
 	find_appl_head_data lvar r, args2
@@ -536,10 +536,10 @@ type pattern_qualid_kind =
 let find_constructor ref f aliases pats scopes =
   let (loc,qid) = qualid_of_reference ref in
   let gref =
-    try extended_locate qid
+    try locate_extended qid
     with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
   match gref with
-  | SyntacticDef sp ->
+  | SynDef sp ->
       let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
       (match a with
        | ARef (ConstructRef cstr) ->
@@ -1357,21 +1357,21 @@ let interp_context_evars ?(fail_anonymous=false) evdref env params =
 (* Locating reference, possibly via an abbreviation *)
 
 let locate_reference qid =
-  match Nametab.extended_locate qid with
+  match Nametab.locate_extended qid with
     | TrueGlobal ref -> ref
-    | SyntacticDef kn -> 
+    | SynDef kn -> 
 	match Syntax_def.search_syntactic_definition dummy_loc kn with
 	  | [],ARef ref -> ref
 	  | _ -> raise Not_found
 
 let is_global id =
   try 
-    let _ = locate_reference (make_short_qualid id) in true
+    let _ = locate_reference (qualid_of_ident id) in true
   with Not_found -> 
     false
 
 let global_reference id = 
-  constr_of_global (locate_reference (make_short_qualid id))
+  constr_of_global (locate_reference (qualid_of_ident id))
 
 let construct_reference ctx id =
   try
@@ -1380,5 +1380,5 @@ let construct_reference ctx id =
     global_reference id
 
 let global_reference_in_absolute_module dir id = 
-  constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id))
+  constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index e110ad00a0..d38ef592fc 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -26,7 +26,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
-  try global_of_extended_global (Nametab.extended_absolute_reference sp)
+  try global_of_extended_global (Nametab.extended_global_of_path sp)
   with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp))
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
@@ -36,7 +36,7 @@ let gen_reference = coq_reference
 let gen_constant = coq_constant
 
 let has_suffix_in_dirs dirs ref =
-  let dir = dirpath (sp_of_global ref) in
+  let dir = dirpath (path_of_global ref) in
   List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
 
 let global_of_extended q =
@@ -45,7 +45,7 @@ let global_of_extended q =
 let gen_constant_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let id = id_of_string s in
-  let all = Nametab.extended_locate_all (make_short_qualid id) in
+  let all = Nametab.locate_extended_all (qualid_of_ident id) in
   let all = list_uniquize (list_map_filter global_of_extended all) in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 5b550a86bf..8b03849602 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -59,7 +59,7 @@ val logic_module : dir_path
 val logic_type_module : dir_path
 
 (* Natural numbers *)
-val nat_path : section_path
+val nat_path : full_path
 val glob_nat : global_reference
 val path_of_O : constructor
 val path_of_S : constructor
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 71f38063af..79b58da84d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -118,7 +118,7 @@ let type_of_global_ref gr =
 let remove_sections dir =
   if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
     (* Not yet (fully) discharged *)
-    Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+    Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
   else
     (* Theorem/Lemma outside its outer section of definition *)
     dir
@@ -139,7 +139,7 @@ let add_glob_gen loc sp lib_dp ty =
 
 let add_glob loc ref = 
   if dump () && loc <> Util.dummy_loc then
-    let sp = Nametab.sp_of_global ref in
+    let sp = Nametab.path_of_global ref in
     let lib_dp = Lib.library_part ref in
     let ty = type_of_global_ref ref in
       add_glob_gen loc sp lib_dp ty
@@ -150,7 +150,7 @@ let mp_of_kn kn =
 
 let add_glob_kn loc kn =
   if dump () && loc <> Util.dummy_loc then
-    let sp = Nametab.sp_of_syntactic_definition kn in
+    let sp = Nametab.path_of_syndef kn in
     let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
       add_glob_gen loc sp lib_dp "syndef"
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4495c22c67..a550111a30 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -30,13 +30,13 @@ let ids_of_list l =
   List.fold_right Idset.add l Idset.empty
 
 let locate_reference qid =
-  match Nametab.extended_locate qid with
+  match Nametab.locate_extended qid with
     | TrueGlobal ref -> true
-    | SyntacticDef kn -> true
+    | SynDef kn -> true
 
 let is_global id =
   try 
-    locate_reference (make_short_qualid id)
+    locate_reference (qualid_of_ident id)
   with Not_found -> 
     false
 
diff --git a/interp/notation.ml b/interp/notation.ml
index e6c627e863..2857f9ad8a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -113,7 +113,7 @@ let subst_scope (_,subst,sc) = sc
 
 open Libobject
 
-let classify_scope (_,(local,_,_ as o)) =
+let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_scope (local,_,_ as x) = if local then None else Some x
@@ -201,7 +201,7 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
 (**********************************************************************)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
-type required_module = section_path * string list 
+type required_module = full_path * string list 
 
 type 'a prim_token_interpreter =
     loc -> 'a -> rawconstr
@@ -248,7 +248,7 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
     (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
-  try let _ = Nametab.absolute_reference sp in ()
+  try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
     str ("Cannot interpret in "^sc^" without requiring first module "
@@ -485,7 +485,7 @@ let (inArgumentsScope,outArgumentsScope) =
       cache_function = cache_arguments_scope;
       load_function = load_arguments_scope;
       subst_function = subst_arguments_scope;
-      classify_function = (fun (_,o) -> Substitute o);
+      classify_function = (fun o -> Substitute o);
       discharge_function = discharge_arguments_scope;
       rebuild_function = rebuild_arguments_scope;
       export_function = (fun x -> Some x) }
diff --git a/interp/notation.mli b/interp/notation.mli
index 06349014db..21d3ae1a08 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -66,7 +66,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
    an appropriate error message *)
 
 type notation_location = dir_path * string
-type required_module = section_path * string list 
+type required_module = full_path * string list 
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
 type 'a prim_token_interpreter =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index bb8d68323a..ef5ecf62a2 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -16,6 +16,7 @@ open Topconstr
 open Libobject
 open Lib
 open Nameops
+open Nametab
 
 (* Syntactic definitions. *)
 
@@ -37,13 +38,13 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant kn pat;
-  Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
+  Nametab.push_syndef (Nametab.Until i) sp kn;
   if not onlyparse then
     (* Declare it to be used as long name *)
     Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
 
 let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
-  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
+  Nametab.push_syndef (Nametab.Exactly i) sp kn;
   if not onlyparse then
     (* Redeclare it to be used as (short) name in case an other (distfix)
        notation was declared inbetween *)
@@ -55,7 +56,7 @@ let cache_syntax_constant d =
 let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
   (local,subst_interpretation subst pat,onlyparse)
 
-let classify_syntax_constant (_,(local,_,_ as o)) =
+let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_syntax_constant (local,_,_ as o) =
@@ -85,19 +86,19 @@ let search_syntactic_definition loc kn =
 
 let global_of_extended_global = function
   | TrueGlobal ref -> ref
-  | SyntacticDef kn -> 
+  | SynDef kn -> 
   match search_syntactic_definition dummy_loc kn with
   | [],ARef ref -> ref
   | _ -> raise Not_found
 
 let locate_global_with_alias (loc,qid) =
-  let ref = Nametab.extended_locate qid in
+  let ref = Nametab.locate_extended qid in
   try global_of_extended_global ref
   with Not_found ->
     user_err_loc (loc,"",pr_qualid qid ++ 
       str " is bound to a notation that does not denote a reference")
 
-let inductive_of_reference_with_alias r =
+let global_inductive_with_alias r =
   match locate_global_with_alias (qualid_of_reference r) with
   | IndRef ind -> ind
   | ref ->
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 39583d8568..fb0c3c9f28 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,6 +13,7 @@ open Util
 open Names
 open Topconstr
 open Rawterm
+open Nametab
 open Libnames
 (*i*)
 
@@ -39,4 +40,4 @@ val global_of_extended_global : extended_global_reference -> global_reference
 val global_with_alias : reference -> global_reference
 
 (* The same for inductive types *)
-val inductive_of_reference_with_alias : reference -> inductive
+val global_inductive_with_alias : reference -> inductive
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 32595cdc65..eb46a5d6e7 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -770,7 +770,7 @@ let ids_of_cases_tomatch tms =
     tms []
 
 let is_constructor id =
-  try ignore (Nametab.extended_locate (make_short_qualid id)); true
+  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
   with Not_found -> true
  
 let rec cases_pattern_fold_names f a = function