diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 4 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 3 |
2 files changed, 5 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8e6a01aa3..b766f0c6b 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -611,8 +611,8 @@ let unfreeze (grams, lex) = the lexer state should not be resetted, since it contains keywords declared in g_*.ml4 *) -let _ = - Summary.declare_summary "GRAMMAR_LEXER" +let parser_summary_tag = + Summary.declare_summary_tag "GRAMMAR_LEXER" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = Summary.nop } diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d17ccb0b4..3ca013a96 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -313,3 +313,6 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t + +type frozen_t +val parser_summary_tag : frozen_t Summary.Dyn.tag |