Prise en compte des notations "alias" dans la globalisation des coercions.

Au passage, un peu plus de standardisation des noms de fonctions de
globalisation 

Principe de base :

  locate_foo : qualid -> foo                   (échoue avec Not_found)
  global : reference -> global_reference       (échoue avec UserError)
  global_of_foo : foo -> global_reference      (échoue avec UserError)

  f_with_alias : se comporte comme f mais prenant aussi en compte les
    notations de la forme "Notation id:=ref"

Principale exception :

  locate, au lieu de locate_global
  locate_global_with_alias, qui prend en entrée un "qualid located"

Restent beaucoup de fonctions qui pourraient utiliser
global_with_alias au lieu de global, notamment dans contribs.


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

3 files changed, 25 insertions, 44 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0b9f76d951..99f9e3ed7c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -853,7 +853,7 @@ requested
        let l1,l2 = split_scheme q in
     ( match t with
       | InductionScheme (x,y,z) ->
-             let ind = mkInd (Nametab.global_inductive y) in
+             let ind = mkInd (Nametab.inductive_of_reference 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
@@ -892,7 +892,7 @@ let build_induction_scheme lnamedepindsort =
   let lrecspec =
     List.map
       (fun (_,dep,indid,sort) ->
-        let ind = Nametab.global_inductive indid in
+        let ind = Nametab.inductive_of_reference indid in
         let (mib,mip) = Global.lookup_inductive ind in
          (ind,mib,mip,dep,interp_elimination_sort sort)) 
       lnamedepindsort
@@ -921,7 +921,7 @@ tried to declare different schemes at once *)
     else (
       if ischeme <> [] then build_induction_scheme ischeme;
       List.iter ( fun indname -> 
-        let ind = Nametab.global_inductive indname
+        let ind = Nametab.inductive_of_reference indname
         in declare_eq_scheme (fst ind);
            make_eq_decidability ind 
       ) escheme
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1eb1f89867..784cabcd5c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -35,6 +35,7 @@ open Decl_kinds
 open Topconstr
 open Pretyping
 open Redexpr
+open Syntax_def
 
 (* Pcoq hooks *)
 
@@ -58,7 +59,7 @@ let set_pcoq_hook f = pcoq := Some f
 let cl_of_qualid = function
   | FunClass -> Classops.CL_FUN
   | SortClass -> Classops.CL_SORT
-  | RefClass r -> Class.class_of_global (Nametab.global r)
+  | RefClass r -> Class.class_of_global (global_with_alias r)
 
 (*******************)
 (* "Show" commands *)
@@ -284,8 +285,8 @@ let vernac_bind_scope sc cll =
 
 let vernac_open_close_scope = Notation.open_close_scope
 
-let vernac_arguments_scope local qid scl =
-  Notation.declare_arguments_scope local (global qid) scl
+let vernac_arguments_scope local r scl =
+  Notation.declare_arguments_scope local (global_with_alias r) scl
 
 let vernac_infix = Metasyntax.add_infix
 
@@ -506,24 +507,13 @@ let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
   Library.require_library qidl import
 
-let vernac_canonical locqid =
-  Recordops.declare_canonical_structure (Nametab.global locqid)
-
-let locate_reference ref =
-  let (loc,qid) = qualid_of_reference ref in
-  try match Nametab.extended_locate qid with
-    | TrueGlobal ref -> ref
-    | SyntacticDef kn -> 
-	match Syntax_def.search_syntactic_definition loc kn with
-	  | Rawterm.RRef (_,ref) -> ref
-	  | _ -> raise Not_found
-  with Not_found ->
-    error_global_not_found_loc loc qid
+let vernac_canonical r =
+  Recordops.declare_canonical_structure (global_with_alias r)
 
 let vernac_coercion stre ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  let ref' = locate_reference ref in
+  let ref' = global_with_alias ref in
   Class.try_add_new_coercion_with_target ref' stre source target;
   if_verbose message ((string_of_reference ref) ^ " is now a coercion")
 
@@ -666,11 +656,11 @@ let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition = Command.syntax_definition 
 
-let vernac_declare_implicits local locqid = function
+let vernac_declare_implicits local r = function
   | Some imps ->
-      Impargs.declare_manual_implicits local (Nametab.global locqid) imps
+      Impargs.declare_manual_implicits local (global_with_alias r) imps
   | None -> 
-      Impargs.declare_implicits local (Nametab.global locqid)
+      Impargs.declare_implicits local (global_with_alias r)
 
 let vernac_reserve idl c =
   let t = Constrintern.interp_type Evd.empty (Global.env()) c in
@@ -861,8 +851,8 @@ let _ =
       optread=(fun () -> get_debug () <> Tactic_debug.DebugOff);
       optwrite=vernac_debug }
 
-let vernac_set_opacity opaq locqid =
-  match Nametab.global locqid with
+let vernac_set_opacity opaq r =
+  match global_with_alias r with
     | ConstRef sp ->
 	if opaq then set_opaque_const sp
 	else set_transparent_const sp
@@ -962,7 +952,7 @@ let vernac_print = function
   | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
   | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ()))
   | PrintUniverses (Some s) -> dump_universes s
-  | PrintHint qid -> Auto.print_hint_ref (Nametab.global qid)
+  | PrintHint r -> Auto.print_hint_ref (global_with_alias r)
   | PrintHintGoal -> Auto.print_applicable_hint ()
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
   | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
@@ -977,17 +967,14 @@ let vernac_print = function
   | PrintAbout qid -> msgnl (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
-  | PrintNeededAssumptions qid ->
-      let cstr =  constr_of_reference (global qid)
-      in
-      let nassumptions = Environ.needed_assumptions cstr
-                                          (Global.env ())
-      in
+  | PrintNeededAssumptions r ->
+      let cstr = constr_of_global (global_with_alias r) in
+      let nassumptions = Environ.needed_assumptions cstr (Global.env ()) in
       msg 
       (try
         Printer.pr_assumptionset (Global.env ()) nassumptions
       with Not_found ->
-        pr_reference qid ++ str " is closed under the global context")
+        pr_reference r ++ str " is closed under the global context")
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in
@@ -1003,7 +990,7 @@ let interp_search_restriction = function
 open Search
 
 let interp_search_about_item = function
-  | SearchRef qid -> GlobSearchRef (Nametab.global qid)
+  | SearchRef r -> GlobSearchRef (global_with_alias r)
   | SearchString s -> GlobSearchString s
 
 let vernac_search s r =
@@ -1016,8 +1003,8 @@ let vernac_search s r =
   | SearchRewrite c ->
       let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
       Search.search_rewrite pat r
-  | SearchHead locqid ->
-      Search.search_by_head (Nametab.global locqid) r
+  | SearchHead ref ->
+      Search.search_by_head (global_with_alias ref) r
   | SearchAbout sl ->
       Search.search_about (List.map interp_search_about_item sl) r
 
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 67ba2bd52e..4a200591e4 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -28,6 +28,7 @@ open Command
 open Pfedit
 open Refiner
 open Tacmach
+open Syntax_def
 
 (* Coq interface to the Whelp query engine developed at 
    the University of Bologna *)
@@ -192,13 +193,6 @@ let whelp_locate s =
 let whelp_elim ind = 
   send_whelp "elim" (make_string uri_of_global (IndRef ind))
 
-let locate_inductive r =
-  let (loc,qid) = qualid_of_reference r in
-  try match Syntax_def.locate_global qid with
-    | IndRef ind -> ind
-    | _ -> user_err_loc (loc,"",str "Inductive type expected")
-  with Not_found -> error_global_not_found_loc loc qid
-
 let on_goal f =
   let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in
   f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
@@ -221,7 +215,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 (locate_inductive r) ] 
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] 
 | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
 END