aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--gramlib/grammar.ml10
-rw-r--r--gramlib/grammar.mli2
-rw-r--r--parsing/g_constr.mlg6
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg10
-rw-r--r--plugins/ssr/ssrparser.mlg32
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mlg2
-rw-r--r--toplevel/coqloop.ml4
-rw-r--r--toplevel/g_toplevel.mlg2
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
-rw-r--r--vernac/g_vernac.mlg2
-rw-r--r--vernac/pvernac.ml2
14 files changed, 40 insertions, 40 deletions
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index f96cfebed5..f86cb0f6f2 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -23,7 +23,7 @@ module type S =
val create : string -> 'a e
val parse : 'a e -> parsable -> 'a
val name : 'a e -> string
- val of_parser : string -> (te Stream.t -> 'a) -> 'a e
+ val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a e
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
end
@@ -112,7 +112,7 @@ type 'a ty_entry = {
and 'a ty_desc =
| Dlevels of 'a ty_level list
-| Dparser of 'a parser_t
+| Dparser of (Plexing.location_function -> 'a parser_t)
and 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level
@@ -1449,7 +1449,7 @@ let start_parser_of_entry entry =
match entry.edesc with
Dlevels [] -> empty_entry entry.ename
| Dlevels elev -> start_parser_of_levels entry 0 elev
- | Dparser p -> fun levn strm -> p strm
+ | Dparser p -> fun levn strm -> p !floc strm
(* Extend syntax *)
@@ -1549,9 +1549,9 @@ let clear_entry e =
let parse_token_stream (e : 'a e) ts : 'a =
e.estart 0 ts
let name e = e.ename
- let of_parser n (p : te Stream.t -> 'a) : 'a e =
+ let of_parser n (p : Plexing.location_function -> te Stream.t -> 'a) : 'a e =
{ ename = n;
- estart = (fun _ -> p);
+ estart = (fun _ -> p !floc);
econtinue =
(fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
edesc = Dparser p}
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index ec4ec62409..658baf1de9 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -32,7 +32,7 @@ module type S =
val create : string -> 'a e
val parse : 'a e -> parsable -> 'a
val name : 'a e -> string
- val of_parser : string -> (te Stream.t -> 'a) -> 'a e
+ val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a e
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
end
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
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 2654729652..e6e6e29d4f 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -332,7 +332,7 @@ END
let local_test_lpar_id_colon =
let err () = raise Stream.Failure in
Pcoq.Entry.of_parser "lpar_id_colon"
- (fun strm ->
+ (fun _ strm ->
match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" ->
(match Util.stream_nth 1 strm with
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5c84b35f1b..cab8ed0a55 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -64,7 +64,7 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
Pcoq.Entry.of_parser "test_bracket_ident"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "[" ->
(match stream_nth 1 strm with
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 945a2dd613..7cd43cb5cd 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -40,7 +40,7 @@ let err () = raise Stream.Failure
(* admissible notation "(x t)" *)
let test_lpar_id_coloneq =
Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
@@ -54,7 +54,7 @@ let test_lpar_id_coloneq =
(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
@@ -68,7 +68,7 @@ let test_lpar_id_rpar =
(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
@@ -85,7 +85,7 @@ open Extraargs
(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
let check_for_coloneq =
Pcoq.Entry.of_parser "lpar_id_colon"
- (fun strm ->
+ (fun _ strm ->
let rec skip_to_rpar p n =
match List.last (Stream.npeek n strm) with
| KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
@@ -109,7 +109,7 @@ let check_for_coloneq =
let lookup_at_as_comma =
Pcoq.Entry.of_parser "lookup_at_as_comma"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| KEYWORD (","|"at"|"as") -> ()
| _ -> err ())
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index c09250ade5..3ad88bc8ba 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -235,7 +235,7 @@ let pr_ssrsimpl _ _ _ = pr_simpl
let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
-let test_ssrslashnum b1 b2 strm =
+let test_ssrslashnum b1 b2 _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "/" ->
(match Util.stream_nth 1 strm with
@@ -276,8 +276,8 @@ let test_ssrslashnum11 = test_ssrslashnum true true
let test_ssrslashnum01 = test_ssrslashnum false true
let test_ssrslashnum00 = test_ssrslashnum false false
-let negate_parser f x =
- let rc = try Some (f x) with Stream.Failure -> None in
+let negate_parser f tok x =
+ let rc = try Some (f tok x) with Stream.Failure -> None in
match rc with
| None -> ()
| Some _ -> raise Stream.Failure
@@ -475,7 +475,7 @@ END
(* Old kinds of terms *)
-let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> xInParens
| Tok.KEYWORD "@" -> xWithAt
| _ -> xNoFlag
@@ -484,7 +484,7 @@ let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
(* New kinds of terms *)
-let input_term_annotation strm =
+let input_term_annotation _ strm =
match Stream.npeek 2 strm with
| Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
| Tok.KEYWORD "(" :: _ -> `Parens
@@ -751,7 +751,7 @@ let pushIPatNoop = function
| pats :: orpat -> (IPatNoop :: pats) :: orpat
| [] -> []
-let test_ident_no_do strm =
+let test_ident_no_do _ strm =
match Util.stream_nth 0 strm with
| Tok.IDENT s when s <> "do" -> ()
| _ -> raise Stream.Failure
@@ -830,7 +830,7 @@ END
{
-let reject_ssrhid strm =
+let reject_ssrhid _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "[" ->
(match Util.stream_nth 1 strm with
@@ -840,13 +840,13 @@ let reject_ssrhid strm =
let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
-let rec reject_binder crossed_paren k s =
+let rec reject_binder crossed_paren k tok s =
match
try Some (Util.stream_nth k s)
with Stream.Failure -> None
with
- | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s
- | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s
+ | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) tok s
+ | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) tok s
| Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren ->
raise Stream.Failure
| Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
@@ -1013,7 +1013,7 @@ END
{
-let accept_ssrfwdid strm =
+let accept_ssrfwdid _ strm =
match stream_nth 0 strm with
| Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
| _ -> raise Stream.Failure
@@ -1597,7 +1597,7 @@ END
let sq_brace_tacnames =
["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
(* "by" is a keyword *)
-let accept_ssrseqvar strm =
+let accept_ssrseqvar _ strm =
match stream_nth 0 strm with
| Tok.IDENT id when not (List.mem id sq_brace_tacnames) ->
accept_before_syms_or_ids ["["] ["first";"last"] strm
@@ -1691,7 +1691,7 @@ let ssr_id_of_string loc s =
^ "Scripts with explicit references to anonymous variables are fragile."))
end; Id.of_string s
-let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
}
@@ -2002,7 +2002,7 @@ END
{
-let accept_ssreqid strm =
+let accept_ssreqid _ strm =
match Util.stream_nth 0 strm with
| Tok.IDENT _ -> accept_before_syms [":"] strm
| Tok.KEYWORD ":" -> ()
@@ -2423,7 +2423,7 @@ let lbrace = Char.chr 123
(** Workaround to a limitation of coqpp *)
let test_ssr_rw_syntax =
- let test strm =
+ let test _ strm =
if not !ssr_rw_syntax then raise Stream.Failure else
if is_ssr_loaded () then () else
match Util.stream_nth 0 strm with
@@ -2634,7 +2634,7 @@ END
{
-let accept_idcomma strm =
+let accept_idcomma _ strm =
match stream_nth 0 strm with
| Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
| _ -> raise Stream.Failure
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index d920ea9a46..42b800b596 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -66,7 +66,7 @@ END
{
-let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> '('
| Tok.KEYWORD "@" -> '@'
| _ -> ' '
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 2673995a86..f37feb24de 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -242,10 +242,10 @@ let set_prompt prompt =
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
- let rec dot st = match Stream.next st with
+ let rec dot tok st = match Stream.next st with
| Tok.KEYWORD ("."|"...") -> ()
| Tok.EOI -> ()
- | _ -> dot st
+ | _ -> dot tok st
in
Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 1a1537113e..e180d9e750 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -36,7 +36,7 @@ let err () = raise Stream.Failure
let test_show_goal =
Pcoq.Entry.of_parser "test_show_goal"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| IDENT "Show" ->
(match stream_nth 1 strm with
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 23b5f4daef..e0e660b984 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -26,7 +26,7 @@ let err () = raise Stream.Failure
type lookahead = int -> Tok.t Stream.t -> int option
let entry_of_lookahead s (lk : lookahead) =
- let run strm = match lk 0 strm with None -> err () | Some _ -> () in
+ let run _ strm = match lk 0 strm with None -> err () | Some _ -> () in
Pcoq.Entry.of_parser s run
let (>>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index ad5d98669d..dcd1979a85 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -519,7 +519,7 @@ END
let only_starredidentrefs =
Pcoq.Entry.of_parser "test_only_starredidentrefs"
- (fun strm ->
+ (fun _ strm ->
let rec aux n =
match Util.stream_nth n strm with
| KEYWORD "." -> ()
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index da28e260b3..826e88cabf 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -67,7 +67,7 @@ module Vernac_ =
let command_entry =
Pcoq.Entry.of_parser "command_entry"
- (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
+ (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:05:53 +0000