diff options
| author | Hugo Herbelin | 2017-08-17 20:12:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:06 +0100 |
| commit | e4d93d1cef27d3a8c1e36139fc1e118730406f67 (patch) | |
| tree | 0149d4c6ff1fc4cc978e796f303ee6dcdda65074 /interp/constrexpr_ops.mli | |
| parent | 50970e4043d73d9a4fbd17ffe765745f6d726317 (diff) | |
Adding general support for irrefutable disjunctive patterns.
This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 9a59d66f42..0b00b0e4dc 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 *) |