diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 2 | ||||
| -rw-r--r-- | intf/glob_term.ml | 8 |
2 files changed, 9 insertions, 1 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index e0d2d7bf48..8bcdbcc0ef 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -104,7 +104,7 @@ and case_expr = constr_expr (* expression that is being matched * cases_pattern_expr option (* in-clause *) and branch_expr = - (cases_pattern_expr list Loc.located list * constr_expr) Loc.located + (cases_pattern_expr list list * constr_expr) Loc.located and binder_expr = Name.t Loc.located list * binder_kind * constr_expr diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 72c91db6a0..f311d33b8a 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -93,6 +93,14 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr +type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located +type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list +type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list + +type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g +type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g +type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g + type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option |