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 /interp/constrexpr_ops.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/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 0b00b0e4d..50c818d3c 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Libnames open Misctypes @@ -44,9 +43,9 @@ val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr -val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr -val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr +val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [abstract_constr_expr], with location *) @@ -72,10 +71,10 @@ val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr val coerce_reference_to_id : reference -> Id.t (** FIXME: nothing to do here *) -val coerce_to_id : constr_expr -> Id.t located +val coerce_to_id : constr_expr -> lident (** Destruct terms of the form [CRef (Ident _)]. *) -val coerce_to_name : constr_expr -> Name.t located +val coerce_to_name : constr_expr -> lname (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr @@ -84,10 +83,10 @@ val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr val default_binder_kind : binder_kind -val names_of_local_binders : local_binder_expr list -> Name.t located list +val names_of_local_binders : local_binder_expr list -> lname list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder_expr list -> Name.t located list +val names_of_local_assums : local_binder_expr list -> lname list (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) @@ -113,7 +112,7 @@ val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t val free_vars_of_constr_expr : constr_expr -> Id.Set.t val occur_var_constr_expr : Id.t -> constr_expr -> bool -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 -> lident option -> local_binder_expr list * local_binder_expr list val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list |