diff options
| author | Maxime Dénès | 2018-02-21 19:02:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-21 19:02:56 +0100 |
| commit | 4b0fe4e09d547f0e6ee98da3fd6f7a134e51f3fd (patch) | |
| tree | 9550d5b99c9023c9c0ad84d2d7b89e05f344348b /interp/constrexpr_ops.mli | |
| parent | 2f13806f10b2781f84417014c8018097c8e8b2ad (diff) | |
| parent | 2aff5c40ba9b40b4e0188b799dde6f31585e356b (diff) | |
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
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 |