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

4 files changed, 15 insertions, 15 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index f07541912..a3ac17b34 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -412,8 +412,8 @@ let add_hints local dbnames0 h =
   | HintsImmediate lhints ->
       add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
-      let f qid =
-	let r = Nametab.global qid in
+      let f r =
+	let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
         let r' = match r with
          | ConstRef c -> EvalConstRef c
          | VarRef c -> EvalVarRef c
@@ -427,7 +427,7 @@ let add_hints local dbnames0 h =
   | HintsConstructors lqid ->
       let add_one qid =
         let env = Global.env() and sigma = Evd.empty in
-        let isp = global_inductive qid in
+        let isp = inductive_of_reference qid in
         let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
         let lcons = list_tabulate
           (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in
@@ -893,8 +893,8 @@ let superauto n to_add argl  =
 
 let default_superauto g = superauto !default_search_depth [] [] g
 
-let interp_to_add gl locqid =
-  let r = Nametab.global locqid in
+let interp_to_add gl r =
+  let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
   let id = id_of_global r in
   (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r)
 
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 02c688e25..ec8a38501 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -153,7 +153,7 @@ let special_whd env =
   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
-let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+let _eq = Libnames.constr_of_global (Coqlib.glob_eq)
 
 let decompose_eq env id =
   let typ = Environ.named_type id env in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 134f018ca..1d5ab017c 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -530,7 +530,7 @@ let instr_cut mkstat _thus _then cut gls0 =
 
 
 (* iterated equality *)
-let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+let _eq = Libnames.constr_of_global (Coqlib.glob_eq)
 
 let decompose_eq id gls =
   let typ = pf_get_hyp_typ gls id in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index abe06e5d3..11d86630b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -383,7 +383,7 @@ let loc_of_by_notation f = function
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 
 let intern_inductive_or_by_notation = function
-  | AN r -> Nametab.global_inductive r
+  | AN r -> Nametab.inductive_of_reference r
   | ByNotation (loc,ntn) ->
       destIndRef (Notation.interp_notation_as_global_reference loc
         (function IndRef ind -> true | _ -> false) ntn)
@@ -395,9 +395,9 @@ let intern_inductive ist = function
 let intern_global_reference ist = function
   | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
   | r -> 
-      let loc,qid = qualid_of_reference r in
-      try ArgArg (loc,locate_global qid)
-      with _ -> 
+      let loc,qid as lqid = qualid_of_reference r in
+      try ArgArg (loc,locate_global_with_alias lqid)
+      with Not_found -> 
 	error_global_not_found_loc loc qid
 
 let intern_tac_ref ist = function
@@ -420,8 +420,8 @@ let intern_constr_reference strict ist = function
   | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
       RVar (dloc,id), None
   | r ->
-      let loc,qid = qualid_of_reference r in
-      RRef (loc,locate_global qid), if strict then None else Some (CRef r)
+      let loc,_ as lqid = qualid_of_reference r in
+      RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
 
 let intern_reference strict ist r =
   (try Reference (intern_tac_ref ist r)
@@ -512,8 +512,8 @@ let short_name = function
   | _ -> None
 
 let interp_global_reference r =
-  let loc,qid = qualid_of_reference r in
-  try locate_global qid
+  let loc,qid as lqid = qualid_of_reference r in
+  try locate_global_with_alias lqid
   with Not_found ->
   match r with 
   | Ident (loc,id) when not !strict_check -> VarRef id