diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_prim.ml4 | 12 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 8 |
3 files changed, 12 insertions, 12 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 94149a085..1fa26b455 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -202,11 +202,11 @@ GEXTEND Gram | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) | "@"; lid = pattern_identref; args=LIST1 identref -> let { CAst.loc = locid; v = id } = lid in - let args = List.map (fun x -> CAst.make @@ CRef (CAst.make ?loc:x.CAst.loc @@ Ident x.CAst.v, None), None) args in + let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - CAst.make ~loc:!@loc @@ CAppExpl ((None, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ] + CAst.make ~loc:!@loc @@ CAppExpl ((None, (qualid_of_ident ~loc:!@loc ldots_var), None),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 08bcd0f8c..91dce27fe 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -18,7 +18,7 @@ let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] let _ = List.iter CLexer.add_keyword prim_kw -let local_make_qualid l id = make_qualid (DirPath.make l) id +let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id let my_int_of_string loc s = try @@ -67,8 +67,8 @@ GEXTEND Gram ] ] ; basequalid: - [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' - | id = ident -> qualid_of_ident id + [ [ id = ident; (l,id')=fields -> local_make_qualid !@loc (l@[id]) id' + | id = ident -> qualid_of_ident ~loc:!@loc id ] ] ; name: @@ -77,8 +77,8 @@ GEXTEND Gram ; reference: [ [ id = ident; (l,id') = fields -> - CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id') - | id = ident -> CAst.make ~loc:!@loc @@ Ident id + local_make_qualid !@loc (l@[id]) id' + | id = ident -> local_make_qualid !@loc [] id ] ] ; by_notation: @@ -89,7 +89,7 @@ GEXTEND Gram | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ] ; qualid: - [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] + [ [ qid = basequalid -> qid ] ] ; ne_string: [ [ s = STRING -> diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9a45bc973..f959bd80c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,11 +213,11 @@ module Prim : val integer : int Gram.entry val string : string Gram.entry val lstring : lstring Gram.entry - val qualid : qualid CAst.t Gram.entry + val reference : qualid Gram.entry + val qualid : qualid Gram.entry val fullyqualid : Id.t list CAst.t Gram.entry - val reference : reference Gram.entry val by_notation : (string * string option) Gram.entry - val smart_global : reference or_by_notation Gram.entry + val smart_global : qualid or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry val ne_lstring : lstring Gram.entry @@ -232,7 +232,7 @@ module Constr : val binder_constr : constr_expr Gram.entry val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry - val global : reference Gram.entry + val global : qualid Gram.entry val universe_level : Glob_term.glob_level Gram.entry val sort : Glob_term.glob_sort Gram.entry val sort_family : Sorts.family Gram.entry |