diff options
| author | Emilio Jesus Gallego Arias | 2018-02-14 06:24:02 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-14 06:24:02 +0100 |
| commit | 2e015ec8e2958c2848c33a152dd883e048069a7d (patch) | |
| tree | b58ab42df9c5bc08606e00a51834429b1718c783 /src/tac2intern.ml | |
| parent | 46dfd18cd1744adbe9fe8463423c5a4484ebeb70 (diff) | |
[coq] Adapt to coq/coq#6745
Nothing remarkable.
Diffstat (limited to 'src/tac2intern.ml')
| -rw-r--r-- | src/tac2intern.ml | 4 |
1 files changed, 2 insertions, 2 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) -> |