3 files changed, 14 insertions, 2 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 6805a96ed..f57e32c88 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -101,7 +101,7 @@ type ('self, 'a) symbol =
 | Aself : ('self, 'self) symbol
 | Anext : ('self, 'self) symbol
 | Aentry : 'a entry -> ('self, 'a) symbol
-| Aentryl : 'a entry * int -> ('self, 'a) symbol
+| Aentryl : 'a entry * string -> ('self, 'a) symbol
 | Arules : 'a rules list -> ('self, 'a) symbol
 
 and ('self, _, 'r) rule =
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6fdd9ea9b..171276a70 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -17,9 +17,17 @@ let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y
 
 (** Location Utils  *)
+let ploc_file_of_coq_file = function
+| Loc.ToplevelInput -> ""
+| Loc.InFile f -> f
+
 let coq_file_of_ploc_file s =
   if s = "" then Loc.ToplevelInput else Loc.InFile s
 
+let of_coqloc loc =
+  let open Loc in
+  Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) ""
+
 let to_coqloc loc =
   { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
     Loc.line_nb = Ploc.line_nb loc;
@@ -236,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Aentry e ->
     Symbols.snterm (G.Entry.obj e)
   | Aentryl (e, n) ->
-    Symbols.snterml (G.Entry.obj e, string_of_int n)
+    Symbols.snterml (G.Entry.obj e, n)
   | Arules rs ->
     G.srules' (List.map symbol_of_rules rs)
 
@@ -328,6 +336,7 @@ module Gram =
       I'm not entirely sure it makes sense, but at least it would be more correct.
           *)
       G.delete_rule e pil
+    let safe_extend e ext = grammar_extend e None ext
   end
 
 (** Remove extensions
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