- 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

8 files changed, 50 insertions, 53 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 29bef7b5a3..4946ee9330 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -161,7 +161,7 @@ let new_inst_no =
   fun () -> incr cnt; string_of_int !cnt
 
 let make_instance_ident gr =
-  Nameops.add_suffix (Nametab.id_of_global gr) ("_autoinstance_"^new_inst_no())
+  Nameops.add_suffix (Nametab.basename_of_global gr) ("_autoinstance_"^new_inst_no())
 
 let new_instance_message ident typ def =
   Flags.if_verbose
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 48a5119d15..82fd9bc1aa 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -612,7 +612,7 @@ let eq_local_binders bl1 bl2 =
   List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2
 
 let extract_coercions indl =
-  let mkqid (_,((_,id),_)) = make_short_qualid id in
+  let mkqid (_,((_,id),_)) = qualid_of_ident id in
   let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
   List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
 
@@ -930,7 +930,7 @@ requested
        let l1,l2 = split_scheme q in
     ( match t with
       | InductionScheme (x,y,z) ->
-             let ind = mkInd (Nametab.inductive_of_reference y) in
+             let ind = mkInd (Nametab.global_inductive y) in
              let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind)
 in
              let z' = family_of_sort (interp_sort z) in
@@ -969,7 +969,7 @@ let build_induction_scheme lnamedepindsort =
   let lrecspec =
     List.map
       (fun (_,dep,indid,sort) ->
-        let ind = Nametab.inductive_of_reference indid in
+        let ind = Nametab.global_inductive indid in
         let (mib,mip) = Global.lookup_inductive ind in
          (ind,mib,mip,dep,interp_elimination_sort sort)) 
       lnamedepindsort
@@ -998,7 +998,7 @@ tried to declare different schemes at once *)
     else (
       if ischeme <> [] then build_induction_scheme ischeme;
       List.iter ( fun indname -> 
-        let ind = Nametab.inductive_of_reference indname
+        let ind = Nametab.global_inductive indname
         in declare_eq_scheme (fst ind);
         try
            make_eq_decidability ind 
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 6fd49b15b9..4e10d1d52c 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -74,7 +74,7 @@ let (input,output) =
 	load_function = (fun _ -> load);
 	subst_function = (fun (_,s,t) -> subst s t);
 	export_function = (fun x -> Some x);
-	classify_function = (fun (_,x) -> Substitute x) 
+	classify_function = (fun x -> Substitute x) 
     }
 
 let update () = Lib.add_anonymous_leaf (input !defined_types)
@@ -102,7 +102,7 @@ let add a b = Profile.profile1 add_key add a b
 
 let _ = Declare.add_cache_hook 
   ( fun sp ->
-      let gr = Nametab.absolute_reference sp in
+      let gr = Nametab.global_of_path sp in
       let ty = Global.type_of_global gr in
       add ty gr )
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d085584264..e6c469974b 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -35,7 +35,7 @@ let (inToken, outToken) =
        open_function = (fun i o -> if i=1 then cache_token o);
        cache_function = cache_token;
        subst_function = Libobject.ident_subst_function;
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        export_function = (fun x -> Some x)}
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
@@ -74,7 +74,7 @@ let (inTacticGrammar, outTacticGrammar) =
        open_function = (fun i o -> if i=1 then cache_tactic_notation o);
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        export_function = (fun x -> Some x)}
 
 let cons_production_parameter l = function
@@ -681,7 +681,7 @@ let subst_syntax_extension (_,subst,(local,sy)) =
   (local, List.map (fun (prec,ntn,gr,pp) ->
      (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy)
 
-let classify_syntax_definition (_,(local,_ as o)) =
+let classify_syntax_definition (local,_ as o) =
   if local then Dispose else Substitute o
 
 let export_syntax_definition (local,_ as o) =
@@ -873,7 +873,7 @@ let cache_notation o =
 let subst_notation (_,subst,(lc,scope,pat,b,ndf)) =
   (lc,scope,subst_interpretation subst pat,b,ndf)
 
-let classify_notation (_,(local,_,_,_,_ as o)) =
+let classify_notation (local,_,_,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_notation (local,_,_,_,_ as o) =
@@ -1058,7 +1058,7 @@ let (inScopeCommand,outScopeCommand) =
       open_function = open_scope_command;
       load_function = load_scope_command;
       subst_function = subst_scope_command;
-      classify_function = (fun (_,obj) -> Substitute obj);
+      classify_function = (fun obj -> Substitute obj);
       export_function = (fun x -> Some x) }
 
 let add_delimiters scope key =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 334b4d82a5..837d502074 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -309,7 +309,7 @@ let (inMLModule,outMLModule) =
                     cache_function = cache_ml_module_object;
                     export_function = export_ml_module_object;
                     subst_function = (fun (_,_,o) -> o);
-                    classify_function = (fun (_,o) -> Substitute o) }
+                    classify_function = (fun o -> Substitute o) }
 
 let declare_ml_modules l =
   Lib.add_anonymous_leaf (inMLModule {mnames=l})
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 481d91787d..66dc28e2d0 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -47,7 +47,7 @@ let rec head_const c = match kind_of_term c with
 
 let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
-  let crible_rec (sp,_) lobj = match object_tag lobj with
+  let crible_rec (sp,kn) lobj = match object_tag lobj with
     | "VARIABLE" ->
 	(try 
 	   let (id,_,typ) = Global.lookup_named (basename sp) in 
@@ -57,14 +57,13 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	     fn (VarRef id) env typ
 	 with Not_found -> (* we are in a section *) ())
     | "CONSTANT" ->
-	let cst = locate_constant (qualid_of_sp sp) in
+	let cst = constant_of_kn kn in
 	let typ = Typeops.type_of_constant env cst in
         if refopt = None
 	  || head_const typ = constr_of_global (Option.get refopt)
 	then
 	  fn (ConstRef cst) env typ
     | "INDUCTIVE" -> 
-	let kn = locate_mind (qualid_of_sp sp) in
         let mib = Global.lookup_mind kn in 
         (match refopt with 
 	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
@@ -86,7 +85,7 @@ let crible ref = gen_crible (Some ref)
 
 (* Fine Search. By Yves Bertot. *)
 
-exception No_section_path
+exception No_full_path
 
 let rec head c = 
   let c = strip_outer_cast c in
@@ -95,9 +94,9 @@ let rec head c =
   | LetIn (_,_,_,c) -> head c
   | _              -> c
       
-let constr_to_section_path c = match kind_of_term c with
+let constr_to_full_path c = match kind_of_term c with
   | Const sp -> sp
-  | _ -> raise No_section_path
+  | _ -> raise No_full_path
       
 let xor a b = (a or b) & (not (a & b))
 
@@ -109,14 +108,14 @@ let plain_display ref a c =
 let filter_by_module (module_list:dir_path list) (accept:bool) 
   (ref:global_reference) _ _ =
   try
-    let sp = sp_of_global ref in
+    let sp = path_of_global ref in
     let sl = dirpath sp in
     let rec filter_aux = function
       | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
       | [] -> true 
     in
     xor accept (filter_aux module_list)
-  with No_section_path -> 
+  with No_full_path -> 
     false
 
 let ref_eq = Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0
@@ -209,7 +208,7 @@ let gen_filtered_search filter_function display_function =
 
 (** SearchAbout *)
 
-let name_of_reference ref = string_of_id (id_of_global ref)
+let name_of_reference ref = string_of_id (basename_of_global ref)
 
 type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fa56e60f69..1de9d739a3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -506,12 +506,11 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
          Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
            export
 
-let vernac_end_module export (loc,id) =
-  let mp = Declaremods.end_module id in
-    Dumpglob.dump_modref loc mp "mod";
-    if_verbose message ("Module "^ string_of_id id ^" is defined") ;
-    Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
-
+let vernac_end_module export (loc,id as lid) =
+  let mp = Declaremods.end_module () in
+  Dumpglob.dump_modref loc mp "mod";
+  if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+  Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
   if Lib.sections_are_opened () then
@@ -549,46 +548,43 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
 	  if_verbose message 
 	    ("Module Type "^ string_of_id id ^" is defined")
 
-
 let vernac_end_modtype (loc,id) =
-  let mp = Declaremods.end_modtype id in
-    Dumpglob.dump_modref loc mp "modtype";
-    if_verbose message 
-      ("Module Type "^ string_of_id id ^" is defined")
-
+  let mp = Declaremods.end_modtype () in
+  Dumpglob.dump_modref loc mp "modtype";
+  if_verbose message ("Module Type "^ string_of_id id ^" is defined")
+	  
 let vernac_include = function
   | CIMTE mty_ast ->
       Declaremods.declare_include Modintern.interp_modtype mty_ast false
   | CIME mexpr_ast ->
       Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true
 	  
-	  
-	  
 (**********************)
 (* Gallina extensions *)
 
-  (* Sections *)
+(* Sections *)
 
 let vernac_begin_section (_, id as lid) =
   check_no_pending_proofs ();
   Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
-let vernac_end_section (loc, id) = 
-  
-    Dumpglob.dump_reference loc 
-      (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
-  Lib.close_section id
+let vernac_end_section (loc,_) =
+  Dumpglob.dump_reference loc 
+    (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
+  Lib.close_section ()
+
+(* Dispatcher of the "End" command *)
 
-let vernac_end_segment lid =
+let vernac_end_segment (_,id as lid) =
   check_no_pending_proofs ();
-  let o = try Lib.what_is_opened () with 
-      Not_found -> error "There is nothing to end." in
-    match o with
-      | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid
-      | _,Lib.OpenedModtype _ -> vernac_end_modtype lid
-      | _,Lib.OpenedSection _ -> vernac_end_section lid
-      | _ -> anomaly "No more opened things"
+  match Lib.find_opening_node id with
+  | Lib.OpenedModule (export,_,_) -> vernac_end_module export lid
+  | Lib.OpenedModtype _ -> vernac_end_modtype lid
+  | Lib.OpenedSection _ -> vernac_end_section lid
+  | _ -> anomaly "No more opened things"
+
+(* Libraries *)
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
@@ -597,6 +593,8 @@ let vernac_require import _ qidl =
     List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
   Library.require_library_from_dirpath modrefl import
 
+(* Coercions and canonical structures *)
+
 let vernac_canonical r =
   Recordops.declare_canonical_structure (global_with_alias r)
 
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 63d93a7676..b844f03ca1 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -131,9 +131,9 @@ let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
 
 let section_parameters = function
   | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
-      get_discharged_hyp_names (sp_of_global (IndRef(induri,0)))
+      get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
   | RRef (_,(ConstRef cst as ref)) ->
-      get_discharged_hyp_names (sp_of_global ref)
+      get_discharged_hyp_names (path_of_global ref)
   | _ -> []
 
 let merge vl al =
@@ -217,7 +217,7 @@ END
 VERNAC COMMAND EXTEND Whelp
 | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
 | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
-| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] 
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (global_inductive_with_alias r) ] 
 | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
 END