diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e7d2cde122..9f9e348463 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -38,3 +38,6 @@ val extend_tactic_grammar : val extend_vernac_command_grammar : string -> (string * grammar_tactic_production list) list -> unit + +val subst_all_grammar_command : + Names.substitution -> all_grammar_command -> all_grammar_command |