aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r--parsing/pcoq.mli3
1 files changed, 3 insertions, 0 deletions
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