diff options
Diffstat (limited to 'parsing/notation_gram.ml')
| -rw-r--r-- | parsing/notation_gram.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index d8c08803b6..fc5feba58b 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -32,7 +32,7 @@ type grammar_constr_prod_item = type one_notation_grammar = { notgram_level : level; - notgram_assoc : Extend.gram_assoc option; + notgram_assoc : Gramlib.Gramext.g_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; } |