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 f959bd80c..48604e188 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -80,6 +80,8 @@ module type S =
(* Get comment parsing information from the Lexer *)
val comment_state : coq_parsable -> ((int * int) * string) list
+ val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit
+
(* Apparently not used *)
val srules' : production_rule list -> symbol
val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
@@ -299,6 +301,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
(** Location Utils *)
+val of_coqloc : Loc.t -> Ploc.t
val to_coqloc : Ploc.t -> Loc.t
val (!@) : Ploc.t -> Loc.t