diff options
Diffstat (limited to 'parsing/egramml.mli')
| -rw-r--r-- | parsing/egramml.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 1a3ae173c..030d39605 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -15,7 +15,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string - | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * + | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option * ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : |