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