diff options
| author | Emilio Jesus Gallego Arias | 2017-12-10 09:26:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-22 00:44:33 +0100 |
| commit | 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f (patch) | |
| tree | 24e8de17078242c1ea39e31ecfe55a1c024d0eff /interp/topconstr.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 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 9fc02461e0..66d87707c8 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Constrexpr @@ -15,7 +14,7 @@ val asymmetric_patterns : bool ref [@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"] (** Utilities on constr_expr *) -val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list +val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list [@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"] val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list |