diff options
Diffstat (limited to 'parsing/extend.mli')
| -rw-r--r-- | parsing/extend.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/extend.mli b/parsing/extend.mli index b092e766b..1fc8800ef 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -13,8 +13,10 @@ open Util (**********************************************************************) (* constr entry keys *) +type side = Left | Right + type production_position = - | BorderProd of bool * Gramext.g_assoc option (* true=left; false=right *) + | BorderProd of side * Gramext.g_assoc option (* true=left; false=right *) | InternalProd type production_level = |