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

21 files changed, 106 insertions, 111 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index b5ba3b00e..22fefa65d 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -443,7 +443,7 @@ and axiomatize_body env r id d = match r with
   | IndRef i ->
       iter_all_constructors i
 	(fun _ c ->
-	   let rc = reference_of_constr c in
+	   let rc = global_of_constr c in
 	   try
 	     begin match tr_global env rc with
 	       | DeclFun (_, _, [], _) -> ()
@@ -460,7 +460,7 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
       iter_all_constructors ci.ci_ind
 	(fun j cj ->
 	   try
-	     let cjr = reference_of_constr cj in
+	     let cjr = global_of_constr cj in
 	     begin match tr_global env cjr with
 	       | DeclFun (idc, _, l, _) ->
 		   let b = br.(j) in
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 13b242d5d..609504ba5 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -131,7 +131,7 @@ let coq_constant s =
     (Coqlib.init_modules @ Coqlib.arith_modules) s;;
 
 let constant sl s =
-  constr_of_reference
+  constr_of_global
     (Nametab.locate (make_qualid(Names.make_dirpath 
 			   (List.map id_of_string (List.rev sl)))
 	       (id_of_string s)));;
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 832e4647f..318cde773 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -236,7 +236,7 @@ let coq_constant s =
     (Coqlib.init_modules @ Coqlib.arith_modules) s;;
 
 let constant sl s =
-  constr_of_reference
+  constr_of_global
     (locate (make_qualid(Names.make_dirpath 
 			   (List.map id_of_string (List.rev sl)))
 	       (id_of_string s)));;
@@ -275,8 +275,8 @@ let acc_inv_id = function () -> (coq_constant "Acc_inv")
 let well_founded_ltof = function () ->  (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
 let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
-let iter = function () -> (constr_of_reference (delayed_force iter_ref))
-let max_constr = function () -> (constr_of_reference (delayed_force max_ref))
+let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let max_constr = function () -> (constr_of_global (delayed_force max_ref))
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
@@ -622,7 +622,7 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
  
 	   
 let rec_leaf_terminate concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr =
-  match find_call_occs 0 (mkVar (get_f (constr_of_reference func))) expr with
+  match find_call_occs 0 (mkVar (get_f (constr_of_global func))) expr with
   | context_fn, args ->
       observe_tac "introduce_all_values" 
 	(introduce_all_values concl_tac is_mes acc_inv func context_fn eqs  hrec args  [] [])
@@ -669,13 +669,13 @@ let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)
   proveterminate 
 
 let hyp_terminates nb_args func = 
-  let a_arrow_b = arg_type (constr_of_reference func) in 
+  let a_arrow_b = arg_type (constr_of_global func) in 
   let rev_args,b = decompose_prod_n nb_args a_arrow_b in 
   let left = 
     mkApp(delayed_force iter, 
 	  Array.of_list 
 	    (lift 5 a_arrow_b:: mkRel 3::
-	       constr_of_reference func::mkRel 1::
+	       constr_of_global func::mkRel 1::
 	       List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
 	    )
 	 )
@@ -798,7 +798,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
   begin 
     fun g -> 
       let ids = ids_of_named_context (pf_hyps g) in
-      let func_body = (def_of_const (constr_of_reference func)) in
+      let func_body = (def_of_const (constr_of_global func)) in
       let (f_name, _, body1) = destLambda func_body in
       let f_id =
 	match f_name with
@@ -864,7 +864,7 @@ let build_and_l l =
 	let c,tac,nb = f pl in 
 	mk_and p1 c, 
 	tclTHENS
-	  (apply (constr_of_reference conj_constr)) 
+	  (apply (constr_of_global conj_constr)) 
 	  [tclIDTAC;
 	   tac
 	  ],nb+1
@@ -1090,7 +1090,7 @@ let rec n_x_id ids n =
 let start_equation (f:global_reference) (term_f:global_reference) 
   (cont_tactic:identifier list -> tactic) g =
   let ids = pf_ids_of_hyps g in
-  let terminate_constr = constr_of_reference term_f in 
+  let terminate_constr = constr_of_global term_f in 
   let nargs = nb_prod (type_of_const terminate_constr) in 
   let x = n_x_id ids nargs in
   tclTHENLIST [
@@ -1136,7 +1136,7 @@ let rec introduce_all_values_eq cont_tac functional termine
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
            simpl_iter (onHyp heq2);
            unfold_in_hyp [([1], evaluable_of_global_reference 
-                             (reference_of_constr functional))]
+                             (global_of_constr functional))]
              (([], heq2), Tacexpr.InHyp);
            tclTHENS
 	     (fun gls -> 
@@ -1260,7 +1260,7 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
 	        fun g ->
 		  let ids = ids_of_named_context (pf_hyps g) in
 	          rec_leaf_eq termine f ids
-		    (constr_of_reference functional)
+		    (constr_of_global functional)
 		    eqs expr fn args g))
        | _ -> 
 	   (match find_call_occs 0 f expr with
@@ -1269,7 +1269,7 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
 		  fun g ->
 		    let ids = ids_of_named_context (pf_hyps g) in
 		    observe_tac "rec_leaf_eq" (rec_leaf_eq  
-		      termine f ids (constr_of_reference functional)
+		      termine f ids (constr_of_global functional)
 		      eqs expr fn args) g));;
 
 let (com_eqn : identifier ->
@@ -1285,7 +1285,7 @@ let (com_eqn : identifier ->
 	| _ -> anomaly "terminate_lemma: not a constant"
     in 
     let (evmap, env) = Command.get_current_context() in
-    let f_constr = (constr_of_reference f_ref) in
+    let f_constr = (constr_of_global f_ref) in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (start_proof eq_name (Global, Proof Lemma)
        (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
@@ -1293,12 +1293,12 @@ let (com_eqn : identifier ->
        (start_equation f_ref terminate_ref
 	  (fun  x ->
 	     prove_eq 
-	       (constr_of_reference terminate_ref)
+	       (constr_of_global terminate_ref)
 	       f_constr 
 	       functional_ref
 	       []
 	       (instantiate_lambda
-	       	  (def_of_const (constr_of_reference functional_ref))
+	       	  (def_of_const (constr_of_global functional_ref))
 	       	  (f_constr::List.map mkVar x)
 	       )
 	  )
@@ -1371,9 +1371,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     if not !stop
     then
       let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
-      let f_ref = destConst (constr_of_reference f_ref) 
-      and functional_ref = destConst (constr_of_reference functional_ref) 
-      and eq_ref = destConst (constr_of_reference eq_ref) in
+      let f_ref = destConst (constr_of_global f_ref) 
+      and functional_ref = destConst (constr_of_global functional_ref) 
+      and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
 	functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
       if Options.is_verbose ()
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 649db86ce..1cbae1e2f 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -565,7 +565,8 @@ type cst_tac_spec =
 let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
   match cst_tac with
       Some (CstTac t) -> Tacinterp.glob_tactic t
-    | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc)
+    | Some (Closed lc) ->
+        closed_term_ast (List.map Syntax_def.global_with_alias lc)
     | None ->
         (match rk, opp, kind with
             Abstract, None, _ ->
@@ -608,7 +609,8 @@ let interp_power env pow =
       let tac = 
         match tac with
         | CstTac t -> Tacinterp.glob_tactic t
-        | Closed lc -> closed_term_ast (List.map Nametab.global lc) in
+        | Closed lc ->
+            closed_term_ast (List.map Syntax_def.global_with_alias lc) in
       let spec = make_hyp env (ic spec) in
       (tac, lapp coq_Some [|carrier; spec|])
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 9cbfb0246..d7d304279 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -287,7 +287,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let fix_def =
     match measure_fn with
 	None ->
-	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
+	  mkApp (constr_of_global (Lazy.force fix_sub_ref), 
 		 [| argtyp ;
 		    wf_rel ;
 		    make_existential dummy_loc ~opaque:false env isevars wf_proof ;
@@ -295,7 +295,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		    lift lift_cst intern_body_lam |])
       | Some f ->
 	  lift (succ after_length) 
-	    (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
+	    (mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), 
 		    [| argtyp ; 
 		       f ;
 		       lift lift_cst prop ;
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 3769362b1..b81e7e6c8 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -79,14 +79,24 @@ let rec set_loc loc _ a =
 let search_syntactic_definition loc kn =
   set_loc loc () (KNmap.find kn !syntax_table)
 
-exception BoundToASyntacticDefThatIsNotARef
-
-let locate_global qid =
+let locate_global_with_alias (loc,qid) =
   match Nametab.extended_locate qid with
   | TrueGlobal ref -> ref
   | SyntacticDef kn -> 
   match search_syntactic_definition dummy_loc kn with
   | Rawterm.RRef (_,ref) -> ref
   | _ -> 
-      errorlabstrm "" (pr_qualid qid ++ 
+      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 =
+  match locate_global_with_alias (qualid_of_reference r) with
+  | IndRef ind -> ind
+  | ref ->
+      user_err_loc (loc_of_reference r,"global_inductive",
+        pr_reference r ++ spc () ++ str "is not an inductive type")
+
+let global_with_alias r =
+  let (loc,qid as lqid) = qualid_of_reference r in
+  try locate_global_with_alias lqid
+  with Not_found -> Nametab.error_global_not_found_loc loc qid
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 50f2f3e7d..e83cb8885 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,6 +13,7 @@ open Util
 open Names
 open Topconstr
 open Rawterm
+open Libnames
 (*i*)
 
 (* Syntactic definitions. *)
@@ -23,10 +24,16 @@ val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
 val search_syntactic_definition : loc -> kernel_name -> rawconstr
 
 
-(* [locate_global] locates global reference possibly following a chain of 
-   syntactic aliases; raise Not_found if not bound in the global env; 
-   raise an error if bound to a syntactic def that does not denote a
-   reference *)
+(* [locate_global_with_alias] locates global reference possibly following
+   a notation if this notation has a role of aliasing; raise Not_found
+   if not bound in the global env; raise an error if bound to a
+   syntactic def that does not denote a reference *)
 
-val locate_global : Libnames.qualid -> Libnames.global_reference
+val locate_global_with_alias : qualid located -> global_reference
+
+(* Locate a reference taking into account possible "alias" notations *)
+val global_with_alias : reference -> global_reference
+
+(* The same for inductive types *)
+val inductive_of_reference_with_alias : reference -> inductive
 
diff --git a/library/libnames.ml b/library/libnames.ml
index dcdd5ac41..4d25c42f9 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -49,8 +49,10 @@ let constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
+(*
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
+*)
 
 module RefOrdered =
   struct
diff --git a/library/libnames.mli b/library/libnames.mli
index fe5033d73..6c6d435be 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -34,9 +34,11 @@ val constr_of_global : global_reference -> constr
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> global_reference
 
+(*
 (* Obsolete synonyms for constr_of_global and global_of_constr *)
 val constr_of_reference : global_reference -> constr
 val reference_of_constr : constr -> global_reference
+*)
 
 module Refset : Set.S with type elt = global_reference 
 module Refmap : Map.S with type key = global_reference
diff --git a/library/nametab.ml b/library/nametab.ml
index ffca8bf4a..395b2159f 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -427,7 +427,7 @@ let global r =
     | TrueGlobal ref -> ref
     | SyntacticDef _ -> 
         user_err_loc (loc,"global",
-          str "Unexpected reference to a syntactic definition: " ++
+          str "Unexpected reference to a notation: " ++
           pr_qualid qid)
   with Not_found ->
     error_global_not_found_loc loc qid
@@ -497,7 +497,7 @@ let pr_global_env env ref =
   let s = string_of_qualid (shortest_qualid_of_global env ref) in
   (str s)
 
-let global_inductive r =
+let inductive_of_reference r =
   match global r with
   | IndRef ind -> ind
   | ref ->
diff --git a/library/nametab.mli b/library/nametab.mli
index 2f6e9e8cb..66de6a708 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -89,9 +89,9 @@ val locate : qualid -> global_reference
 val global : reference -> global_reference
 
 (* The same for inductive types *)
-val global_inductive : reference -> inductive
+val inductive_of_reference : reference -> inductive
 
-(* This locates also syntactic definitions *)
+(* This locates also syntactic definitions; raise [Not_found] if not found *)
 val extended_locate : qualid -> extended_global_reference
 
 (* This locates all names with a given suffix, if qualid is valid as
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 49147dfd7..9a628b3fd 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -370,8 +370,8 @@ let classes () = Bijint.dom !class_tab
 let coercions () = Gmap.rng !coercion_tab
 let inheritance_graph () = Gmap.to_list !inheritance_graph
 
-let coercion_of_qualid qid =
-  let ref = Nametab.global qid in
+let coercion_of_reference r =
+  let ref = Nametab.global r in
   if not (coercion_exists ref) then
     errorlabstrm "try_add_coercion" 
       (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion");
@@ -380,7 +380,7 @@ let coercion_of_qualid qid =
 module CoercionPrinting =
   struct
     type t = coe_typ
-    let encode = coercion_of_qualid
+    let encode = coercion_of_reference
     let subst = subst_coe_typ
     let printer x = pr_global_env Idset.empty x
     let key = Goptions.SecondaryTable ("Printing","Coercion")
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 049c93641..829c5f404 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -31,8 +31,8 @@ let dl = dummy_loc
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
-let encode_inductive qid =
-  let indsp = global_inductive qid in
+let encode_inductive r =
+  let indsp = inductive_of_reference r in
   let constr_lengths = mis_constr_nargs indsp in
   (indsp,constr_lengths)
 
@@ -108,13 +108,6 @@ module PrintingCasesLet =
 module PrintingIf  = Goptions.MakeRefTable(PrintingCasesIf)
 module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet)
 
-let force_let ci =
-  let indsp = ci.ci_ind in
-  let lc = mis_constr_nargs indsp in PrintingLet.active (indsp,lc)
-let force_if ci =
-  let indsp = ci.ci_ind in
-  let lc = mis_constr_nargs indsp in PrintingIf.active (indsp,lc)
-
 (* Options for printing or not wildcard and synthetisable types *)
 
 open Goptions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 445c2183d..588bc8c84 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -50,8 +50,6 @@ val lookup_index_as_renamed : env -> constr -> int -> int option
 val set_detype_anonymous : (loc -> int -> rawconstr) -> unit
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
-val force_if : case_info -> bool
-val force_let : case_info -> bool
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
 
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
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0b9f76d95..99f9e3ed7 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 1eb1f8986..784cabcd5 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 67ba2bd52..4a200591e 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