aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-06-06 16:52:23 +0200
committerVincent Laporte2019-07-29 14:18:01 +0000
commit55400b02a70c540d6c6e8152affe1eae99760b91 (patch)
tree72055f03180e1bbaad97e29c6287c51828c289bc /parsing
parent807b1e18575914f9956569ab71bb5fe29716cbdf (diff)
Tentatively providing a localization function to ad-hoc camlp5 parsers.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.mlg6
-rw-r--r--parsing/pcoq.mli2
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 8fdec7d1a8..78a12a2e7d 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -84,7 +84,7 @@ let err () = raise Stream.Failure
(* admissible notation "(x t)" *)
let lpar_id_coloneq =
Pcoq.Entry.of_parser "test_lpar_id_coloneq"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
@@ -99,7 +99,7 @@ let lpar_id_coloneq =
let impl_ident_head =
Pcoq.Entry.of_parser "impl_ident_head"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "{" ->
(match stream_nth 1 strm with
@@ -112,7 +112,7 @@ let impl_ident_head =
let name_colon =
Pcoq.Entry.of_parser "name_colon"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| IDENT s ->
(match stream_nth 1 strm with
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cde867d2ef..7efeab6ba0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -29,7 +29,7 @@ module Entry : sig
val create : string -> 'a t
val parse : 'a t -> Parsable.t -> 'a
val print : Format.formatter -> 'a t -> unit
- val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t
+ val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t
val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a
val name : 'a t -> string
end