diff options
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index fbea84e7bb..b62e23b5e3 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -20,8 +20,10 @@ open Genarg (**********************************************************************) (* 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 = |