diff options
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 6e5c0f8515..50c818d3c3 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 *) @@ -54,6 +53,11 @@ val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_e val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) +val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr + +val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr +(** Apply a list of pattern arguments to a pattern *) + (** @deprecated variant of mkCLambdaN *) val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr [@@ocaml.deprecated "deprecated variant of mkCLambdaN"] @@ -67,20 +71,22 @@ 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 + (** {6 Binder manipulation} *) 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. *) @@ -106,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 |