From 2e015ec8e2958c2848c33a152dd883e048069a7d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 14 Feb 2018 06:24:02 +0100
Subject: [coq] Adapt to coq/coq#6745

Nothing remarkable.
---
 src/tac2intern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/tac2intern.ml')

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) ->
-- 
cgit v1.2.3