Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`

14 files changed, 72 insertions, 184 deletions

diff --git a/META.coq.in b/META.coq.in
index 25c0b666f4..b3a96a8303 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -146,7 +146,7 @@ package "gramlib" (
   description = "Coq Grammar Engine"
   version     = "8.10"
 
-  requires    = ""
+  requires    = "coq.lib"
   directory   = "gramlib__pack"
 
   archive(byte)    = "gramlib.cma"
diff --git a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh
new file mode 100644
index 0000000000..e9daa7a44e
--- /dev/null
+++ b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9065" ] || [ "$CI_BRANCH" = "gramlib+no_ploc" ]; then
+
+    elpi_CI_REF=gramlib+no_ploc
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
diff --git a/gramlib/dune b/gramlib/dune
index 6a9e622b4c..8ca6aff25a 100644
--- a/gramlib/dune
+++ b/gramlib/dune
@@ -1,3 +1,4 @@
 (library
  (name gramlib)
- (public_name coq.gramlib))
+ (public_name coq.gramlib)
+ (libraries coq.lib))
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 285c14ec62..8f7953b714 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -130,7 +130,7 @@ let loc_of_token_interval bp ep =
   if bp == ep then
     if bp == 0 then Ploc.dummy else Ploc.after (!floc (bp - 1)) 0 1
   else
-    let loc1 = !floc bp in let loc2 = !floc (pred ep) in Ploc.encl loc1 loc2
+    let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2
 
 let name_of_symbol entry =
   function
@@ -816,7 +816,7 @@ let parse_parsable entry p =
       let cnt = Stream.count ts in
       let loc = fun_loc cnt in
       if !token_count - 1 <= cnt then loc
-      else Ploc.encl loc (fun_loc (!token_count - 1))
+      else Loc.merge loc (fun_loc (!token_count - 1))
     with Failure _ -> Ploc.make_unlined (Stream.count cs, Stream.count cs + 1)
   in
   floc := fun_loc;
@@ -884,7 +884,7 @@ module type S =
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
         ('self, 'b -> 'a, 'r) ty_rule
-    val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
+    val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
     module Unsafe :
       sig
         val clear_entry : 'a Entry.e -> unit
@@ -946,7 +946,7 @@ module GMake (L : GLexerType) =
     let r_stop = []
     let r_next r s = r @ [s]
     let production
-        (p : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f) : 'a ty_production =
+        (p : ('a, 'f, Loc.t -> 'a) ty_rule * 'f) : 'a ty_production =
       Obj.magic p
     module Unsafe =
       struct
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 0c585a7c0d..4b61286859 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -58,7 +58,7 @@ module type S =
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
         ('self, 'b -> 'a, 'r) ty_rule
-    val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
+    val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
 
     module Unsafe :
       sig
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index 986363ec1f..7b8618fd20 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -6,8 +6,7 @@ type pattern = string * string
 
 exception Error of string
 
-type location = Ploc.t
-type location_function = int -> location
+type location_function = int -> Loc.t
 type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
 
 type 'te lexer =
@@ -16,4 +15,4 @@ type 'te lexer =
     tok_removing : pattern -> unit;
     mutable tok_match : pattern -> 'te -> string;
     tok_text : pattern -> string;
-    mutable tok_comm : location list option }
+    mutable tok_comm : Loc.t list option }
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 96b432a8ad..63c89dac28 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -30,8 +30,8 @@ type 'te lexer =
     tok_removing : pattern -> unit;
     mutable tok_match : pattern -> 'te -> string;
     tok_text : pattern -> string;
-    mutable tok_comm : Ploc.t list option }
+    mutable tok_comm : Loc.t list option }
 and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
-and location_function = int -> Ploc.t
+and location_function = int -> Loc.t
   (** The type of a function giving the location of a token in the
       source from the token number in the stream (starting from zero). *)
diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml
index 082686db01..9342fc6c1d 100644
--- a/gramlib/ploc.ml
+++ b/gramlib/ploc.ml
@@ -2,60 +2,23 @@
 (* ploc.ml,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-type t =
-  { fname : string;
-    line_nb : int;
-    bol_pos : int;
-    line_nb_last : int;
-    bol_pos_last : int;
-    bp : int;
-    ep : int;
-    comm : string;
-    ecomm : string }
-
-let make_loc fname line_nb bol_pos (bp, ep) comm =
-  {fname = fname; line_nb = line_nb; bol_pos = bol_pos;
-   line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep;
-   comm = comm; ecomm = ""}
+open Loc
 
 let make_unlined (bp, ep) =
-  {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
    bp = bp; ep = ep; comm = ""; ecomm = ""}
 
 let dummy =
-  {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
    bp = 0; ep = 0; comm = ""; ecomm = ""}
 
-let file_name loc = loc.fname
-let first_pos loc = loc.bp
-let last_pos loc = loc.ep
-let line_nb loc = loc.line_nb
-let bol_pos loc = loc.bol_pos
-let line_nb_last loc = loc.line_nb_last
-let bol_pos_last loc = loc.bol_pos_last
-let comment loc = loc.comm
-let comment_last loc = loc.ecomm
-
 (* *)
 
-let encl loc1 loc2 =
-  if loc1.bp < loc2.bp then
-    if loc1.ep < loc2.ep then
-      {fname = loc1.fname; line_nb = loc1.line_nb; bol_pos = loc1.bol_pos;
-       line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last;
-       bp = loc1.bp; ep = loc2.ep; comm = loc1.comm; ecomm = loc2.comm}
-    else loc1
-  else if loc2.ep < loc1.ep then
-    {fname = loc2.fname; line_nb = loc2.line_nb; bol_pos = loc2.bol_pos;
-     line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last;
-     bp = loc2.bp; ep = loc1.ep; comm = loc2.comm; ecomm = loc1.comm}
-  else loc2
-let shift sh loc = {loc with bp = sh + loc.bp; ep = sh + loc.ep}
 let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len}
 let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len}
 let with_comment loc comm = {loc with comm = comm}
 
-exception Exc of t * exn
+exception Exc of Loc.t * exn
 
 let raise loc exc =
   match exc with
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index 2ce6382183..766e96fdfc 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -2,85 +2,36 @@
 (* ploc.mli,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-(** Locations and some pervasive type and value. *)
-
-type t
-
 (* located exceptions *)
 
-exception Exc of t * exn
+exception Exc of Loc.t * exn
    (** [Ploc.Exc loc e] is an encapsulation of the exception [e] with
        the input location [loc]. To be used to specify a location
        for an error. This exception must not be raised by [raise] but
        rather by [Ploc.raise] (see below), to prevent the risk of several
        encapsulations of [Ploc.Exc]. *)
-val raise : t -> exn -> 'a
+val raise : Loc.t -> exn -> 'a
    (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc],
        re-raise it (ignoring the new location [loc]), else raise the
        exception [Ploc.Exc loc e]. *)
 
-(* making locations *)
-
-val make_loc : string -> int -> int -> int * int -> string -> t
-   (** [Ploc.make_loc fname line_nb bol_pos (bp, ep) comm] creates a location
-       starting at line number [line_nb], where the position of the beginning
-       of the line is [bol_pos] and between the positions [bp] (included) and
-       [ep] excluded. And [comm] is the comment before the location. The
-       positions are in number of characters since the begin of the stream. *)
-val make_unlined : int * int -> t
+val make_unlined : int * int -> Loc.t
    (** [Ploc.make_unlined] is like [Ploc.make] except that the line number
        is not provided (to be used e.g. when the line number is unknown. *)
 
-val dummy : t
+val dummy : Loc.t
    (** [Ploc.dummy] is a dummy location, used in situations when location
        has no meaning. *)
 
-(* getting location info *)
-
-val file_name : t -> string
-   (** [Ploc.file_name loc] returns the file name of the location. *)
-val first_pos : t -> int
-   (** [Ploc.first_pos loc] returns the position of the begin of the location
-       in number of characters since the beginning of the stream. *)
-val last_pos : t -> int
-   (** [Ploc.last_pos loc] returns the position of the first character not
-       in the location in number of characters since the beginning of the
-       stream. *)
-val line_nb : t -> int
-   (** [Ploc.line_nb loc] returns the line number of the location or [-1] if
-       the location does not contain a line number (i.e. built with
-       [Ploc.make_unlined]. *)
-val bol_pos : t -> int
-   (** [Ploc.bol_pos loc] returns the position of the beginning of the line
-       of the location in number of characters since the beginning of
-       the stream, or [0] if the location does not contain a line number
-       (i.e. built with [Ploc.make_unlined]. *)
-val line_nb_last : t -> int
-val bol_pos_last : t -> int
-   (** Return the line number and the position of the beginning of the line
-       of the last position. *)
-val comment : t -> string
-   (** [Ploc.comment loc] returns the comment before the location. *)
-val comment_last : t -> string
-   (** [Ploc.comment loc] returns the last comment of the location. *)
-
 (* combining locations *)
 
-val encl : t -> t -> t
-   (** [Ploc.encl loc1 loc2] returns the location starting at the
-       smallest start of [loc1] and [loc2] and ending at the greatest end
-       of them. In other words, it is the location enclosing [loc1] and
-       [loc2]. *)
-val shift : int -> t -> t
-   (** [Ploc.shift sh loc] returns the location [loc] shifted with [sh]
-       characters. The line number is not recomputed. *)
-val sub : t -> int -> int -> t
+val sub : Loc.t -> int -> int -> Loc.t
    (** [Ploc.sub loc sh len] is the location [loc] shifted with [sh]
        characters and with length [len]. The previous ending position
        of the location is lost. *)
-val after : t -> int -> int -> t
+val after : Loc.t -> int -> int -> Loc.t
    (** [Ploc.after loc sh len] is the location just after loc (starting at
        the end position of [loc]) shifted with [sh] characters and of length
        [len]. *)
-val with_comment : t -> string -> t
+val with_comment : Loc.t -> string -> Loc.t
    (** Change the comment part of the given location *)
diff --git a/lib/loc.ml b/lib/loc.ml
index 1a09091bff..c08648911b 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -22,15 +22,19 @@ type t = {
   bol_pos_last : int; (** position of the beginning of end line *)
   bp : int; (** start position *)
   ep : int; (** end position *)
+  comm : string; (** start comment *)
+  ecomm : string (** end comment *)
 }
 
 let create fname line_nb bol_pos bp ep = {
   fname = fname; line_nb = line_nb; bol_pos = bol_pos;
-  line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
+  line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep;
+  comm = ""; ecomm = "" }
 
 let make_loc (bp, ep) = {
   fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
-  bp = bp; ep = ep; }
+  bp = bp; ep = ep;
+  comm = ""; ecomm = "" }
 
 let mergeable loc1 loc2 =
   loc1.fname = loc2.fname
@@ -45,7 +49,8 @@ let merge loc1 loc2 =
       bol_pos = loc1.bol_pos;
       line_nb_last = loc2.line_nb_last;
       bol_pos_last = loc2.bol_pos_last;
-      bp = loc1.bp; ep = loc2.ep; }
+      bp = loc1.bp; ep = loc2.ep;
+      comm = loc1.comm; ecomm = loc2.comm }
     else loc1
   else if loc2.ep < loc1.ep then {
     fname = loc2.fname;
@@ -53,7 +58,9 @@ let merge loc1 loc2 =
     bol_pos = loc2.bol_pos;
     line_nb_last = loc1.line_nb_last;
     bol_pos_last = loc1.bol_pos_last;
-    bp = loc2.bp; ep = loc1.ep; }
+    bp = loc2.bp; ep = loc1.ep;
+    comm = loc2.comm; ecomm = loc1.comm
+  }
   else loc2
 
 let merge_opt l1 l2 = match l1, l2 with
diff --git a/lib/loc.mli b/lib/loc.mli
index 23df1ebd9a..c46311b639 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -22,6 +22,8 @@ type t = {
   bol_pos_last : int; (** position of the beginning of end line *)
   bp : int; (** start position *)
   ep : int; (** end position *)
+  comm : string; (** start comment *)
+  ecomm : string (** end comment *)
 }
 
 (** {5 Location manipulation} *)
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index d81ee475b5..c327f8aa43 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -13,28 +13,6 @@ open Util
 open Tok
 open Gramlib
 
-(** Location utilities  *)
-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 from_coqloc fname line_nb bol_pos bp ep =
-  Ploc.make_loc (ploc_file_of_coq_file fname) line_nb bol_pos (bp, ep) ""
-
-let to_coqloc loc =
-  { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
-    Loc.line_nb = Ploc.line_nb loc;
-    Loc.bol_pos = Ploc.bol_pos loc;
-    Loc.bp = Ploc.first_pos loc;
-    Loc.ep = Ploc.last_pos loc;
-    Loc.line_nb_last = Ploc.line_nb_last loc;
-    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
-
-let (!@) = to_coqloc
-
 (* Dictionaries: trees annotated with string options, each node being a map
    from chars to dictionaries (the subtrees). A trie, in other words. *)
 
@@ -128,18 +106,22 @@ module Error = struct
 end
 open Error
 
-let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str)
+let err loc str = Loc.raise ~loc (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
 (* Update a loc without allocating an intermediate pair *)
 let set_loc_pos loc bp ep =
-  Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp)
+  Ploc.sub loc (bp - loc.Loc.bp) (ep - bp)
 
 (* Increase line number by 1 and update position of beginning of line *)
 let bump_loc_line loc bol_pos =
-  Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos
-		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+  Loc.{ loc with
+        line_nb      = loc.line_nb + 1;
+        line_nb_last = loc.line_nb + 1;
+        bol_pos;
+        bol_pos_last = bol_pos;
+      }
 
 (* Same as [bump_loc_line], but for the last line in location *)
 (* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop,
@@ -147,19 +129,25 @@ let bump_loc_line loc bol_pos =
 (* Warning: [bump_loc_line_last] changes the end position. You may need to call
    [set_loc_pos] to fix it. *)
 let bump_loc_line_last loc bol_pos =
-  let loc' =
-    Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos
-		  (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc)
-  in
-  Ploc.encl loc loc'
+  let open Loc in
+  let loc' = { loc with
+               line_nb      = loc.line_nb_last + 1;
+               line_nb_last = loc.line_nb_last + 1;
+               bol_pos;
+               bol_pos_last = bol_pos;
+               bp = loc.bp + 1;
+               ep = loc.ep + 1;
+             } in
+  Loc.merge loc loc'
 
 (* For some reason, the [Ploc.after] function of Camlp5 does not update line
    numbers, so we define our own function that does it. *)
 let after loc =
-  let line_nb = Ploc.line_nb_last loc in
-  let bol_pos = Ploc.bol_pos_last loc in
-  Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos
-		(Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+  Loc.{ loc with
+        line_nb = loc.line_nb_last;
+        bol_pos = loc.bol_pos_last;
+        bp      = loc.ep;
+      }
 
 (** Lexer conventions on tokens *)
 
@@ -324,7 +312,7 @@ let rec ident_tail loc len s = match Stream.peek s with
       | Utf8Token (st, n) when Unicode.is_unknown st ->
           let id = get_buff len in
           let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in
-          warn_unrecognized_unicode ~loc:!@loc (u,id); len
+          warn_unrecognized_unicode ~loc (u,id); len
       | _ -> len
 
 let rec number len s = match Stream.peek s with
@@ -368,7 +356,7 @@ let rec string loc ~comm_level bp len s = match Stream.peek s with
             Stream.junk s;
             let () = match comm_level with
             | Some 0 ->
-              warn_comment_terminator_in_string ~loc:!@loc ()
+              warn_comment_terminator_in_string ~loc ()
             | _ -> ()
             in
             let comm_level = Option.map pred comm_level in
@@ -757,7 +745,7 @@ let token_text = function
 
 let func cs =
   let loct = loct_create () in
-  let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in
+  let cur_loc = ref (Loc.create !current_file 1 0 0 0) in
   let ts =
     Stream.from
       (fun i ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 816a02a6aa..923147ba2e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -14,29 +14,6 @@ open Extend
 open Genarg
 open Gramlib
 
-(** 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;
-    Loc.bol_pos = Ploc.bol_pos loc;
-    Loc.bp = Ploc.first_pos loc;
-    Loc.ep = Ploc.last_pos loc;
-    Loc.line_nb_last = Ploc.line_nb_last loc;
-    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
-
-let (!@) = to_coqloc
-
 (** The parser of Coq *)
 module G : sig
 
@@ -112,7 +89,7 @@ end with type 'a Entry.e = 'a Extend.entry = struct
     with Ploc.Exc (loc,e) ->
       CLexer.drop_lexer_state ();
       let loc' = Loc.get_loc (Exninfo.info e) in
-      let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
+      let loc = match loc' with None -> loc | Some loc -> loc in
       Loc.raise ~loc e
 
   let comment_state (p,state) =
@@ -197,8 +174,8 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol
   let warning msg = Feedback.msg_warning Pp.(str msg) in
   G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)
 
-and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function
-| Stop -> Casted (G.r_stop, fun act loc -> act (!@loc))
+and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Loc.t -> r) casted_rule = function
+| Stop -> Casted (G.r_stop, fun act loc -> act loc)
 | Next (r, s) ->
   let Casted (r, cast) = symbol_of_rule r in
   Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x)))
@@ -209,7 +186,7 @@ and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function
   G.production (symb, cast act)
 
 (** FIXME: This is a hack around a deficient camlp5 API *)
-type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production
+type 'a any_production = AnyProduction : ('a, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production
 
 let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function
 | Rule (toks, act) ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 69ba57d516..352857d4cd 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -13,7 +13,6 @@ open Extend
 open Genarg
 open Constrexpr
 open Libnames
-open Gramlib
 
 (** The parser of Coq *)
 
@@ -261,11 +260,6 @@ val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t
 
 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
-
 type frozen_t
 val parser_summary_tag : frozen_t Summary.Dyn.tag