diff options
| author | coqbot-app[bot] | 2020-11-20 22:01:06 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 22:01:06 +0000 |
| commit | 23d30fa1c19af9a29787204d81d7bd2d2e0c9b1f (patch) | |
| tree | 98e1452ac1c2b2e88178461fbe51393d1d918f3e /interp/notation_term.ml | |
| parent | 87a59a875b0945fa7976fd16b17a2ff5dd015402 (diff) | |
| parent | 345bcc504a1ed4f11d328cc1dfa17ba37f6875b3 (diff) | |
Merge PR #13265: Add support for general non-necessarily-recursive binders in notations
Reviewed-by: ejgallego
Ack-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'interp/notation_term.ml')
| -rw-r--r-- | interp/notation_term.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 82238b71b7..29db23cc54 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -27,8 +27,8 @@ type notation_constr = | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (* Part only in [glob_constr] *) - | NLambda of Name.t * notation_constr * notation_constr - | NProd of Name.t * notation_constr * notation_constr + | NLambda of Name.t * notation_constr option * notation_constr + | NProd of Name.t * notation_constr option * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of Constr.case_style * notation_constr option * @@ -78,6 +78,8 @@ type notation_binder_source = | NtnParsedAsIdent (* This accepts ident, or pattern, or both *) | NtnBinderParsedAsConstr of constr_as_binder_kind + (* This accepts ident, _, and quoted pattern *) + | NtnParsedAsBinder type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList |