diff options
Diffstat (limited to 'intf/extend.ml')
| -rw-r--r-- | intf/extend.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index 5552bed55..e4d014a09 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,6 +29,8 @@ type production_level = | NextLevel | NumLevel of int +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + type ('lev,'pos) constr_entry_key_gen = | ETName | ETReference | ETBigint | ETBinder of bool @@ -36,7 +38,7 @@ type ('lev,'pos) constr_entry_key_gen = | ETPattern | ETOther of string * string | ETConstrList of ('lev * 'pos) * Tok.t list - | ETBinderList of bool * Tok.t list + | ETBinderList of binder_entry_kind (** Entries level (left-hand-side of grammar rules) *) |