diff options
| author | Emilio Jesus Gallego Arias | 2018-03-05 23:38:52 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-10 00:33:08 +0100 |
| commit | 4718f5afec0538781195fdac82ffefb0b7c57535 (patch) | |
| tree | ed60d5b3913f4701ad108e6f9fd007eb3478db24 /src | |
| parent | 123de18a0886233b047ef2bad4bd7b3694f2abcc (diff) | |
[coq] Adapt to coq/coq#6837.
Minor.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 8 | ||||
| -rw-r--r-- | src/tac2core.ml | 6 | ||||
| -rw-r--r-- | src/tac2entries.ml | 2 | ||||
| -rw-r--r-- | src/tac2quote.ml | 3 |
4 files changed, 9 insertions, 10 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index f4818f4ece..6189bb18cc 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -372,8 +372,8 @@ GEXTEND Gram [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ] ; globref: - [ [ "&"; id = Prim.ident -> Libnames.Ident (Loc.tag ~loc:!@loc id) - | qid = Prim.qualid -> Libnames.Qualid (Loc.tag ~loc:!@loc qid.CAst.v) + [ [ "&"; id = Prim.ident -> CAst.make ~loc:!@loc (Libnames.Ident id) + | qid = Prim.qualid -> CAst.map (fun qid -> Libnames.Qualid qid) qid ] ] ; END @@ -667,8 +667,8 @@ GEXTEND Gram ] ] ; refglobal: - [ [ "&"; id = Prim.ident -> QExpr (Libnames.Ident (Loc.tag ~loc:!@loc id)) - | qid = Prim.qualid -> QExpr (Libnames.Qualid Loc.(tag ~loc:!@loc qid.CAst.v)) + [ [ "&"; id = Prim.ident -> QExpr (CAst.make ~loc:!@loc @@ Libnames.Ident id) + | qid = Prim.qualid -> QExpr (CAst.make ~loc:!@loc @@ Libnames.Qualid qid.CAst.v) | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id) ] ] ; diff --git a/src/tac2core.ml b/src/tac2core.ml index c6c3f26b6b..cf9af526d4 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -910,13 +910,13 @@ let () = let () = let intern self ist qid = match qid with - | Libnames.Ident (_, id) -> + | {CAst.v=Libnames.Ident id} -> GlbVal (Globnames.VarRef id), gtypref t_reference - | Libnames.Qualid (loc, qid) -> + | {CAst.loc;v=Libnames.Qualid qid} -> let gr = try Nametab.locate qid with Not_found -> - Nametab.error_global_not_found ?loc qid + Nametab.error_global_not_found (CAst.make ?loc qid) in GlbVal gr, gtypref t_reference in diff --git a/src/tac2entries.ml b/src/tac2entries.ml index e4bddf439b..430142832b 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -831,7 +831,7 @@ end (** Printing *) let print_ltac ref = - let (loc, qid) = qualid_of_reference ref in + let {loc;v=qid} = qualid_of_reference ref in if Tac2env.is_constructor qid then let kn = try Tac2env.locate_constructor qid diff --git a/src/tac2quote.ml b/src/tac2quote.ml index e986bfc393..2a0230b779 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -344,8 +344,7 @@ let make_red_flag l = let of_reference r = let of_ref ref = - let loc = Libnames.loc_of_reference ref in - inj_wit ?loc wit_reference ref + inj_wit ?loc:ref.loc wit_reference ref in of_anti of_ref r |