- 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

1 files changed, 4 insertions, 4 deletions

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) }