Remove reference name type.

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.

14 files changed, 123 insertions, 128 deletions

diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 642e52155..35ed14fc1 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -173,7 +173,7 @@ TACTIC EXTEND convert_concl_no_check
 | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ]
 END
 
-let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
+let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
 let glob_hints_path_atom ist = Hints.glob_hints_path_atom
 
@@ -189,7 +189,7 @@ ARGUMENT EXTEND hints_path_atom
 END
 
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
-let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c
+let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c
 let glob_hints_path ist = Hints.glob_hints_path
 
 ARGUMENT EXTEND hints_path
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index d7d642e50..620f14707 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -39,11 +39,12 @@ let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
 let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
-let reference_to_id = CAst.map_with_loc (fun ?loc -> function
-  | Libnames.Ident id -> id
-  | Libnames.Qualid _ ->
-    CErrors.user_err ?loc
-      (str "This expression should be a simple identifier."))
+let reference_to_id qid =
+  if Libnames.qualid_is_ident qid then
+    CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid
+  else
+    CErrors.user_err ?loc:qid.CAst.loc
+      (str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 
@@ -199,8 +200,7 @@ GEXTEND Gram
      verbose most of the time. *)
   fresh_id:
     [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*)
-        | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in
-                          Locus.ArgVar (CAst.make ~loc:!@loc id) ] ]
+        | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -475,7 +475,7 @@ END
 
 VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
 | [ "Print" "Ltac" reference(r) ] ->
-  [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ]
+  [ Feedback.msg_notice (Tacintern.print_ltac r) ]
 END
 
 VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
@@ -483,7 +483,7 @@ VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
   [ Tacentries.print_located_tactic r ]
 END
 
-let pr_ltac_ref = Libnames.pr_reference
+let pr_ltac_ref = Libnames.pr_qualid
 
 let pr_tacdef_body tacdef_body =
   let id, redef, body =
@@ -510,8 +510,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
 | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
-      | TacticRedefinition ({CAst.v=Ident r},_) -> r
-      | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater
+      | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
   ] -> [ fun ~atts ~st -> let open Vernacinterp in
            Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
            st
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 352e92c2a..1f56244c7 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,6 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
 
-open Libnames
 open Constrexpr
 open Constrexpr_ops
 open Stdarg
@@ -49,7 +48,7 @@ module Tactic = Pltac
 
 open Pcoq
 
-let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig")
 
 type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
 
@@ -68,7 +67,7 @@ GEXTEND Gram
 
   Constr.closed_binder:
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
-	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+          let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in
           [CLocalAssum ([id], default_binder_kind, typ)]
     ] ];
 
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 2189e224f..f1634f156 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -67,13 +67,13 @@ let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
 let pr_raw_strategy prc prlc _ (s : raw_strategy) =
-  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in
+  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
   Rewrite.pr_strategy prc prr s
 let pr_glob_strategy prc prlc _ (s : glob_strategy) =
   let prr = Pptactic.pr_red_expr
     (Ppconstr.pr_constr_expr,
     Ppconstr.pr_lconstr_expr,
-    Pputils.pr_or_by_notation Libnames.pr_reference,
+    Pputils.pr_or_by_notation Libnames.pr_qualid,
     Ppconstr.pr_constr_expr)
   in
   Rewrite.pr_strategy prc prr s
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 05005c733..31bc34a32 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -156,7 +156,7 @@ let mkTacCase with_evar = function
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
-      TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings)))
+      TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings)))
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 4c075d413..c5aa542fd 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -21,8 +21,8 @@ val open_constr : constr_expr Gram.entry
 val constr_with_bindings : constr_expr with_bindings Gram.entry
 val bindings : constr_expr bindings Gram.entry
 val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
-val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
-val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
+val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
 val uconstr : constr_expr Gram.entry
 val quantified_hypothesis : quantified_hypothesis Gram.entry
 val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e19a95e84..09179dad3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -17,7 +17,6 @@ open Constrexpr
 open Genarg
 open Geninterp
 open Stdarg
-open Libnames
 open Notation_gram
 open Tactypes
 open Locus
@@ -1109,8 +1108,8 @@ let pr_goal_selector ~toplevel s =
       pr_lconstr = pr_lconstr_expr;
       pr_pattern = pr_constr_pattern_expr;
       pr_lpattern = pr_lconstr_pattern_expr;
-      pr_constant = pr_or_by_notation pr_reference;
-      pr_reference = pr_reference;
+      pr_constant = pr_or_by_notation pr_qualid;
+      pr_reference = pr_qualid;
       pr_name = pr_lident;
       pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
       pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
@@ -1323,7 +1322,7 @@ let () =
   let open Genprint in
   register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
   register_basic_print0 wit_ref
-    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+    pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
   register_basic_print0 wit_ident pr_id pr_id pr_id;
   register_basic_print0 wit_var pr_lident pr_lident pr_id;
   register_print0
@@ -1357,7 +1356,7 @@ let () =
   ;
   Genprint.register_print0
     wit_red_expr
-    (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)))
+    (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr)))
     (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)))
     pr_red_expr_env
   ;
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index cd04f4ae9..01c52c413 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1773,11 +1773,11 @@ let rec strategy_of_ast = function
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
-let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l)
 
 let declare_an_instance n s args =
   (((CAst.make @@ Name n),None), Explicit,
-   CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args))
+   CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
@@ -1791,17 +1791,17 @@ let anew_instance global binders instance fields =
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
   in anew_instance global binders instance
-       [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)]
+       [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance global binders instance
-       [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)]
+       [(qualid_of_ident (Id.of_string "symmetry"),lemma)]
 
 let declare_instance_trans global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
   in anew_instance global binders instance
-       [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)]
+       [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
 let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
@@ -1825,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
 	    anew_instance global binders instance
-              [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1);
-               (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)])
+              [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+               (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
 	    anew_instance global binders instance
-              [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2);
-               (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)])
+              [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
+               (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
 	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1842,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
 	  anew_instance global binders instance
-            [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1);
-             (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2);
-             (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)])
+            [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+             (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+             (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)])
 
 let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
@@ -1949,16 +1949,15 @@ let add_setoid global binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance global binders instance
-      [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+      [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 
 let make_tactic name =
   let open Tacexpr in
-  let tacpath = Libnames.qualid_of_string name in
-  let tacname = CAst.make @@ Qualid tacpath in
-  TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, []))))
+  let tacqid = Libnames.qualid_of_string name in
+  TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, []))))
 
 let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
@@ -2008,7 +2007,7 @@ let add_morphism glob binders m s n =
   let instance =
     (((CAst.make @@ Name instance_id),None), Explicit,
     CAst.make @@ CAppExpl (
-             (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
+             (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fada7424c..98d451536 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -449,12 +449,12 @@ let register_ltac local tacl =
         in
         let () = if is_shadowed then warn_unusable_identifier id in
         NewTac id, body
-    | Tacexpr.TacticRedefinition (ident, body) ->
+    | Tacexpr.TacticRedefinition (qid, body) ->
         let kn =
-          try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v
+          try Tacenv.locate_tactic qid
           with Not_found ->
-            CErrors.user_err ?loc:ident.CAst.loc
-                       (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+            CErrors.user_err ?loc:qid.CAst.loc
+                       (str "There is no Ltac named " ++ pr_qualid qid ++ str ".")
         in
         UpdateTac kn, body
   in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 3f804ee8d..2bfbbe2e1 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -65,7 +65,7 @@ val create_ltac_quotation : string ->
 val print_ltacs : unit -> unit
 (** Display the list of ltac definitions currently available. *)
 
-val print_located_tactic : Libnames.reference -> unit
+val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
 type _ ty_sig =
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index d51de8c65..06d2711ad 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -333,8 +333,8 @@ type glob_tactic_arg =
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
-type r_ref = reference
+type r_cst = qualid or_by_notation
+type r_ref = qualid
 type r_nam = lident
 type r_lev = rlevel
 
@@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
   | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 01eead164..71e1edfd7 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -333,8 +333,8 @@ type glob_tactic_arg =
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
-type r_ref = reference
+type r_cst = qualid or_by_notation
+type r_ref = qualid
 type r_nam = lident
 type r_lev = rlevel
 
@@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
   | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index cef5bb1b8..481fc30df 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -92,88 +92,83 @@ let intern_or_var f ist = function
 let intern_int_or_var = intern_or_var (fun (n : int) -> n)
 let intern_string_or_var = intern_or_var (fun (s : string) -> s)
 
-let intern_global_reference ist = function
-  | {CAst.loc;v=Ident id} when find_var id ist ->
-    ArgVar (make ?loc id)
-  | r ->
-    let {CAst.loc} as lqid = qualid_of_reference r in
-    try ArgArg (loc,locate_global_with_alias lqid)
-    with Not_found -> error_global_not_found lqid
-
-let intern_ltac_variable ist = function
-  | {loc;v=Ident id} ->
-      if find_var id ist then
-	(* A local variable of any type *)
-        ArgVar (make ?loc id)
-      else raise Not_found
-  | _ ->
-      raise Not_found
-
-let intern_constr_reference strict ist = function
-  | {v=Ident id} as r when not strict && find_hyp id ist ->
-      (DAst.make @@ GVar id), Some (make @@ CRef (r,None))
-  | {v=Ident id} as r when find_var id ist ->
-      (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None))
-  | r ->
-      let {loc} as lqid = qualid_of_reference r in
-      DAst.make @@ GRef (locate_global_with_alias lqid,None), 
-        if strict then None else Some (make @@ CRef (r,None))
+let intern_global_reference ist qid =
+  if qualid_is_ident qid && find_var (qualid_basename qid) ist then
+    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
+  else
+    try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
+    with Not_found -> error_global_not_found qid
+
+let intern_ltac_variable ist qid =
+  if qualid_is_ident qid && find_var (qualid_basename qid) ist then
+    (* A local variable of any type *)
+    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
+  else raise Not_found
+
+let intern_constr_reference strict ist qid =
+  let id = qualid_basename qid in
+  if qualid_is_ident qid && not strict && find_hyp (qualid_basename qid) ist then
+    (DAst.make @@ GVar id), Some (make @@ CRef (qid,None))
+  else if qualid_is_ident qid && find_var (qualid_basename qid) ist then
+    (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (qid,None))
+  else
+    DAst.make @@ GRef (locate_global_with_alias qid,None),
+    if strict then None else Some (make @@ CRef (qid,None))
 
 (* Internalize an isolated reference in position of tactic *)
 
-let intern_isolated_global_tactic_reference r =
-  let {loc;v=qid} = qualid_of_reference r in
+let intern_isolated_global_tactic_reference qid =
+  let loc = qid.CAst.loc in
   TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
 
-let intern_isolated_tactic_reference strict ist r =
+let intern_isolated_tactic_reference strict ist qid =
   (* An ltac reference *)
-  try Reference (intern_ltac_variable ist r)
+  try Reference (intern_ltac_variable ist qid)
   with Not_found ->
   (* A global tactic *)
-  try intern_isolated_global_tactic_reference r
+  try intern_isolated_global_tactic_reference qid
   with Not_found ->
   (* Tolerance for compatibility, allow not to use "constr:" *)
-  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found (qualid_of_reference r)
+  error_global_not_found qid
 
 (* Internalize an applied tactic reference *)
 
-let intern_applied_global_tactic_reference r =
-  let {loc;v=qid} = qualid_of_reference r in
-  ArgArg (loc,Tacenv.locate_tactic qid)
+let intern_applied_global_tactic_reference qid =
+  ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid)
 
-let intern_applied_tactic_reference ist r =
+let intern_applied_tactic_reference ist qid =
   (* An ltac reference *)
-  try intern_ltac_variable ist r
+  try intern_ltac_variable ist qid
   with Not_found ->
   (* A global tactic *)
-  try intern_applied_global_tactic_reference r
+  try intern_applied_global_tactic_reference qid
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found (qualid_of_reference r)
+  error_global_not_found qid
 
 (* Intern a reference parsed in a non-tactic entry *)
 
-let intern_non_tactic_reference strict ist r =
+let intern_non_tactic_reference strict ist qid =
   (* An ltac reference *)
-  try Reference (intern_ltac_variable ist r)
+  try Reference (intern_ltac_variable ist qid)
   with Not_found ->
   (* A constr reference *)
-  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
   with Not_found ->
   (* Tolerance for compatibility, allow not to use "ltac:" *)
-  try intern_isolated_global_tactic_reference r
+  try intern_isolated_global_tactic_reference qid
   with Not_found ->
   (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
-  match r with
-  | {loc;v=Ident id} when not strict ->
-    let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in
+  if qualid_is_ident qid && not strict then
+    let id = qualid_basename qid in
+    let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in
     TacGeneric ipat
-  | _ ->
-  (* Reference not found *)
-  error_global_not_found (qualid_of_reference r)
+  else
+    (* Reference not found *)
+    error_global_not_found qid
 
 let intern_message_token ist = function
   | (MsgString _ | MsgInt _ as x) -> x
@@ -269,7 +264,7 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent {loc;v=id} ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-        let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in
+        let c, p = intern_constr ist (make @@ CRef (qualid_of_ident id, None)) in
 	match DAst.get c with
         | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id)
 	| _ -> clear,ElimOnConstr ((c, p), NoBindings)
@@ -277,16 +272,15 @@ let intern_destruction_arg ist = function
         clear,ElimOnIdent (make ?loc id)
 
 let short_name = function
-  | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id)
+  | {v=AN qid} when qualid_is_ident qid && not !strict_check ->
+    Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
   | _ -> None
 
-let intern_evaluable_global_reference ist r =
-  let lqid = qualid_of_reference r in
-  try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid)
+let intern_evaluable_global_reference ist qid =
+  try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
   with Not_found ->
-  match r with
-  | {loc;v=Ident id} when not !strict_check -> EvalVarRef id
-  | _ -> error_global_not_found lqid
+  if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
+  else error_global_not_found qid
 
 let intern_evaluable_reference_or_by_notation ist = function
   | {v=AN r} -> intern_evaluable_global_reference ist r
@@ -296,14 +290,19 @@ let intern_evaluable_reference_or_by_notation ist = function
         (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalize a reduction expression *)
-let intern_evaluable ist = function
-  | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id)
-  | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist ->
-      ArgArg (EvalVarRef id, Some (make ?loc id))
-  | r ->
-      let e = intern_evaluable_reference_or_by_notation ist r in
-      let na = short_name r in
-      ArgArg (e,na)
+let intern_evaluable ist r =
+  let f ist r =
+    let e = intern_evaluable_reference_or_by_notation ist r in
+    let na = short_name r in
+    ArgArg (e,na)
+  in
+  match r with
+  | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist ->
+    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
+  | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist ->
+    let id = qualid_basename qid in
+      ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id))
+  | _ -> f ist r
 
 let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
 
@@ -356,7 +355,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
          subterm matched when a pattern *)
       let r = match r with
       | {v=AN r} -> r
-      | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in
+      | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in
       let sign = {
         Constrintern.ltac_vars = ist.ltacvars;
         ltac_bound = Id.Set.empty;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 04dd7d6e9..9d1cc1643 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -361,7 +361,7 @@ let interp_reference ist env sigma = function
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
-      with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+      with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
@@ -377,14 +377,14 @@ let interp_evaluable ist env sigma = function
       with Not_found ->
         match r with
         | EvalConstRef _ -> r
-        | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+        | _ -> error_global_not_found (qualid_of_ident ?loc id)
     end
   | ArgArg (r,None) -> r
   | ArgVar {loc;v=id} ->
     try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
-      with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+      with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -643,7 +643,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
         Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
      with Not_found ->
-       error_global_not_found (make ?loc @@ qualid_of_ident id))
+       error_global_not_found (qualid_of_ident ?loc id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
@@ -925,7 +925,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (make ?loc id)
 	else
-          let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in
+          let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in
           let f env sigma =
             let (sigma,c) = interp_open_constr ist env sigma c in
             (sigma, (c,NoBindings))