diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 1d85c74e..0ac46ded 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -71,3 +71,5 @@ val get_extend_vernac_grammars : val recover_notation_grammar : notation -> (precedence * tolerability list) -> notation_var_internalization_type list * notation_grammar + +val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b |