diff options
Diffstat (limited to 'interp/notation_term.ml')
| -rw-r--r-- | interp/notation_term.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 82238b71b7..47b9deccce 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -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 |