aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrexpr_ops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.mli')
-rw-r--r--interp/constrexpr_ops.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 9a59d66f4..0b00b0e4d 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -54,6 +54,8 @@ 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 *)