diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index d24264abc..091f98424 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -42,5 +42,11 @@ val extend_tactic_grammar : val extend_vernac_command_grammar : string -> (string * grammar_tactic_production list) list -> unit +val get_extend_tactic_grammars : + unit -> (string * (string * grammar_tactic_production list) list) list +val get_extend_vernac_grammars : + unit -> (string * (string * grammar_tactic_production list) list) list +val reset_extend_grammars_v8 : unit -> unit + val subst_all_grammar_command : Names.substitution -> all_grammar_command -> all_grammar_command |