diff options
Diffstat (limited to 'intf/notation_term.ml')
| -rw-r--r-- | intf/notation_term.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 0f4bfef600..86f5adbd78 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -61,7 +61,14 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) -type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern +type notation_binder_source = + (* This accepts only pattern *) + (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) + | NtnParsedAsPattern of bool + (* This accepts only ident *) + | NtnParsedAsIdent + (* This accepts ident, or pattern, or both *) + | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList |