diff options
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 122005e011..1e6c40c829 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -167,7 +167,7 @@ type syntax_modifier = | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option | SetLevel of int | SetCustomEntry of string * int option - | SetAssoc of Extend.gram_assoc + | SetAssoc of Gramlib.Gramext.g_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing | SetOnlyPrinting |