diff options
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 6e5c0f8515..0b00b0e4dc 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -54,6 +54,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"] @@ -73,6 +78,8 @@ val coerce_to_id : constr_expr -> Id.t located val coerce_to_name : constr_expr -> Name.t located (** 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 |