diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.ml | 8 | ||||
| -rw-r--r-- | intf/notation_term.ml | 9 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 1 |
3 files changed, 16 insertions, 2 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index 813ed6dc6c..78f0aa1178 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,6 +29,11 @@ type production_level = | NextLevel | NumLevel of int +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + (** User-level types used to tell how to parse or interpret of the non-terminal *) type 'a constr_entry_key_gen = @@ -37,7 +42,8 @@ type 'a constr_entry_key_gen = | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of 'a - | ETPattern of int option + | ETConstrAsBinder of constr_as_binder_kind * 'a + | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) | ETOther of string * string (** Entries level (left-hand side of grammar rules) *) 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 diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 8e0fe54c55..0b5009e26b 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -214,6 +214,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key |