diff options
| -rw-r--r-- | parsing/egrammar.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index f54b31484d..e8292bf051 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -14,6 +14,7 @@ open Topconstr open Ast open Coqast open Vernacexpr +open Ppextend open Extend open Rawterm open Mod_subst @@ -23,7 +24,7 @@ type notation_grammar = int * Gramext.g_assoc option * notation * prod_item list * int list option type all_grammar_command = - | Notation of Symbols.level * notation_grammar + | Notation of (precedence * tolerability list) * notation_grammar | Grammar of grammar_command | TacticGrammar of (string * (string * grammar_production list) * @@ -55,4 +56,5 @@ val subst_all_grammar_command : val interp_entry_name : string -> string -> entry_type * Token.t Gramext.g_symbol -val recover_notation_grammar : notation -> Symbols.level -> notation_grammar +val recover_notation_grammar : + notation -> (precedence * tolerability list) -> notation_grammar |