[coq] Adapt to coq/coq#6745

Nothing remarkable.

4 files changed, 7 insertions, 7 deletions

diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 9afdb3aedc..dc142043e8 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -505,7 +505,7 @@ let check_redundant_clause = function
 let get_variable0 mem var = match var with
 | RelId (loc, qid) ->
   let (dp, id) = repr_qualid qid in
-  if DirPath.is_empty dp && mem id then ArgVar (loc, id)
+  if DirPath.is_empty dp && mem id then ArgVar CAst.(make ?loc id)
   else
     let kn =
       try Tac2env.locate_ltac qid
@@ -652,7 +652,7 @@ let rec intern_rec env (loc, e) = match e with
 | CTacAtm atm -> intern_atm env atm
 | CTacRef qid ->
   begin match get_variable env qid with
-  | ArgVar (_, id) ->
+  | ArgVar {CAst.v=id} ->
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
   | ArgArg (TacConstant kn) ->
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index ad52884ca6..2f6c97f08b 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -136,7 +136,7 @@ type constr_matching = constr_match_branch list located
 
 type goal_match_pattern_r = {
   q_goal_match_concl : constr_match_pattern;
-  q_goal_match_hyps : (Name.t located * constr_match_pattern) list;
+  q_goal_match_hyps : (Misctypes.lname * constr_match_pattern) list;
 }
 
 type goal_match_pattern = goal_match_pattern_r located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 33c4a97de1..d0c1365eff 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -425,7 +425,7 @@ let of_goal_matching (loc, gm) =
     let map (_, _, pat, knd) = of_tuple [knd; of_pattern pat] in
     let concl = of_tuple [concl_knd; of_pattern concl_pat] in
     let r = of_tuple [of_list ?loc map hyps_pats; concl] in
-    let hyps = List.map (fun ((_, na), _, _, _) -> na) hyps_pats in
+    let hyps = List.map (fun ({CAst.v=na}, _, _, _) -> na) hyps_pats in
     let map (_, na, _, _) = na in
     let hctx = List.map map hyps_pats in
     (** Order of elements is crucial here! *)
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index e7d5578b6e..65cdef0f3f 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -107,7 +107,7 @@ let mk_destruction_arg = function
 | ElimOnConstr c ->
   let c = c >>= fun c -> return (mk_with_bindings c) in
   Misctypes.ElimOnConstr (delayed_of_tactic c)
-| ElimOnIdent id -> Misctypes.ElimOnIdent (Loc.tag id)
+| ElimOnIdent id -> Misctypes.ElimOnIdent CAst.(make id)
 | ElimOnAnonHyp n -> Misctypes.ElimOnAnonHyp n
 
 let mk_induction_clause (arg, eqn, as_, occ) =
@@ -343,7 +343,7 @@ let on_destruction_arg tac ev arg =
       let flags = tactic_infer_flags ev in
       let (sigma', c) = Unification.finish_evar_resolution ~flags env sigma' (sigma, c) in
       Proofview.tclUNIT (Some sigma', Misctypes.ElimOnConstr (c, lbind))
-    | ElimOnIdent id -> Proofview.tclUNIT (None, Misctypes.ElimOnIdent (Loc.tag id))
+    | ElimOnIdent id -> Proofview.tclUNIT (None, Misctypes.ElimOnIdent CAst.(make id))
     | ElimOnAnonHyp n -> Proofview.tclUNIT (None, Misctypes.ElimOnAnonHyp n)
     in
     arg >>= fun (sigma', arg) ->
@@ -429,7 +429,7 @@ let inversion knd arg pat ids =
     | None -> assert false
     | Some (_, Misctypes.ElimOnAnonHyp n) ->
       Inv.inv_clause knd pat ids (AnonHyp n)
-    | Some (_, Misctypes.ElimOnIdent (_, id)) ->
+    | Some (_, Misctypes.ElimOnIdent {CAst.v=id}) ->
       Inv.inv_clause knd pat ids (NamedHyp id)
     | Some (_, Misctypes.ElimOnConstr c) ->
       let open Misctypes in