Adapt to Coq's PR #7797 (removal of reference).

10 files changed, 63 insertions, 70 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index b13c036549..16e7278235 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -98,25 +98,25 @@ let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c
 let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c
 let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e
 
-let pattern_of_qualid ?loc id =
-  if Tac2env.is_constructor id.CAst.v then CAst.make ?loc @@ CPatRef (RelId id, [])
+let pattern_of_qualid qid =
+  if Tac2env.is_constructor qid then CAst.make ?loc:qid.CAst.loc @@ CPatRef (RelId qid, [])
   else
-    let (dp, id) = Libnames.repr_qualid id.CAst.v in
-    if DirPath.is_empty dp then CAst.make ?loc @@ CPatVar (Name id)
+    let open Libnames in
+    if qualid_is_ident qid then CAst.make ?loc:qid.CAst.loc @@ CPatVar (Name (qualid_basename qid))
     else
-      CErrors.user_err ?loc (Pp.str "Syntax error")
+      CErrors.user_err ?loc:qid.CAst.loc (Pp.str "Syntax error")
 
 GEXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
           tac2def_mut tac2def_run;
   tac2pat:
     [ "1" LEFTA
-      [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
-        if Tac2env.is_constructor (id.CAst.v) then
-          CAst.make ~loc:!@loc @@ CPatRef (RelId id, pl)
+      [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
+        if Tac2env.is_constructor qid then
+          CAst.make ~loc:!@loc @@ CPatRef (RelId qid, pl)
         else
           CErrors.user_err ~loc:!@loc (Pp.str "Syntax error")
-      | id = Prim.qualid -> pattern_of_qualid ~loc:!@loc id
+      | qid = Prim.qualid -> pattern_of_qualid qid
       | "["; "]" -> CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_nil), [])
       | p1 = tac2pat; "::"; p2 = tac2pat ->
         CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_cons), [p1; p2])
@@ -124,7 +124,7 @@ GEXTEND Gram
     | "0"
       [ "_" -> CAst.make ~loc:!@loc @@ CPatVar Anonymous
       | "()" -> CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
-      | id = Prim.qualid -> pattern_of_qualid ~loc:!@loc id
+      | qid = Prim.qualid -> pattern_of_qualid qid
       | "("; p = atomic_tac2pat; ")" -> p
     ] ]
   ;
@@ -205,11 +205,11 @@ GEXTEND Gram
   tactic_atom:
     [ [ n = Prim.integer -> CAst.make ~loc:!@loc @@ CTacAtm (AtmInt n)
       | s = Prim.string -> CAst.make ~loc:!@loc @@ CTacAtm (AtmStr s)
-      | id = Prim.qualid ->
-        if Tac2env.is_constructor id.CAst.v then
-          CAst.make ~loc:!@loc @@ CTacCst (RelId id)
+      | qid = Prim.qualid ->
+        if Tac2env.is_constructor qid then
+          CAst.make ~loc:!@loc @@ CTacCst (RelId qid)
         else
-          CAst.make ~loc:!@loc @@ CTacRef (RelId id)
+          CAst.make ~loc:!@loc @@ CTacRef (RelId qid)
       | "@"; id = Prim.ident -> Tac2quote.of_ident (CAst.make ~loc:!@loc id)
       | "&"; id = lident -> Tac2quote.of_hyp ~loc:!@loc id
       | "'"; c = Constr.constr -> inj_open_constr !@loc c
@@ -372,7 +372,7 @@ GEXTEND Gram
   ;
   globref:
     [ [ "&"; id = Prim.ident -> CAst.make ~loc:!@loc (QHypothesis id)
-      | qid = Prim.qualid -> CAst.map (fun qid -> QReference qid) qid
+      | qid = Prim.qualid -> CAst.make ~loc:!@loc @@ QReference qid
     ] ]
   ;
 END
@@ -667,7 +667,7 @@ GEXTEND Gram
   ;
   refglobal:
     [ [ "&"; id = Prim.ident -> QExpr (CAst.make ~loc:!@loc @@ QHypothesis id)
-      | qid = Prim.qualid -> QExpr (CAst.make ~loc:!@loc @@ QReference qid.CAst.v)
+      | qid = Prim.qualid -> QExpr (CAst.make ~loc:!@loc @@ QReference qid)
       | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id)
     ] ]
   ;
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 4bd294d4df..97f25ef5ed 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -917,8 +917,7 @@ let () =
     let gr =
       try Nametab.locate qid
       with Not_found ->
-        let loc = ref.CAst.loc in
-        Nametab.error_global_not_found (CAst.make ?loc qid)
+        Nametab.error_global_not_found qid
     in
     GlbVal gr, gtypref t_reference
   in
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index c85ffb2539..8ebfeec948 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -303,7 +303,7 @@ let inline_rec_tactic tactics =
     let bnd = List.map map_body tactics in
     let pat_of_id {loc;v=id} = CAst.make ?loc @@ CPatVar (Name id) in
     let var_of_id {loc;v=id} =
-      let qid = CAst.make ?loc @@ qualid_of_ident id in
+      let qid = qualid_of_ident ?loc id in
       CAst.make ?loc @@ CTacRef (RelId qid)
     in
     let loc0 = e.loc in
@@ -360,10 +360,9 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
   in
   List.iter iter defs
 
-let qualid_to_ident {loc;v=qid} =
-  let (dp, id) = Libnames.repr_qualid qid in
-  if DirPath.is_empty dp then CAst.make ?loc id
-  else user_err ?loc (str "Identifier expected")
+let qualid_to_ident qid =
+  if qualid_is_ident qid then CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid
+  else user_err ?loc:qid.CAst.loc (str "Identifier expected")
 
 let register_typedef ?(local = false) isrec types =
   let same_name ({v=id1}, _) ({v=id2}, _) = Id.equal id1 id2 in
@@ -453,21 +452,21 @@ let register_primitive ?(local = false) {loc;v=id} t ml =
   } in
   ignore (Lib.add_leaf id (inTacDef def))
 
-let register_open ?(local = false) {loc;v=qid} (params, def) =
+let register_open ?(local = false) qid (params, def) =
   let kn =
     try Tac2env.locate_type qid
     with Not_found ->
-      user_err ?loc (str "Unbound type " ++ pr_qualid qid)
+      user_err ?loc:qid.CAst.loc (str "Unbound type " ++ pr_qualid qid)
   in
   let (tparams, t) = Tac2env.interp_type kn in
   let () = match t with
   | GTydOpn -> ()
   | GTydAlg _ | GTydRec _ | GTydDef _ ->
-    user_err ?loc (str "Type " ++ pr_qualid qid ++ str " is not an open type")
+    user_err ?loc:qid.CAst.loc (str "Type " ++ pr_qualid qid ++ str " is not an open type")
   in
   let () =
     if not (Int.equal (List.length params) tparams) then
-      Tac2intern.error_nparams_mismatch ?loc (List.length params) tparams
+      Tac2intern.error_nparams_mismatch ?loc:qid.CAst.loc (List.length params) tparams
   in
   match def with
   | CTydOpn -> ()
@@ -492,12 +491,11 @@ let register_open ?(local = false) {loc;v=qid} (params, def) =
     } in
     Lib.add_anonymous_leaf (inTypExt def)
   | CTydRec _ | CTydDef _ ->
-    user_err ?loc (str "Extensions only accept inductive constructors")
+    user_err ?loc:qid.CAst.loc (str "Extensions only accept inductive constructors")
 
 let register_type ?local isrec types = match types with
 | [qid, true, def] ->
-  let {loc} = qid in
-  let () = if isrec then user_err ?loc (str "Extensions cannot be recursive") in
+  let () = if isrec then user_err ?loc:qid.CAst.loc (str "Extensions cannot be recursive") in
   register_open ?local qid def
 | _ ->
   let map (qid, redef, def) =
@@ -709,30 +707,30 @@ let inTac2Redefinition : redefinition -> obj =
      subst_function = subst_redefinition;
      classify_function = classify_redefinition }
 
-let register_redefinition ?(local = false) (loc, qid) e =
+let register_redefinition ?(local = false) qid e =
   let kn =
     try Tac2env.locate_ltac qid
-    with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
+    with Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown tactic " ++ pr_qualid qid)
   in
   let kn = match kn with
   | TacConstant kn -> kn
   | TacAlias _ ->
-    user_err ?loc (str "Cannot redefine syntactic abbreviations")
+    user_err ?loc:qid.CAst.loc (str "Cannot redefine syntactic abbreviations")
   in
   let data = Tac2env.interp_global kn in
   let () =
     if not (data.Tac2env.gdata_mutable) then
-      user_err ?loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable")
+      user_err ?loc:qid.CAst.loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable")
   in
   let (e, t) = intern ~strict:true e in
   let () =
     if not (is_value e) then
-      user_err ?loc (str "Tactic definition must be a syntactical value")
+      user_err ?loc:qid.CAst.loc (str "Tactic definition must be a syntactical value")
   in
   let () =
     if not (Tac2intern.check_subtype t data.Tac2env.gdata_type) then
       let name = int_name () in
-      user_err ?loc (str "Type " ++ pr_glbtype name (snd t) ++
+      user_err ?loc:qid.CAst.loc (str "Type " ++ pr_glbtype name (snd t) ++
         str " is not a subtype of " ++ pr_glbtype name (snd data.Tac2env.gdata_type))
   in
   let def = {
@@ -779,7 +777,7 @@ let register_struct ?local str = match str with
 | StrTyp (isrec, t) -> register_type ?local isrec t
 | StrPrm (id, t, ml) -> register_primitive ?local id t ml
 | StrSyn (tok, lev, e) -> register_notation ?local tok lev e
-| StrMut (qid, e) -> register_redefinition ?local CAst.(qid.loc, qid.v) e
+| StrMut (qid, e) -> register_redefinition ?local qid e
 | StrRun e -> perform_eval e
 
 (** Toplevel exception *)
@@ -831,19 +829,18 @@ end
 
 (** Printing *)
 
-let print_ltac ref =
-  let {loc;v=qid} = qualid_of_reference ref in
+let print_ltac qid =
   if Tac2env.is_constructor qid then
     let kn =
       try Tac2env.locate_constructor qid
-      with Not_found -> user_err ?loc (str "Unknown constructor " ++ pr_qualid qid)
+      with Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown constructor " ++ pr_qualid qid)
     in
     let _ = Tac2env.interp_constructor kn in
     Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid))
   else
     let kn =
       try Tac2env.locate_ltac qid
-      with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
+      with Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown tactic " ++ pr_qualid qid)
     in
     match kn with
     | TacConstant kn ->
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 777f3f1a43..37944981d7 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -16,7 +16,7 @@ val register_ltac : ?local:bool -> ?mut:bool -> rec_flag ->
   (Names.lname * raw_tacexpr) list -> unit
 
 val register_type : ?local:bool -> rec_flag ->
-  (qualid CAst.t * redef_flag * raw_quant_typedef) list -> unit
+  (qualid * redef_flag * raw_quant_typedef) list -> unit
 
 val register_primitive : ?local:bool ->
   Names.lident -> raw_typexpr -> ml_tactic_name -> unit
@@ -41,7 +41,7 @@ val parse_scope : sexpr -> scope_rule
 
 (** {5 Inspecting} *)
 
-val print_ltac : Libnames.reference -> unit
+val print_ltac : Libnames.qualid -> unit
 
 (** {5 Eval loop} *)
 
diff --git a/src/tac2env.ml b/src/tac2env.ml
index d0f286b396..dcf7440498 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -208,10 +208,10 @@ let locate_extended_all_type qid =
   let tab = !nametab in
   KnTab.find_prefixes qid tab.tab_type
 
-let shortest_qualid_of_type kn =
+let shortest_qualid_of_type ?loc kn =
   let tab = !nametab in
   let sp = KNmap.find kn tab.tab_type_rev in
-  KnTab.shortest_qualid Id.Set.empty sp tab.tab_type
+  KnTab.shortest_qualid ?loc Id.Set.empty sp tab.tab_type
 
 let push_projection vis sp kn =
   let tab = !nametab in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 022c518143..7616579d63 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -88,7 +88,7 @@ val shortest_qualid_of_constructor : ltac_constructor -> qualid
 val push_type : visibility -> full_path -> type_constant -> unit
 val locate_type : qualid -> type_constant
 val locate_extended_all_type : qualid -> type_constant list
-val shortest_qualid_of_type : type_constant -> qualid
+val shortest_qualid_of_type : ?loc:Loc.t -> type_constant -> qualid
 
 val push_projection : visibility -> full_path -> ltac_projection -> unit
 val locate_projection : qualid -> ltac_projection
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 1f2c3ebf3b..1069d0bfa3 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -26,7 +26,7 @@ type tacref =
 | TacAlias of ltac_alias
 
 type 'a or_relid =
-| RelId of qualid CAst.t
+| RelId of qualid
 | AbsKn of 'a
 
 (** {5 Misc} *)
@@ -160,13 +160,13 @@ type sexpr =
 type strexpr =
 | StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
   (** Term definition *)
-| StrTyp of rec_flag * (qualid CAst.t * redef_flag * raw_quant_typedef) list
+| StrTyp of rec_flag * (qualid * redef_flag * raw_quant_typedef) list
   (** Type definition *)
 | StrPrm of Names.lident * raw_typexpr * ml_tactic_name
   (** External definition *)
 | StrSyn of sexpr list * int option * raw_tacexpr
   (** Syntactic extensions *)
-| StrMut of qualid CAst.t * raw_tacexpr
+| StrMut of qualid * raw_tacexpr
   (** Redefinition of mutable globals *)
 | StrRun of raw_tacexpr
   (** Toplevel evaluation of an expression *)
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 86d81ef5d2..f3b222df21 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -208,9 +208,9 @@ let rec intern_type env ({loc;v=t} : raw_typexpr) : UF.elt glb_typexpr = match t
 | CTypVar Anonymous -> GTypVar (fresh_id env)
 | CTypRef (rel, args) ->
   let (kn, nparams) = match rel with
-  | RelId {loc;v=qid} ->
-    let (dp, id) = repr_qualid qid in
-    if DirPath.is_empty dp && Id.Map.mem id env.env_rec then
+  | RelId qid ->
+    let id = qualid_basename qid in
+    if qualid_is_ident qid && Id.Map.mem id env.env_rec then
       let (kn, n) = Id.Map.find id env.env_rec in
       (Other kn, n)
     else
@@ -230,9 +230,9 @@ let rec intern_type env ({loc;v=t} : raw_typexpr) : UF.elt glb_typexpr = match t
   let nargs = List.length args in
   let () =
     if not (Int.equal nparams nargs) then
-      let {loc;v=qid} = match rel with
+      let qid = match rel with
       | RelId lid -> lid
-      | AbsKn (Other kn) -> CAst.make ?loc @@ shortest_qualid_of_type kn
+      | AbsKn (Other kn) -> shortest_qualid_of_type ?loc kn
       | AbsKn (Tuple _) -> assert false
       in
       user_err ?loc (strbrk "The type constructor " ++ pr_qualid qid ++
@@ -500,14 +500,14 @@ let check_redundant_clause = function
 | (p, _) :: _ -> warn_redundant_clause ?loc:p.loc ()
 
 let get_variable0 mem var = match var with
-| RelId {loc;v=qid} ->
-  let (dp, id) = repr_qualid qid in
-  if DirPath.is_empty dp && mem id then ArgVar CAst.(make ?loc id)
+| RelId qid ->
+  let id = qualid_basename qid in
+  if qualid_is_ident qid && mem id then ArgVar CAst.(make ?loc:qid.CAst.loc id)
   else
     let kn =
       try Tac2env.locate_ltac qid
       with Not_found ->
-        CErrors.user_err ?loc (str "Unbound value " ++ pr_qualid qid)
+        CErrors.user_err ?loc:qid.CAst.loc (str "Unbound value " ++ pr_qualid qid)
     in
     ArgArg kn
 | AbsKn kn -> ArgArg kn
@@ -517,19 +517,19 @@ let get_variable env var =
   get_variable0 mem var
 
 let get_constructor env var = match var with
-| RelId {loc;v=qid} ->
+| RelId qid ->
   let c = try Some (Tac2env.locate_constructor qid) with Not_found -> None in
   begin match c with
   | Some knc -> Other knc
   | None ->
-    CErrors.user_err ?loc (str "Unbound constructor " ++ pr_qualid qid)
+    CErrors.user_err ?loc:qid.CAst.loc (str "Unbound constructor " ++ pr_qualid qid)
   end
 | AbsKn knc -> knc
 
 let get_projection var = match var with
-| RelId {loc;v=qid} ->
+| RelId qid ->
   let kn = try Tac2env.locate_projection qid with Not_found ->
-    user_err ?loc (pr_qualid qid ++ str " is not a projection")
+    user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is not a projection")
   in
   Tac2env.interp_projection kn
 | AbsKn kn ->
@@ -622,7 +622,7 @@ let expand_pattern avoid bnd =
       na, None
     | _ ->
       let id = fresh_var avoid in
-      let qid = RelId (CAst.make ?loc:pat.loc (qualid_of_ident id)) in
+      let qid = RelId (qualid_of_ident ?loc:pat.loc id) in
       Name id, Some qid
     in
     let avoid = ids_of_pattern avoid pat in
@@ -1206,9 +1206,9 @@ let check_subtype t1 t2 =
 (** Globalization *)
 
 let get_projection0 var = match var with
-| RelId {CAst.loc;v=qid} ->
+| RelId qid ->
   let kn = try Tac2env.locate_projection qid with Not_found ->
-    user_err ?loc (pr_qualid qid ++ str " is not a projection")
+    user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is not a projection")
   in
   kn
 | AbsKn kn -> kn
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 2a0230b779..1d742afd83 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -82,10 +82,10 @@ let inj_wit ?loc wit x =
   CAst.make ?loc @@ CTacExt (wit, x)
 
 let of_variable {loc;v=id} =
-  let qid = Libnames.qualid_of_ident id in
+  let qid = Libnames.qualid_of_ident ?loc id in
   if Tac2env.is_constructor qid then
     CErrors.user_err ?loc (str "Invalid identifier")
-  else CAst.make ?loc @@ CTacRef (RelId (CAst.make ?loc qid))
+  else CAst.make ?loc @@ CTacRef (RelId qid)
 
 let of_anti f = function
 | QExpr x -> f x
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 2ce347f397..09aa92f9ee 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -90,9 +90,6 @@ val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag
 val wit_ident : (Id.t, Id.t) Arg.tag
 
 val wit_reference : (reference, GlobRef.t) Arg.tag
-(** Beware, at the raw level, [Qualid [id]] has not the same meaning as
-    [Ident id]. The first is an unqualified global reference, the second is
-    the dynamic reference to id. *)
 
 val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag