diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-10 09:26:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-22 00:44:33 +0100 |
| commit | 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f (patch) | |
| tree | 24e8de17078242c1ea39e31ecfe55a1c024d0eff /parsing/pcoq.mli | |
| parent | 0c5f0afffd37582787f79267d9841259095b7edc (diff) | |
[ast] Improve precision of Ast location recognition in serialization.
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index accb51366..f36250176 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -192,17 +192,17 @@ module Prim : open Libnames val preident : string Gram.entry val ident : Id.t Gram.entry - val name : Name.t located Gram.entry - val identref : Id.t located Gram.entry + val name : lname Gram.entry + val identref : lident Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry - val pattern_identref : Id.t located Gram.entry + val pattern_identref : lident Gram.entry val base_ident : Id.t Gram.entry val natural : int Gram.entry val bigint : Constrexpr.raw_natural_number Gram.entry val integer : int Gram.entry val string : string Gram.entry - val lstring : string located Gram.entry + val lstring : lstring Gram.entry val qualid : qualid located Gram.entry val fullyqualid : Id.t list located Gram.entry val reference : reference Gram.entry @@ -210,8 +210,8 @@ module Prim : val smart_global : reference or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry - val ne_lstring : string located Gram.entry - val var : Id.t located Gram.entry + val ne_lstring : lstring Gram.entry + val var : lident Gram.entry end module Constr : @@ -233,10 +233,10 @@ module Constr : val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) val binders : local_binder_expr list Gram.entry (* list of binder *) val open_binders : local_binder_expr list Gram.entry - val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry - val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry + val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry + val typeclass_constraint : (lname * bool * constr_expr) Gram.entry val record_declaration : constr_expr Gram.entry - val appl_arg : (constr_expr * explicitation located option) Gram.entry + val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry end module Module : |