[parser] initialization based on Loc.t rather than Loc.source

In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.

1 files changed, 2 insertions, 2 deletions

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3203a25b46..0418249e42 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -19,7 +19,7 @@ open Libnames
 module Parsable :
 sig
   type t
-  val make : ?file:Loc.source -> char Stream.t -> t
+  val make : ?loc:Loc.t -> char Stream.t -> t
   (* Get comment parsing information from the Lexer *)
   val comment_state : t -> ((int * int) * string) list
 end
@@ -121,7 +121,7 @@ end
 
 (** Parse a string *)
 
-val parse_string : 'a Entry.t -> string -> 'a
+val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
 val eoi_entry : 'a Entry.t -> 'a Entry.t
 val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t