aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-09 14:00:26 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:03 +0100
commit407e154baa44609dea9f6f1ade746e24d60e2513 (patch)
treed29ce22e16bdd2a243f45d16f6a07ec81a299f18 /intf
parent66eae7fa7f8e1f075a8c84afad48af4d35c4bfaf (diff)
Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.
Diffstat (limited to 'intf')
-rw-r--r--intf/extend.ml4
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) *)