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 /intf/constrexpr.ml | |
| parent | 2f13806f10b2781f84417014c8018097c8e8b2ad (diff) | |
| parent | 2aff5c40ba9b40b4e0188b799dde6f31585e356b (diff) | |
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Diffstat (limited to 'intf/constrexpr.ml')
| -rw-r--r-- | intf/constrexpr.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index fbf9e248ab..c598287943 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -46,7 +46,7 @@ type prim_token = type instance_expr = Misctypes.glob_level list type cases_pattern_expr_r = - | CPatAlias of cases_pattern_expr * Id.t + | CPatAlias of cases_pattern_expr * Name.t Loc.located | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) @@ -70,8 +70,8 @@ and constr_expr_r = | CRef of reference * instance_expr option | CFix of Id.t Loc.located * fix_expr list | CCoFix of Id.t Loc.located * cofix_expr list - | CProdN of binder_expr list * constr_expr - | CLambdaN of binder_expr list * constr_expr + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * @@ -107,9 +107,6 @@ and case_expr = constr_expr (* expression that is being matched and branch_expr = (cases_pattern_expr list list * constr_expr) Loc.located -and binder_expr = - Name.t Loc.located list * binder_kind * constr_expr - and fix_expr = Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr @@ -131,7 +128,8 @@ and local_binder_expr = and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) - local_binder_expr list list (** for binders subexpressions *) + cases_pattern_expr list * (** for binders *) + local_binder_expr list list (** for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr |