diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.mli | 11 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
2 files changed, 11 insertions, 2 deletions
diff --git a/intf/extend.mli b/intf/extend.mli index ca40eb7443..d66f29ba72 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -10,8 +10,17 @@ type side = Left | Right +type gram_assoc = NonA | RightA | LeftA + +type gram_position = + | First + | Last + | Before of string + | After of string + | Level of string + type production_position = - | BorderProd of side * Compat.gram_assoc option + | BorderProd of side * gram_assoc option | InternalProd type production_level = diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index dfa03a4d75..31c1643d24 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -185,7 +185,7 @@ type grammar_tactic_prod_item_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level | SetLevel of int - | SetAssoc of Compat.gram_assoc + | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing of Flags.compat_version | SetFormat of string located |