Build:
- 0
2026-06-16 11:44.06: New job: build coq.8.14.0 (c1d09703a697)
2026-06-16 11:44.06: Waiting for resource in pool day11-builds
2026-06-16 12:05.18: Got resource from pool day11-builds
2026-06-16 12:05.18: [profile full] build coq.8.14.0
2026-06-16 12:05.18: build coq.8.14.0 (c1d09703a697)
=== DEPENDENCIES (11 transitive) ===
base-threads.base b7164ff76afe
base-unix.base 839dc585f12d
conf-findutils.1 a943cdd45084
conf-gmp.5 61e3c79e0ddf
conf-pkg-config.5 64c6b37d622b
dune.3.23.1 5402470d931c
ocaml.4.14.4 cb826ea44eb2
ocaml-base-compiler.4.14.4 d2f775f983d7
ocaml-config.2 669e0fcf9e4d
ocamlfind.1.9.8 6025f4a8e98e
zarith.1.14 cde7973b8292
=== STDOUT ===
Processing: [default: loading data]
[coq.8.14.0: dl]
[coq.8.14.0: extract]
[coq.8.14.0/disable_warn_70.patch: dl]
[coq.8.14.0/dune-install-set-root.patch: dl]
[coq.8.14.0/ld_stricter.patch: dl]
-> retrieved coq.8.14.0 (https://opam.ocaml.org/cache)
[coq: patch] applying dune-install-set-root.patch
[coq: patch] applying ld_stricter.patch
[coq: patch] applying disable_warn_70.patch
[coq: ./configure no]
+ /home/opam/.opam/default/.opam-switch/build/coq.8.14.0/./configure "-configdir" "/home/opam/.opam/default/lib/coq/config" "-prefix" "/home/opam/.opam/default" "-mandir" "/home/opam/.opam/default/man" "-docdir" "/home/opam/.opam/default/doc/coq" "-libdir" "/home/opam/.opam/default/lib/coq" "-datadir" "/home/opam/.opam/default/share/coq" "-coqide" "no" "-native-compiler" "no" (CWD=/home/opam/.opam/default/.opam-switch/build/coq.8.14.0)
- You have OCaml 4.14.4. Good!
- You have OCamlfind 1.9.8. Good!
- You have native-code compilation. Good!
- You have the Zarith library 1.14 installed. Good!
- CoqIde manually disabled:
- => no CoqIde will be built.
-
- Architecture : Linux
- Sys.os_type : Unix
- Coq VM bytecode link flags : -dllib -lcoqrun -dllpath /home/opam/.opam/default/lib/coq/kernel/byterun
- Other bytecode link flags :
- OCaml version : 4.14.4
- OCaml binaries in : /home/opam/.opam/default/bin/
- OCaml library in : /home/opam/.opam/default/lib/ocaml
- OCaml flambda flags :
- Native dynamic link support : true
- CoqIde : no
- Documentation : None
- Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
- Coq web site : http://coq.inria.fr/
- Bytecode VM enabled : true
- Native Compiler enabled : no
-
- Paths for true installation:
- - the Coq binaries will be copied in /home/opam/.opam/default/bin
- - the Coq library will be copied in /home/opam/.opam/default/lib/coq
- - the Coqide configuration files will be copied in /home/opam/.opam/default/lib/coq/config
- - the Coqide data files will be copied in /home/opam/.opam/default/share/coq
- - the Coq man pages will be copied in /home/opam/.opam/default/man
- - the Coq documentation will be copied in /home/opam/.opam/default/doc/coq
- - the Coqdoc LaTeX files will be copied in /home/opam/.opam/default/share/texmf/tex/latex/misc
-
- If anything is wrong above, please restart './configure'.
-
- *Warning* To compile the system for a new architecture
- don't forget to do a 'make clean' before './configure'.
[coq: make]
+ /usr/bin/make "COQ_USE_DUNE=" "-j39" (CWD=/home/opam/.opam/default/.opam-switch/build/coq.8.14.0)
- /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build
- make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/coq.8.14.0'
- MKDIR BUILD_OUT
- DUNE _build/install/default/bin/coqdep
- DUNE sources
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -no-alias-deps -o lib/.lib.objs/byte/util.cmi -c -intf lib/util.mli)
- File "lib/util.mli", line 81, characters 27-35:
- 81 | val stream_nth : int -> 'a Stream.t -> 'a
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/util.mli", line 82, characters 29-37:
- 82 | val stream_njunk : int -> 'a Stream.t -> unit
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/native/lStream.cmx -c -impl lib/lStream.ml)
- File "lib/lStream.ml", line 14, characters 12-20:
- 14 | strm : 'a Stream.t;
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 26, characters 4-15:
- 26 | Stream.from
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 35, characters 17-29:
- 35 | let count strm = Stream.count strm.strm
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 38, characters 16-28:
- 38 | strm.fun_loc (Stream.count strm.strm)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 57, characters 10-21:
- 57 | let a = Stream.peek strm.strm in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 58, characters 22-33:
- 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 58, characters 72-84:
- 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek;
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 62, characters 10-22:
- 62 | let l = Stream.npeek n strm.strm in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 63, characters 24-36:
- 63 | strm.max_peek <- max (Stream.count strm.strm + List.length l) strm.max_peek;
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 67, characters 13-25:
- 67 | let list = Stream.npeek (n + 1) strm.strm in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 70, characters 36-48:
- 70 | x :: _, 0 -> strm.max_peek <- Stream.count strm.strm + n + 1; x
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 72, characters 32-44:
- 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 72, characters 72-86:
- 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 76, characters 16-27:
- 76 | let junk strm = Stream.junk strm.strm
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 78, characters 16-27:
- 78 | let next strm = Stream.next strm.strm
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/native/util.cmx -c -impl lib/util.ml)
- File "lib/util.ml", line 126, characters 16-28:
- 126 | try List.nth (Stream.npeek (n+1) st) n
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/util.ml", line 127, characters 26-40:
- 127 | with Failure _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/util.ml", line 130, characters 11-22:
- 130 | repeat n Stream.junk st
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/native/coqProject_file.cmx -c -impl lib/coqProject_file.ml)
- File "lib/coqProject_file.ml", line 100, characters 35-46:
- 100 | let rec parse_string buf s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 105, characters 12-26:
- 105 | | exception Stream.Failure -> buffer buf
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 107, characters 32-43:
- 107 | and parse_string2 buf s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 112, characters 12-26:
- 112 | | exception Stream.Failure -> raise (Parsing_error "unterminated string")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 114, characters 33-44:
- 114 | and parse_skip_comment s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 117, characters 12-26:
- 117 | | exception Stream.Failure -> ()
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 119, characters 34-45:
- 119 | and parse_args buf accu s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 131, characters 12-26:
- 131 | | exception Stream.Failure -> accu
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 138, characters 31-48:
- 138 | let res = parse_args buf [] (Stream.of_channel c) in
- ^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQDEP VFILES
- DUNE sources
- DUNE _build/install/default/bin/coqc
- DUNE _build/default/plugins/ltac/ltac_plugin.cmxs
- DUNE _build/default/plugins/syntax/number_string_notation_plugin.cmxs
- DUNE _build/default/plugins/ltac/tauto_plugin.cmxs
- DUNE _build/default/plugins/cc/cc_plugin.cmxs
- DUNE _build/default/plugins/firstorder/firstorder_plugin.cmxs
- DUNE _build/default/plugins/ssrmatching/ssrmatching_plugin.cmxs
- DUNE _build/default/plugins/ssr/ssreflect_plugin.cmxs
- DUNE _build/default/plugins/ring/ring_plugin.cmxs
- DUNE _build/default/plugins/micromega/zify_plugin.cmxs
- DUNE _build/default/plugins/micromega/micromega_plugin.cmxs
- DUNE _build/default/plugins/extraction/extraction_plugin.cmxs
- DUNE _build/default/plugins/funind/funind_plugin.cmxs
- DUNE _build/default/plugins/ssrsearch/ssrsearch_plugin.cmxs
- DUNE _build/default/plugins/btauto/btauto_plugin.cmxs
- DUNE _build/default/plugins/nsatz/nsatz_plugin.cmxs
- DUNE _build/default/plugins/derive/derive_plugin.cmxs
- DUNE _build/default/plugins/rtauto/rtauto_plugin.cmxs
- DUNE _build/default/plugins/syntax/float_syntax_plugin.cmxs
- DUNE _build/default/user-contrib/Ltac2/ltac2_plugin.cmxs
- DUNE _build/install/default/bin/coqproofworker.opt
- DUNE _build/install/default/bin/coqtacticworker.opt
- DUNE _build/install/default/bin/coqqueryworker.opt
- DUNE _build/install/default/bin/coqtop
- DUNE _build/install/default/bin/coqchk
- DUNE _build/install/default/bin/csdpcert
- DUNE _build/install/default/bin/coqnative
- DUNE _build/install/default/bin/votour
- DUNE _build/install/default/bin/coqdoc
- DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty
- DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css
- DUNE _build/install/default/bin/coqwc
- DUNE _build/install/default/bin/coq_makefile
- DUNE _build/default/tools/CoqMakefile.in
- DUNE _build/install/default/bin/ocamllibdep
- DUNE _build/default/doc/tools/docgram/doc_grammar.exe
- DUNE _build/default/coq-core.install
- DUNE _build/default/coqide-server.install
- DUNE revision
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Plexing.cmi -c -intf gramlib/plexing.mli)
- File "gramlib/plexing.mli", line 14, characters 41-49:
- 14 | type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/native/gramlib__Plexing.cmx -c -impl gramlib/plexing.ml)
- File "gramlib/plexing.ml", line 5, characters 41-49:
- 5 | type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Grammar.cmi -c -intf gramlib/grammar.mli)
- File "gramlib/grammar.mli", line 30, characters 34-42:
- 30 | val make : ?loc:Loc.t -> char Stream.t -> t
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/native/gramlib__Grammar.cmx -c -impl gramlib/grammar.ml)
- File "gramlib/grammar.ml", line 20, characters 34-42:
- 20 | val make : ?loc:Loc.t -> char Stream.t -> t
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1073, characters 15-29:
- 1073 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1082, characters 15-29:
- 1082 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1091, characters 27-41:
- 1091 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1091, characters 61-75:
- 1091 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1095, characters 13-27:
- 1095 | else raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1101, characters 6-20:
- 1101 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son))
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1101, characters 31-43:
- 1101 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1120, characters 4-18:
- 1120 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1127, characters 62-76:
- 1127 | skip_if_empty bp (fun (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1129, characters 11-25:
- 1129 | with Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1162, characters 52-66:
- 1162 | DeadEnd -> (fun (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1173, characters 53-67:
- 1173 | try Some (entry.estart alevn strm__) with Stream.Failure -> None
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1183, characters 31-45:
- 1183 | try p1 strm__ with Stream.Failure -> p2 strm__)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1193, characters 17-31:
- 1193 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1194, characters 26-38:
- 1194 | raise (Stream.Error (tree_failed entry a s son))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1204, characters 43-57:
- 1204 | match try Some (ps strm) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1207, characters 49-63:
- 1207 | (try Some (p1 bp a strm) with Stream.Failure -> None)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1210, characters 34-46:
- 1210 | | None -> raise (Stream.Error (tree_failed entry a s son))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1217, characters 4-18:
- 1217 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1245, characters 66-80:
- 1245 | (match (try Some (tematch (LStream.peek_nth n strm)) with Stream.Failure -> None) with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1247, characters 44-58:
- 1247 | (match try Some (p1 a strm) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1251, characters 42-56:
- 1251 | | DeadEnd -> fun last_a strm -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1257, characters 35-49:
- 1257 | try Some (ps strm) with Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1259, characters 87-101:
- 1259 | try Some (parser_of_tree entry nlevn alevn (top_tree entry tree) strm) with Stream.Failure -> None
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1262, characters 26-38:
- 1262 | | None -> raise (Stream.Error (tree_failed entry last_a (Stoken last_tok) tree))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1269, characters 20-34:
- 1269 | | None -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1277, characters 43-57:
- 1277 | match try Some (ps al strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1287, characters 40-54:
- 1287 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1291, characters 16-30:
- 1291 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1292, characters 25-37:
- 1292 | raise (Stream.Error (symb_failed entry v sep symb))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1298, characters 44-58:
- 1298 | match try Some (ps [] strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1305, characters 40-54:
- 1305 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1308, characters 44-58:
- 1308 | (try Some (ps al strm__) with Stream.Failure -> None)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1316, characters 44-58:
- 1316 | match try Some (ps [] strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1322, characters 43-57:
- 1322 | match try Some (ps al strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1333, characters 40-54:
- 1333 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1337, characters 16-30:
- 1337 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1340, characters 22-36:
- 1340 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1341, characters 31-43:
- 1341 | raise (Stream.Error (symb_failed entry v sep symb))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1355, characters 40-54:
- 1355 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1358, characters 44-58:
- 1358 | (try Some (ps al strm__) with Stream.Failure -> None)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1364, characters 20-34:
- 1364 | Stream.Failure -> None
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1377, characters 41-55:
- 1377 | match try Some (ps strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1400, characters 20-34:
- 1400 | | None -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1434, characters 52-66:
- 1434 | [] -> (fun levn (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1470, characters 50-64:
- 1470 | match try Some (p2 strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1491, characters 57-71:
- 1491 | [] -> (fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1510, characters 16-30:
- 1510 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1521, characters 37-51:
- 1521 | try p levn bp a strm__ with Stream.Failure -> a)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1522, characters 63-77:
- 1522 | | Dparser p -> fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1525, characters 9-21:
- 1525 | raise (Stream.Error ("entry [" ^ ename ^ "] is empty"))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1586, characters 6-20:
- 1586 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1589, characters 6-18:
- 1589 | | Stream.Error _ as exc ->
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1588, characters 22-34:
- 1588 | Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1629, characters 51-65:
- 1629 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1642, characters 51-65:
- 1642 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1728, characters 55-69:
- 1728 | e.estart <- (fun _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1729, characters 62-76:
- 1729 | e.econtinue <- (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 -Wall -Wno-unused -g -O2 -msse2 -mfpmath=sse -g -I /home/opam/.opam/default/lib/ocaml -o coq_fix_code.o -c coq_fix_code.c)
- coq_fix_code.c: In function 'coq_stat_alloc':
- coq_fix_code.c:36:13: warning: "raise_out_of_memory" is deprecated: use "caml_raise_out_of_memory" instead
- 36 | if (result == NULL) raise_out_of_memory ();
- | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- (cd _build/default/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 -Wall -Wno-unused -g -O2 -msse2 -mfpmath=sse -g -I /home/opam/.opam/default/lib/ocaml -o coq_memory.o -c coq_memory.c)
- coq_memory.c: In function 'init_coq_vm':
- coq_memory.c:114:13: warning: "scan_roots_hook" is deprecated: use "caml_scan_roots_hook" instead
- 114 | coq_prev_scan_roots_hook = scan_roots_hook;
- | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- coq_memory.c:115:13: warning: "scan_roots_hook" is deprecated: use "caml_scan_roots_hook" instead
- 115 | scan_roots_hook = coq_scan_roots;
- | ^~~~~~~~~~~~~~~~~~~~~~~~~
- (cd _build/default/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 -Wall -Wno-unused -g -O2 -msse2 -mfpmath=sse -g -I /home/opam/.opam/default/lib/ocaml -o coq_interp.o -c coq_interp.c)
- coq_interp.c: In function 'coq_interprete':
- coq_interp.c:287:20: warning: storing the address of local variable 'coq_lbl_ACC0' in 'coq_instr_base' [-Wdangling-pointer=]
- 287 | coq_instr_base = coq_Jumptbl_base;
- | ^
- coq_interp.c:74:26: note: 'coq_lbl_ACC0' declared here
- 74 | # define Instruct(name) coq_lbl_##name:
- | ^~~~~~~~
- coq_interp.c:311:7: note: in expansion of macro 'Instruct'
- 311 | Instruct(ACC0){
- | ^~~~~~~~
- In file included from coq_interp.c:28:
- coq_fix_code.h:20:15: note: 'coq_instr_base' declared here
- 20 | extern char * coq_instr_base;
- | ^~~~~~~~~~~~~~
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -no-alias-deps -o interp/.interp.objs/byte/numTok.cmi -c -intf interp/numTok.mli)
- File "interp/numTok.mli", line 85, characters 19-27:
- 85 | val parse : char Stream.t -> t
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -no-alias-deps -o parsing/.parsing.objs/byte/g_constr.cmo -c -impl parsing/g_constr.ml)
- File "parsing/g_constr.mlg", line 46, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -no-alias-deps -o toplevel/.toplevel.objs/byte/g_toplevel.cmo -c -impl toplevel/g_toplevel.ml)
- File "toplevel/g_toplevel.mlg", line 34, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I engine/.engine.objs/byte -I engine/.engine.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -intf-suffix .ml -no-alias-deps -o engine/.engine.objs/native/evarutil.cmx -c -impl engine/evarutil.ml)
- File "engine/evarutil.ml", line 131, characters 10-18:
- 131 | let m = E.create () in
- ^^^^^^^^
- Alert old_ephemeron_api: E.create
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 132, characters 19-29:
- 132 | fun x y -> match E.get_key1 m, E.get_key2 m with
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.get_key1
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 132, characters 33-43:
- 132 | fun x y -> match E.get_key1 m, E.get_key2 m with
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.get_key2
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 133, characters 60-70:
- 133 | | Some x', Some y' when x == x' && y == y' -> Option.get (E.get_data m)
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.get_data
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 134, characters 26-36:
- 134 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.set_key1
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 134, characters 42-52:
- 134 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.set_key2
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 134, characters 58-68:
- 134 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.set_data
- This function won't be available in 5.0
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/native/numTok.cmx -c -impl interp/numTok.ml)
- File "interp/numTok.ml", line 124, characters 33-44:
- 124 | let rec number len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 125, characters 32-43:
- 125 | | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 126, characters 40-51:
- 126 | | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 129, characters 37-48:
- 129 | let rec hex_number len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 131, characters 9-20:
- 131 | Stream.junk s; hex_number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 133, characters 9-20:
- 133 | Stream.junk s; hex_number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 137, characters 12-24:
- 137 | match Stream.npeek 3 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 139, characters 9-20:
- 139 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 139, characters 24-35:
- 139 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 139, characters 39-50:
- 139 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 144, characters 17-29:
- 144 | match hex, Stream.npeek 2 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 146, characters 9-20:
- 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 146, characters 24-35:
- 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 148, characters 9-20:
- 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 148, characters 24-35:
- 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 151, characters 17-29:
- 151 | match hex, Stream.npeek 2 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 154, characters 9-20:
- 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 154, characters 24-35:
- 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 157, characters 21-33:
- 157 | begin match Stream.npeek 3 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 159, characters 12-23:
- 159 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 159, characters 27-38:
- 159 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 159, characters 42-53:
- 159 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 174, characters 17-33:
- 174 | let strm = Stream.of_string (s ^ " ") in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 176, characters 9-21:
- 176 | if Stream.count strm >= String.length s then Some n else None
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 260, characters 17-33:
- 260 | let strm = Stream.of_string (s ^ " ") in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 262, characters 18-29:
- 262 | | '-' -> (Stream.junk strm; SMinus)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 263, characters 18-29:
- 263 | | '+' -> (Stream.junk strm; SPlus)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 266, characters 9-21:
- 266 | if Stream.count strm >= String.length s then Some (sign,n) else None
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/native/constrexpr_ops.cmx -c -impl interp/constrexpr_ops.ml)
- File "interp/constrexpr_ops.ml", line 569, characters 24-36:
- 569 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/native/constrintern.cmx -c -impl interp/constrintern.ml)
- File "interp/constrintern.ml", line 586, characters 22-34:
- 586 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/tok.cmx -c -impl parsing/tok.ml)
- File "parsing/tok.ml", line 124, characters 21-35:
- 124 | let err () = raise Stream.Failure in
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/cLexer.cmx -c -impl parsing/cLexer.ml)
- File "parsing/cLexer.ml", line 162, characters 11-23:
- 162 | let bp = Stream.count cs in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 163, characters 2-13:
- 163 | Stream.junk cs; (* consume the char to avoid read it and fail again *)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 175, characters 28-39:
- 175 | let njunk n = Util.repeat n Stream.junk
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 188, characters 12-24:
- 188 | match Stream.npeek 2 cs with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 194, characters 12-24:
- 194 | match Stream.npeek 3 cs with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 201, characters 17-29:
- 201 | else match Stream.npeek 4 cs with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 213, characters 8-19:
- 213 | match Stream.peek cs with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 225, characters 30-41:
- 225 | let rec loop_symb s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 227, characters 8-19:
- 227 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 232, characters 23-34:
- 232 | | AsciiChar -> Stream.junk s; loop_symb s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 235, characters 13-29:
- 235 | loop_symb (Stream.of_string str)
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 238, characters 35-46:
- 238 | let rec loop_id intail s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 240, characters 8-19:
- 240 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 243, characters 8-19:
- 243 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 254, characters 17-33:
- 254 | loop_id false (Stream.of_string str)
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 296, characters 39-50:
- 296 | if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 308, characters 37-48:
- 308 | let rec ident_tail loc len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 310, characters 6-17:
- 310 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 318, characters 62-74:
- 318 | let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 332, characters 48-59:
- 332 | let rec string loc ~comm_level bp len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 334, characters 6-17:
- 334 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 336, characters 14-25:
- 336 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 337, characters 22-33:
- 337 | Some '"' -> Stream.junk s; true
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 342, characters 6-17:
- 342 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 343, characters 22-33:
- 343 | (fun s -> match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 345, characters 8-19:
- 345 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 353, characters 6-17:
- 353 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 354, characters 22-33:
- 354 | (fun s -> match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 356, characters 12-23:
- 356 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 367, characters 4-15:
- 367 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 368, characters 13-25:
- 368 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 378, characters 6-17:
- 378 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 381, characters 14-26:
- 381 | let _ = Stream.empty s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 382, characters 15-27:
- 382 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 436, characters 12-24:
- 436 | let bp2 = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 437, characters 8-19:
- 437 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 439, characters 6-17:
- 439 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 442, characters 16-27:
- 442 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 444, characters 14-25:
- 444 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 447, characters 13-27:
- 447 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 447, characters 38-50:
- 447 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 451, characters 6-17:
- 451 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 453, characters 14-25:
- 453 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 454, characters 22-33:
- 454 | Some ')' -> Stream.junk s; push_string "*)"; loc
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 456, characters 11-25:
- 456 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 456, characters 36-48:
- 456 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 459, characters 6-17:
- 459 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 464, characters 20-32:
- 464 | match try Some (Stream.empty s) with Stream.Failure -> None with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 464, characters 41-55:
- 464 | match try Some (Stream.empty s) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 466, characters 15-27:
- 466 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 470, characters 16-27:
- 470 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 472, characters 14-25:
- 472 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 473, characters 23-35:
- 473 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 476, characters 14-25:
- 476 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 478, characters 23-37:
- 478 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 485, characters 54-66:
- 485 | try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 504, characters 36-48:
- 504 | match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 518, characters 8-19:
- 518 | match Stream.peek cs with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 529, characters 16-30:
- 529 | | exception Stream.Failure -> n, List.make n b, List.make n e
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 532, characters 24-38:
- 532 | if len = 0 then raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 541, characters 17-31:
- 541 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 546, characters 14-25:
- 546 | let c = Stream.next s in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 549, characters 10-24:
- 549 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 549, characters 35-47:
- 549 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 551, characters 40-52:
- 551 | get_buff len, set_loc_pos loc bp (Stream.count s)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 559, characters 43-54:
- 559 | let commit1 c = Buffer.add_char b c; Stream.junk s in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 562, characters 14-26:
- 562 | match Stream.npeek lenmarker s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 571, characters 48-60:
- 571 | let loc = bump_loc_line_last loc (Stream.count s) in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 575, characters 63-77:
- 575 | if not dot_gobbling && blank_or_eof s then raise Stream.Failure;
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 580, characters 22-36:
- 580 | | [] -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 583, characters 45-57:
- 583 | Buffer.contents b, set_loc_pos loc bp (Stream.count s)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 590, characters 15-27:
- 590 | let l' = Stream.npeek (i + 1) s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 600, characters 6-17:
- 600 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 609, characters 15-27:
- 609 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 617, characters 10-21:
- 617 | match Stream.peek cs with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 618, characters 30-41:
- 618 | | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 619, characters 57-69:
- 619 | | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 626, characters 11-23:
- 626 | let ep = Stream.count cs in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 647, characters 50-61:
- 647 | let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 649, characters 6-17:
- 649 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 652, characters 10-24:
- 652 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 652, characters 35-47:
- 652 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 657, characters 17-29:
- 657 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 666, characters 21-33:
- 666 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 674, characters 8-19:
- 674 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 686, characters 11-23:
- 686 | let bp = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 687, characters 8-19:
- 687 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 689, characters 6-17:
- 689 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 690, characters 15-27:
- 690 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 693, characters 6-17:
- 693 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 696, characters 6-17:
- 696 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 699, characters 10-24:
- 699 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 699, characters 35-47:
- 699 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 707, characters 21-33:
- 707 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 715, characters 6-17:
- 715 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 722, characters 6-17:
- 722 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 723, characters 15-27:
- 723 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 727, characters 6-17:
- 727 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 730, characters 10-24:
- 730 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 730, characters 35-47:
- 730 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 736, characters 17-29:
- 736 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 740, characters 15-27:
- 740 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 744, characters 6-17:
- 744 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 747, characters 10-24:
- 747 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 747, characters 35-47:
- 747 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 749, characters 15-27:
- 749 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 753, characters 6-17:
- 753 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 755, characters 14-25:
- 755 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 757, characters 12-23:
- 757 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 758, characters 21-33:
- 758 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 761, characters 12-23:
- 761 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 766, characters 11-25:
- 766 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 766, characters 36-48:
- 766 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 769, characters 6-17:
- 769 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 770, characters 15-27:
- 770 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 784, characters 23-35:
- 784 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 787, characters 53-64:
- 787 | let t = process_chars ~diff_mode loc bp (Stream.next s) s in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/pcoq.cmx -c -impl parsing/pcoq.ml)
- File "parsing/pcoq.ml", line 22, characters 21-35:
- 22 | let err () = raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/pcoq.ml", line 199, characters 13-29:
- 199 | let strm = Stream.of_string x in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/native/g_constr.cmx -c -impl parsing/g_constr.ml)
- File "parsing/g_constr.mlg", line 46, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I printing/.printing.objs/byte -I printing/.printing.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -intf-suffix .ml -no-alias-deps -o printing/.printing.objs/native/proof_diffs.cmx -c -impl printing/proof_diffs.ml)
- File "printing/proof_diffs.ml", line 102, characters 15-31:
- 102 | let istr = Stream.of_string s in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/himsg.cmx -c -impl vernac/himsg.ml)
- File "vernac/himsg.ml", line 1413, characters 4-16:
- 1413 | | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/proof_using.cmx -c -impl vernac/proof_using.ml)
- File "vernac/proof_using.ml", line 178, characters 94-110:
- 178 | let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/comInductive.cmx -c -impl vernac/comInductive.ml)
- File "vernac/comInductive.ml", line 365, characters 20-32:
- 365 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/record.cmx -c -impl vernac/record.ml)
- File "vernac/record.ml", line 120, characters 20-32:
- 120 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/vernacinterp.cmx -c -impl vernac/vernacinterp.ml)
- File "vernac/vernacinterp.ml", line 189, characters 64-81:
- 189 | Pcoq.Parsable.make ~loc:(Loc.(initial (InFile longfname))) (Stream.of_channel in_chan) in
- ^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/native/g_toplevel.cmx -c -impl toplevel/g_toplevel.ml)
- File "toplevel/g_toplevel.mlg", line 34, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/native/vernac.cmx -c -impl toplevel/vernac.ml)
- File "toplevel/vernac.ml", line 92, characters 7-24:
- 92 | (Stream.of_channel in_chan) in
- ^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/native/coqloop.cmx -c -impl toplevel/coqloop.ml)
- File "toplevel/coqloop.ml", line 79, characters 37-48:
- 79 | ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf));
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "toplevel/coqloop.ml", line 233, characters 33-47:
- 233 | tokens = Pcoq.Parsable.make (Stream.of_list []);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQCBOOT theories/Init/Notations.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I plugins/ltac/.ltac_plugin.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -no-alias-deps -open Ltac_plugin -o plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_tactic.cmo -c -impl plugins/ltac/g_tactic.ml)
- File "plugins/ltac/g_tactic.mlg", line 33, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I plugins/ltac/.ltac_plugin.objs/byte -I plugins/ltac/.ltac_plugin.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -open Ltac_plugin -o plugins/ltac/.ltac_plugin.objs/native/ltac_plugin__G_tactic.cmx -c -impl plugins/ltac/g_tactic.ml)
- File "plugins/ltac/g_tactic.mlg", line 33, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQCBOOT theories/Init/Ltac.v
- COQCBOOT theories/Init/Logic.v
- COQCBOOT theories/Init/Datatypes.v
- COQCBOOT theories/Init/Logic_Type.v
- COQCBOOT theories/Init/Specif.v
- COQCBOOT theories/Init/Wf.v
- COQCBOOT theories/Init/Tauto.v
- COQCBOOT theories/Init/Decimal.v
- COQCBOOT theories/Init/Tactics.v
- COQCBOOT theories/Init/Hexadecimal.v
- COQCBOOT theories/Init/Number.v
- COQCBOOT theories/Init/Nat.v
- COQCBOOT theories/Init/Numeral.v
- COQCBOOT theories/Init/Byte.v
- COQCBOOT theories/Init/Peano.v
- COQCBOOT theories/Init/Prelude.v
- COQC theories/Bool/Bool.v
- COQC theories/ssr/ssrclasses.v
- COQC theories/Program/Basics.v
- COQC theories/Program/Tactics.v
- COQC theories/Relations/Relation_Definitions.v
- COQC theories/Logic/EqdepFacts.v
- COQC theories/Logic/Decidable.v
- COQC theories/Wellfounded/Inverse_Image.v
- COQC theories/Numbers/BinNums.v
- COQC theories/Bool/Sumbool.v
- COQC theories/micromega/ZifyClasses.v
- COQC theories/Unicode/Utf8_core.v
- COQC theories/Numbers/Cyclic/Abstract/CarryType.v
- COQC theories/Logic/FunctionalExtensionality.v
- COQC theories/Logic/PropExtensionalityFacts.v
- COQC theories/Logic/Hurkens.v
- COQC theories/Program/Utils.v
- COQC theories/Logic/ProofIrrelevanceFacts.v
- COQC theories/Sets/Relations_1.v
- COQC theories/setoid_ring/Algebra_syntax.v
- COQC theories/Sets/Ensembles.v
- COQC theories/Bool/BoolEq.v
- COQC theories/Bool/IfProp.v
- COQC theories/Bool/DecBool.v
- COQC theories/Sets/Permut.v
- COQC theories/Sets/Relations_2.v
- COQC theories/Compat/Coq814.v
- COQC theories/Compat/AdmitAxiom.v
- COQC theories/Logic/RelationalChoice.v
- COQC theories/Logic/ExtensionalFunctionRepresentative.v
- COQC theories/Logic/PropFacts.v
- COQC theories/Logic/SetIsType.v
- COQC theories/Logic/Berardi.v
- COQC theories/Logic/ExtensionalityFacts.v
- COQC theories/Logic/StrictProp.v
- COQC theories/Floats/FloatClass.v
- COQC theories/Numbers/AltBinNotations.v
- COQC theories/Lists/Streams.v
- COQC theories/ssrmatching/ssrmatching.v
- COQC theories/ssr/ssrunder.v
- COQC theories/Classes/Init.v
- COQC theories/Logic/Eqdep.v
- COQC theories/Relations/Relation_Operators.v
- COQC theories/Wellfounded/Inclusion.v
- COQC theories/Logic/Eqdep_dec.v
- COQC theories/PArith/BinPosDef.v
- COQC theories/Unicode/Utf8.v
- COQC theories/Numbers/Cyclic/Int63/PrimInt63.v
- COQC theories/Logic/HLevels.v
- COQC theories/Logic/JMeq.v
- COQC theories/Logic/ProofIrrelevance.v
- COQC theories/Program/Combinators.v
- COQC theories/Sets/Constructive_sets.v
- COQC theories/Sets/Relations_1_facts.v
- COQC theories/Sets/Partial_Order.v
- COQC theories/Sets/Uniset.v
- COQC theories/Sets/Relations_3.v
- COQC theories/Lists/StreamMemo.v
- COQC theories/Classes/RelationClasses.v
- COQC theories/Wellfounded/Well_Ordering.v
- COQC theories/Wellfounded/Transitive_Closure.v
- COQC theories/Classes/CRelationClasses.v
- COQC theories/Relations/Operators_Properties.v
- COQC theories/Wellfounded/Disjoint_Union.v
- COQC theories/Wellfounded/Lexicographic_Product.v
- COQC theories/Program/Equality.v
- COQC theories/Sets/Finite_sets.v
- COQC theories/Sets/Cpo.v
- COQC theories/Sets/Relations_2_facts.v
- COQC theories/ssr/ssrsetoid.v
- COQC theories/Wellfounded/Union.v
- COQC theories/Classes/Morphisms.v
- COQC theories/Program/Subset.v
- COQC theories/Sets/Powerset.v
- COQC theories/Sets/Relations_3_facts.v
- COQC theories/Relations/Relations.v
- COQC theories/Sets/Powerset_facts.v
- COQC theories/Classes/CMorphisms.v
- COQC theories/Classes/Morphisms_Prop.v
- COQC theories/Classes/Equivalence.v
- COQC theories/Classes/SetoidTactics.v
- COQC theories/Classes/CEquivalence.v
- COQC theories/Setoids/Setoid.v
- COQC theories/Structures/Equalities.v
- COQC theories/Numbers/NumPrelude.v
- COQC theories/Structures/Orders.v
- COQC theories/Structures/OrdersTac.v
- COQC theories/Bool/BoolOrder.v
- COQC theories/Structures/OrdersFacts.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -open Gramlib -g -O3 -unbox-closures -I plugins/ssr/.ssreflect_plugin.objs/byte -I plugins/ssr/.ssreflect_plugin.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I plugins/ltac/.ltac_plugin.objs/byte -I plugins/ltac/.ltac_plugin.objs/native -I plugins/ssrmatching/.ssrmatching_plugin.objs/byte -I plugins/ssrmatching/.ssrmatching_plugin.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -open Ssreflect_plugin -o plugins/ssr/.ssreflect_plugin.objs/native/ssreflect_plugin__Ssrparser.cmx -c -impl plugins/ssr/ssrparser.ml)
- File "plugins/ssr/ssrparser.mlg", line 263, characters 28-42:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 265, characters 22-36:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 272, characters 24-38:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 274, characters 22-36:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 276, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 283, characters 24-38:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 285, characters 22-36:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 286, characters 15-29:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 294, characters 31-45:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 297, characters 20-34:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 844, characters 33-47:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 853, characters 9-23:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 858, characters 12-26:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 859, characters 55-69:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 860, characters 45-59:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 2411, characters 37-51:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 2415, characters 17-31:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/Structures/GenericMinMax.v
- COQC theories/ssr/ssreflect.v
- COQC theories/ssr/ssrfun.v
- COQC theories/ssr/ssrbool.v
- COQC theories/Numbers/NatInt/NZAxioms.v
- COQC theories/Numbers/NatInt/NZBase.v
- COQC theories/Numbers/NatInt/NZAdd.v
- COQC theories/Numbers/NatInt/NZOrder.v
- COQC theories/Numbers/NatInt/NZMul.v
- COQC theories/Numbers/NatInt/NZAddOrder.v
- COQC theories/Numbers/NatInt/NZMulOrder.v
- COQC theories/Numbers/NatInt/NZParity.v
- COQC theories/Numbers/NatInt/NZPow.v
- COQC theories/Numbers/NatInt/NZSqrt.v
- COQC theories/Numbers/NatInt/NZDiv.v
- COQC theories/Numbers/NatInt/NZGcd.v
- COQC theories/Numbers/NatInt/NZProperties.v
- COQC theories/Numbers/NatInt/NZLog.v
- COQC theories/extraction/Extraction.v
- COQC theories/Program/Wf.v
- COQC theories/extraction/ExtrOcamlBasic.v
- COQC theories/extraction/ExtrHaskellBasic.v
- COQC theories/Numbers/NatInt/NZBits.v
- COQC theories/Numbers/Natural/Abstract/NAxioms.v
- COQC theories/Numbers/Integer/Abstract/ZAxioms.v
- COQC theories/Numbers/Integer/Abstract/ZBase.v
- COQC theories/Numbers/Natural/Abstract/NBase.v
- COQC theories/Numbers/Integer/Abstract/ZAdd.v
- COQC theories/Numbers/Natural/Abstract/NAdd.v
- COQC theories/Numbers/Natural/Abstract/NIso.v
- COQC theories/Numbers/Integer/Abstract/ZMul.v
- COQC theories/Numbers/Natural/Abstract/NOrder.v
- COQC theories/Numbers/Integer/Abstract/ZLt.v
- COQC theories/Numbers/Integer/Abstract/ZAddOrder.v
- COQC theories/Numbers/Natural/Abstract/NAddOrder.v
- COQC theories/Numbers/Natural/Abstract/NMulOrder.v
- COQC theories/Numbers/Natural/Abstract/NSub.v
- COQC theories/Numbers/Integer/Abstract/ZMulOrder.v
- COQC theories/funind/FunInd.v
- COQC theories/Numbers/Natural/Abstract/NMaxMin.v
- COQC theories/Numbers/Natural/Abstract/NParity.v
- COQC theories/Numbers/Natural/Abstract/NSqrt.v
- COQC theories/Numbers/Natural/Abstract/NDiv.v
- COQC theories/Numbers/Natural/Abstract/NGcd.v
- COQC theories/Numbers/Natural/Abstract/NStrongRec.v
- COQC theories/Numbers/Integer/Abstract/ZMaxMin.v
- COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v
- COQC theories/Numbers/Integer/Abstract/ZParity.v
- COQC theories/Numbers/Natural/Abstract/NPow.v
- COQC theories/ssrsearch/ssrsearch.v
- COQC theories/Numbers/Natural/Abstract/NLcm.v
- COQC theories/Numbers/Natural/Abstract/NLog.v
- COQC theories/Numbers/Natural/Abstract/NBits.v
- COQC theories/Numbers/Integer/Abstract/ZPow.v
- COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v
- COQC theories/Numbers/Integer/Abstract/ZDivFloor.v
- COQC theories/Numbers/Integer/Abstract/ZGcd.v
- COQC theories/Numbers/Integer/Abstract/ZDivEucl.v
- COQC theories/Numbers/Integer/Abstract/ZBits.v
- COQC theories/Numbers/Integer/Abstract/ZLcm.v
- COQC theories/Numbers/Natural/Abstract/NProperties.v
- COQC theories/derive/Derive.v
- COQC theories/Arith/PeanoNat.v
- COQC theories/Lists/List.v
- COQC theories/Arith/Le.v
- COQC theories/Arith/EqNat.v
- COQC theories/Arith/Max.v
- COQC theories/Arith/Min.v
- COQC theories/Arith/Even.v
- COQC theories/Arith/Lt.v
- COQC theories/Arith/Plus.v
- COQC theories/Arith/Minus.v
- COQC theories/Arith/Between.v
- COQC theories/Arith/Peano_dec.v
- COQC theories/Numbers/Integer/Abstract/ZProperties.v
- COQC theories/Floats/PrimFloat.v
- COQC theories/Arith/Div2.v
- COQC theories/Numbers/Natural/Peano/NPeano.v
- COQC theories/PArith/BinPos.v
- COQC theories/Arith/Gt.v
- COQC theories/Arith/Mult.v
- COQC theories/Sets/Multiset.v
- COQC theories/Numbers/NatInt/NZDomain.v
- COQC theories/Arith/Compare_dec.v
- COQC theories/Arith/Factorial.v
- COQC theories/Arith/Wf_nat.v
- COQC theories/Arith/Bool_nat.v
- COQC theories/Arith/Arith_base.v
- COQC theories/Logic/ClassicalFacts.v
- COQC theories/funind/Recdef.v
- COQC theories/Arith/Euclid.v
- COQC theories/Vectors/Fin.v
- COQC theories/Arith/Compare.v
- COQC theories/Logic/Classical_Prop.v
- COQC theories/Logic/PropExtensionality.v
- COQC theories/Vectors/VectorDef.v
- COQC theories/Logic/Classical_Pred_Type.v
- COQC theories/Logic/Classical.v
- COQC theories/Sets/Classical_sets.v
- COQC theories/Logic/ClassicalUniqueChoice.v
- COQC theories/NArith/BinNatDef.v
- COQC theories/PArith/Pnat.v
- COQC theories/PArith/POrderedType.v
- COQC theories/Sets/Powerset_Classical_facts.v
- COQC theories/NArith/BinNat.v
- COQC theories/Wellfounded/Lexicographic_Exponentiation.v
- COQC theories/setoid_ring/BinList.v
- COQC theories/Lists/ListTactics.v
- COQC theories/Vectors/VectorSpec.v
- COQC theories/micromega/Refl.v
- COQC theories/Lists/ListDec.v
- COQC theories/Sorting/Sorted.v
- COQC theories/Logic/WeakFan.v
- COQC theories/rtauto/Bintree.v
- COQC theories/Numbers/NaryFunctions.v
- COQC theories/Lists/ListSet.v
- COQC theories/PArith/PArith.v
- COQC theories/Sets/Finite_sets_facts.v
- COQC theories/Lists/SetoidList.v
- COQC theories/Wellfounded/Wellfounded.v
- COQC theories/Logic/FinFun.v
- COQC theories/rtauto/Rtauto.v
- COQC theories/Sets/Image.v
- COQC theories/micromega/Tauto.v
- COQC theories/ZArith/BinIntDef.v
- COQC theories/NArith/Nnat.v
- COQC theories/setoid_ring/Ring_theory.v
- COQC theories/NArith/Ndiv_def.v
- COQC theories/NArith/Nsqrt_def.v
- COQC theories/NArith/Ngcd_def.v
- COQC theories/Numbers/Natural/Binary/NBinary.v
- COQC theories/Sets/Infinite_sets.v
- COQC theories/Sorting/Permutation.v
- COQC theories/ZArith/BinInt.v
- COQC theories/Sets/Integers.v
- COQC user-contrib/Ltac2/Init.v
- COQC user-contrib/Ltac2/Std.v
- COQC user-contrib/Ltac2/Ltac1.v
- COQC user-contrib/Ltac2/Message.v
- COQC user-contrib/Ltac2/Bool.v
- COQC user-contrib/Ltac2/Ind.v
- COQC user-contrib/Ltac2/String.v
- COQC user-contrib/Ltac2/Int.v
- COQC user-contrib/Ltac2/Char.v
- COQC user-contrib/Ltac2/Ident.v
- COQC user-contrib/Ltac2/Constr.v
- COQC theories/Vectors/VectorEq.v
- COQC user-contrib/Ltac2/Control.v
- COQC user-contrib/Ltac2/Printf.v
- COQC user-contrib/Ltac2/Env.v
- COQC user-contrib/Ltac2/Option.v
- COQC user-contrib/Ltac2/List.v
- COQC user-contrib/Ltac2/Array.v
- COQC user-contrib/Ltac2/Pattern.v
- COQC theories/Vectors/Vector.v
- COQC theories/Strings/Byte.v
- COQC user-contrib/Ltac2/Fresh.v
- COQC user-contrib/Ltac2/Notations.v
- COQC user-contrib/Ltac2/Ltac2.v
- COQC theories/Bool/Bvector.v
- COQC theories/Program/Syntax.v
- COQC theories/Program/Program.v
- COQC theories/Classes/RelationPairs.v
- COQC theories/Structures/OrderedType.v
- COQC theories/Structures/DecidableType.v
- COQC theories/Classes/SetoidClass.v
- COQC theories/Classes/EquivDec.v
- COQC theories/Classes/Morphisms_Relations.v
- COQC theories/Structures/EqualitiesFacts.v
- COQC theories/MSets/MSetInterface.v
- COQC theories/Numbers/Natural/Abstract/NDefOps.v
- COQC theories/Sorting/Mergesort.v
- COQC theories/Sorting/CPermutation.v
- COQC theories/Lists/SetoidPermutation.v
- COQC theories/Structures/OrderedTypeAlt.v
- COQC theories/Structures/OrdersAlt.v
- COQC theories/FSets/FSetInterface.v
- COQC theories/FSets/FMapInterface.v
- COQC theories/Sorting/Sorting.v
- COQC theories/FSets/FSetBridge.v
- COQC theories/FSets/FMapList.v
- COQC theories/FSets/FMapWeakList.v
- COQC theories/Structures/OrdersLists.v
- COQC theories/MSets/MSetWeakList.v
- COQC theories/MSets/MSetList.v
- COQC theories/ZArith/Zcompare.v
- COQC theories/ZArith/Zeven.v
- COQC theories/ZArith/Znat.v
- COQC theories/ZArith/Zpow_def.v
- COQC theories/setoid_ring/Ring_polynom.v
- COQC theories/micromega/Env.v
- COQC theories/Numbers/Cyclic/Abstract/DoubleType.v
- COQC theories/ZArith/Zeuclid.v
- COQC theories/ZArith/Zpow_alt.v
- COQC theories/ZArith/Int.v
- COQC theories/Numbers/Integer/Binary/ZBinary.v
- COQC theories/micromega/EnvRing.v
- COQC theories/ZArith/Zorder.v
- COQC theories/ZArith/Zminmax.v
- COQC theories/ZArith/Zmin.v
- COQC theories/ZArith/Zmax.v
- COQC theories/ZArith/ZArith_dec.v
- COQC theories/ZArith/auxiliary.v
- COQC theories/ZArith/Zmisc.v
- COQC theories/omega/OmegaLemmas.v
- COQC theories/ZArith/Wf_Z.v
- COQC theories/ZArith/Zabs.v
- COQC theories/ZArith/Zbool.v
- COQC theories/ZArith/Zhints.v
- COQC theories/ZArith/ZArith_base.v
- COQC theories/micromega/VarMap.v
- COQC theories/setoid_ring/Ncring.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I checker/.coq_checklib.objs/byte -I checker/.coq_checklib.objs/native -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -intf-suffix .ml -no-alias-deps -open Coq_checklib -o checker/.coq_checklib.objs/native/coq_checklib__Checker.cmx -c -impl checker/checker.ml)
- File "checker/checker.ml", line 230, characters 4-18:
- 230 | | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "checker/checker.ml", line 232, characters 4-16:
- 232 | | Stream.Error txt ->
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/setoid_ring/InitialRing.v
- COQC theories/setoid_ring/Ncring_polynom.v
- COQC theories/Strings/Ascii.v
- COQC theories/setoid_ring/Ring_tac.v
- COQC theories/setoid_ring/Ring_base.v
- COQC theories/setoid_ring/Ring.v
- COQC theories/setoid_ring/ArithRing.v
- COQC theories/micromega/OrderedRing.v
- COQC theories/setoid_ring/NArithRing.v
- COQC theories/setoid_ring/ZArithRing.v
- COQC theories/setoid_ring/Field_theory.v
- COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v
- COQC theories/micromega/Ztac.v
- COQC theories/ZArith/Zcomplements.v
- COQC theories/QArith/QArith_base.v
- COQC theories/Arith/Arith.v
- COQC theories/micromega/ZifyInst.v
- COQC theories/Strings/String.v
- COQC theories/Logic/ConstructiveEpsilon.v
- COQC theories/Classes/SetoidDec.v
- COQC theories/Bool/Zerob.v
- COQC theories/MSets/MSetGenTree.v
- COQC theories/Logic/ChoiceFacts.v
- COQC theories/Logic/WKL.v
- COQC theories/extraction/ExtrOcamlNatInt.v
- COQC theories/extraction/ExtrHaskellNatNum.v
- COQC theories/extraction/ExtrOcamlNatBigInt.v
- COQC theories/ZArith/Zdiv.v
- COQC theories/ZArith/Zpower.v
- COQC theories/extraction/ExtrHaskellNatInt.v
- COQC theories/extraction/ExtrHaskellNatInteger.v
- COQC theories/micromega/Zify.v
- COQC theories/micromega/ZifyPow.v
- COQC theories/Strings/ByteVector.v
- COQC theories/Structures/OrdersEx.v
- COQC theories/Strings/HexString.v
- COQC theories/Strings/BinaryString.v
- COQC theories/Strings/OctalString.v
- COQC theories/Numbers/HexadecimalString.v
- COQC theories/Numbers/DecimalString.v
- COQC theories/extraction/ExtrHaskellString.v
- COQC theories/extraction/ExtrOcamlChar.v
- COQC theories/omega/PreOmega.v
- COQC theories/extraction/ExtrOcamlNativeString.v
- COQC theories/extraction/ExtrOcamlString.v
- COQC theories/NArith/Ndigits.v
- COQC theories/micromega/DeclConstant.v
- COQC theories/QArith/QOrderedType.v
- COQC theories/ZArith/Znumtheory.v
- COQC theories/micromega/ZifyNat.v
- COQC theories/micromega/ZifyN.v
- COQC theories/QArith/Qminmax.v
- COQC theories/NArith/Ndec.v
- COQC theories/NArith/Ndist.v
- COQC theories/Logic/ClassicalChoice.v
- COQC theories/Logic/Description.v
- COQC theories/Logic/ClassicalEpsilon.v
- COQC theories/Logic/Epsilon.v
- COQC theories/Logic/Diaconescu.v
- COQC theories/Logic/IndefiniteDescription.v
- COQC theories/NArith/NArith.v
- COQC theories/MSets/MSetPositive.v
- COQC theories/micromega/RingMicromega.v
- COQC theories/Logic/ClassicalDescription.v
- COQC theories/Logic/SetoidChoice.v
- COQC theories/Structures/OrderedTypeEx.v
- COQC theories/Structures/DecidableTypeEx.v
- COQC theories/FSets/FSetPositive.v
- COQC theories/MSets/MSetAVL.v
- COQC theories/MSets/MSetRBT.v
- COQC theories/FSets/FSetFacts.v
- COQC theories/MSets/MSetFacts.v
- COQC theories/FSets/FMapFacts.v
- COQC theories/QArith/Qreduction.v
- COQC theories/micromega/ZCoeff.v
- COQC theories/FSets/FSetDecide.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/byte/coqProject_file.cmo -c -impl lib/coqProject_file.ml)
- File "lib/coqProject_file.ml", line 100, characters 35-46:
- 100 | let rec parse_string buf s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 105, characters 12-26:
- 105 | | exception Stream.Failure -> buffer buf
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 107, characters 32-43:
- 107 | and parse_string2 buf s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 112, characters 12-26:
- 112 | | exception Stream.Failure -> raise (Parsing_error "unterminated string")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 114, characters 33-44:
- 114 | and parse_skip_comment s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 117, characters 12-26:
- 117 | | exception Stream.Failure -> ()
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 119, characters 34-45:
- 119 | and parse_args buf accu s = match Stream.next s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 131, characters 12-26:
- 131 | | exception Stream.Failure -> accu
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/coqProject_file.ml", line 138, characters 31-48:
- 138 | let res = parse_args buf [] (Stream.of_channel c) in
- ^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/FSets/FSetCompat.v
- COQC theories/MSets/MSetDecide.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/byte/lStream.cmo -c -impl lib/lStream.ml)
- File "lib/lStream.ml", line 14, characters 12-20:
- 14 | strm : 'a Stream.t;
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 26, characters 4-15:
- 26 | Stream.from
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 35, characters 17-29:
- 35 | let count strm = Stream.count strm.strm
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 38, characters 16-28:
- 38 | strm.fun_loc (Stream.count strm.strm)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 57, characters 10-21:
- 57 | let a = Stream.peek strm.strm in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 58, characters 22-33:
- 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 58, characters 72-84:
- 58 | if Option.has_some (Stream.peek strm.strm) then strm.max_peek <- max (Stream.count strm.strm + 1) strm.max_peek;
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 62, characters 10-22:
- 62 | let l = Stream.npeek n strm.strm in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 63, characters 24-36:
- 63 | strm.max_peek <- max (Stream.count strm.strm + List.length l) strm.max_peek;
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 67, characters 13-25:
- 67 | let list = Stream.npeek (n + 1) strm.strm in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 70, characters 36-48:
- 70 | x :: _, 0 -> strm.max_peek <- Stream.count strm.strm + n + 1; x
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 72, characters 32-44:
- 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 72, characters 72-86:
- 72 | | [], p -> strm.max_peek <- Stream.count strm.strm + (n - p); raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 76, characters 16-27:
- 76 | let junk strm = Stream.junk strm.strm
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/lStream.ml", line 78, characters 16-27:
- 78 | let next strm = Stream.next strm.strm
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -intf-suffix .ml -no-alias-deps -o lib/.lib.objs/byte/util.cmo -c -impl lib/util.ml)
- File "lib/util.ml", line 126, characters 16-28:
- 126 | try List.nth (Stream.npeek (n+1) st) n
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/util.ml", line 127, characters 26-40:
- 127 | with Failure _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "lib/util.ml", line 130, characters 11-22:
- 130 | repeat n Stream.junk st
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Plexing.cmo -c -impl gramlib/plexing.ml)
- File "gramlib/plexing.ml", line 5, characters 41-49:
- 5 | type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/FSets/FSetList.v
- COQC theories/FSets/FSetWeakList.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -I lib/.lib.objs/byte -intf-suffix .ml -no-alias-deps -open Gramlib -o gramlib/.gramlib.objs/byte/gramlib__Grammar.cmo -c -impl gramlib/grammar.ml)
- File "gramlib/grammar.ml", line 20, characters 34-42:
- 20 | val make : ?loc:Loc.t -> char Stream.t -> t
- ^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1073, characters 15-29:
- 1073 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1082, characters 15-29:
- 1082 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1091, characters 27-41:
- 1091 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1091, characters 61-75:
- 1091 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1095, characters 13-27:
- 1095 | else raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1101, characters 6-20:
- 1101 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son))
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1101, characters 31-43:
- 1101 | Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1120, characters 4-18:
- 1120 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1127, characters 62-76:
- 1127 | skip_if_empty bp (fun (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1129, characters 11-25:
- 1129 | with Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1162, characters 52-66:
- 1162 | DeadEnd -> (fun (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1173, characters 53-67:
- 1173 | try Some (entry.estart alevn strm__) with Stream.Failure -> None
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1183, characters 31-45:
- 1183 | try p1 strm__ with Stream.Failure -> p2 strm__)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1193, characters 17-31:
- 1193 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1194, characters 26-38:
- 1194 | raise (Stream.Error (tree_failed entry a s son))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1204, characters 43-57:
- 1204 | match try Some (ps strm) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1207, characters 49-63:
- 1207 | (try Some (p1 bp a strm) with Stream.Failure -> None)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1210, characters 34-46:
- 1210 | | None -> raise (Stream.Error (tree_failed entry a s son))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1217, characters 4-18:
- 1217 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1245, characters 66-80:
- 1245 | (match (try Some (tematch (LStream.peek_nth n strm)) with Stream.Failure -> None) with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1247, characters 44-58:
- 1247 | (match try Some (p1 a strm) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1251, characters 42-56:
- 1251 | | DeadEnd -> fun last_a strm -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1257, characters 35-49:
- 1257 | try Some (ps strm) with Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1259, characters 87-101:
- 1259 | try Some (parser_of_tree entry nlevn alevn (top_tree entry tree) strm) with Stream.Failure -> None
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1262, characters 26-38:
- 1262 | | None -> raise (Stream.Error (tree_failed entry last_a (Stoken last_tok) tree))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1269, characters 20-34:
- 1269 | | None -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1277, characters 43-57:
- 1277 | match try Some (ps al strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1287, characters 40-54:
- 1287 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1291, characters 16-30:
- 1291 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1292, characters 25-37:
- 1292 | raise (Stream.Error (symb_failed entry v sep symb))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1298, characters 44-58:
- 1298 | match try Some (ps [] strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1305, characters 40-54:
- 1305 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1308, characters 44-58:
- 1308 | (try Some (ps al strm__) with Stream.Failure -> None)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1316, characters 44-58:
- 1316 | match try Some (ps [] strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1322, characters 43-57:
- 1322 | match try Some (ps al strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1333, characters 40-54:
- 1333 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1337, characters 16-30:
- 1337 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1340, characters 22-36:
- 1340 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1341, characters 31-43:
- 1341 | raise (Stream.Error (symb_failed entry v sep symb))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1355, characters 40-54:
- 1355 | match try Some (pt strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1358, characters 44-58:
- 1358 | (try Some (ps al strm__) with Stream.Failure -> None)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1364, characters 20-34:
- 1364 | Stream.Failure -> None
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1377, characters 41-55:
- 1377 | match try Some (ps strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1400, characters 20-34:
- 1400 | | None -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1434, characters 52-66:
- 1434 | [] -> (fun levn (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1470, characters 50-64:
- 1470 | match try Some (p2 strm__) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1491, characters 57-71:
- 1491 | [] -> (fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1510, characters 16-30:
- 1510 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1521, characters 37-51:
- 1521 | try p levn bp a strm__ with Stream.Failure -> a)
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1522, characters 63-77:
- 1522 | | Dparser p -> fun levn bp a (strm__ : _ LStream.t) -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1525, characters 9-21:
- 1525 | raise (Stream.Error ("entry [" ^ ename ^ "] is empty"))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1586, characters 6-20:
- 1586 | Stream.Failure ->
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1589, characters 6-18:
- 1589 | | Stream.Error _ as exc ->
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1588, characters 22-34:
- 1588 | Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename))
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1629, characters 51-65:
- 1629 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1642, characters 51-65:
- 1642 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1728, characters 55-69:
- 1728 | e.estart <- (fun _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "gramlib/grammar.ml", line 1729, characters 62-76:
- 1729 | e.econtinue <- (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/setoid_ring/Field_tac.v
- COQC theories/setoid_ring/Field.v
- COQC theories/FSets/FSetProperties.v
- COQC theories/MSets/MSetProperties.v
- COQC theories/QArith/Qfield.v
- COQC theories/QArith/Qring.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I engine/.engine.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I clib/.clib.objs/byte -I config/.config.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -intf-suffix .ml -no-alias-deps -o engine/.engine.objs/byte/evarutil.cmo -c -impl engine/evarutil.ml)
- File "engine/evarutil.ml", line 131, characters 10-18:
- 131 | let m = E.create () in
- ^^^^^^^^
- Alert old_ephemeron_api: E.create
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 132, characters 19-29:
- 132 | fun x y -> match E.get_key1 m, E.get_key2 m with
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.get_key1
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 132, characters 33-43:
- 132 | fun x y -> match E.get_key1 m, E.get_key2 m with
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.get_key2
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 133, characters 60-70:
- 133 | | Some x', Some y' when x == x' && y == y' -> Option.get (E.get_data m)
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.get_data
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 134, characters 26-36:
- 134 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.set_key1
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 134, characters 42-52:
- 134 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.set_key2
- This function won't be available in 5.0
- File "engine/evarutil.ml", line 134, characters 58-68:
- 134 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r
- ^^^^^^^^^^
- Alert old_ephemeron_api: E.set_data
- This function won't be available in 5.0
- COQC theories/QArith/QArith.v
- COQC theories/micromega/ZMicromega.v
- COQC theories/QArith/Qabs.v
- COQC theories/QArith/Qround.v
- COQC theories/micromega/QMicromega.v
- COQC theories/QArith/Qcanon.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/byte/numTok.cmo -c -impl interp/numTok.ml)
- File "interp/numTok.ml", line 124, characters 33-44:
- 124 | let rec number len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 125, characters 32-43:
- 125 | | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 126, characters 40-51:
- 126 | | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 129, characters 37-48:
- 129 | let rec hex_number len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 131, characters 9-20:
- 131 | Stream.junk s; hex_number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 133, characters 9-20:
- 133 | Stream.junk s; hex_number (store len c) s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 137, characters 12-24:
- 137 | match Stream.npeek 3 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 139, characters 9-20:
- 139 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 139, characters 24-35:
- 139 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 139, characters 39-50:
- 139 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 144, characters 17-29:
- 144 | match hex, Stream.npeek 2 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 146, characters 9-20:
- 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 146, characters 24-35:
- 146 | Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 148, characters 9-20:
- 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 148, characters 24-35:
- 148 | Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 151, characters 17-29:
- 151 | match hex, Stream.npeek 2 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 154, characters 9-20:
- 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 154, characters 24-35:
- 154 | Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 157, characters 21-33:
- 157 | begin match Stream.npeek 3 s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 159, characters 12-23:
- 159 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 159, characters 27-38:
- 159 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 159, characters 42-53:
- 159 | Stream.junk s; Stream.junk s; Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 174, characters 17-33:
- 174 | let strm = Stream.of_string (s ^ " ") in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 176, characters 9-21:
- 176 | if Stream.count strm >= String.length s then Some n else None
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 260, characters 17-33:
- 260 | let strm = Stream.of_string (s ^ " ") in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 262, characters 18-29:
- 262 | | '-' -> (Stream.junk strm; SMinus)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 263, characters 18-29:
- 263 | | '+' -> (Stream.junk strm; SPlus)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "interp/numTok.ml", line 266, characters 9-21:
- 266 | if Stream.count strm >= String.length s then Some (sign,n) else None
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/byte/constrexpr_ops.cmo -c -impl interp/constrexpr_ops.ml)
- File "interp/constrexpr_ops.ml", line 569, characters 24-36:
- 569 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/byte/tok.cmo -c -impl parsing/tok.ml)
- File "parsing/tok.ml", line 124, characters 21-35:
- 124 | let err () = raise Stream.Failure in
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/byte/pcoq.cmo -c -impl parsing/pcoq.ml)
- File "parsing/pcoq.ml", line 22, characters 21-35:
- 22 | let err () = raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/pcoq.ml", line 199, characters 13-29:
- 199 | let strm = Stream.of_string x in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/micromega/Lqa.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o parsing/.parsing.objs/byte/cLexer.cmo -c -impl parsing/cLexer.ml)
- File "parsing/cLexer.ml", line 162, characters 11-23:
- 162 | let bp = Stream.count cs in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 163, characters 2-13:
- 163 | Stream.junk cs; (* consume the char to avoid read it and fail again *)
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 175, characters 28-39:
- 175 | let njunk n = Util.repeat n Stream.junk
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 188, characters 12-24:
- 188 | match Stream.npeek 2 cs with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 194, characters 12-24:
- 194 | match Stream.npeek 3 cs with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 201, characters 17-29:
- 201 | else match Stream.npeek 4 cs with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 213, characters 8-19:
- 213 | match Stream.peek cs with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 225, characters 30-41:
- 225 | let rec loop_symb s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 227, characters 8-19:
- 227 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 232, characters 23-34:
- 232 | | AsciiChar -> Stream.junk s; loop_symb s
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 235, characters 13-29:
- 235 | loop_symb (Stream.of_string str)
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 238, characters 35-46:
- 238 | let rec loop_id intail s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 240, characters 8-19:
- 240 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 243, characters 8-19:
- 243 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 254, characters 17-33:
- 254 | loop_id false (Stream.of_string str)
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 296, characters 39-50:
- 296 | if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 308, characters 37-48:
- 308 | let rec ident_tail loc len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 310, characters 6-17:
- 310 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 318, characters 62-74:
- 318 | let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 332, characters 48-59:
- 332 | let rec string loc ~comm_level bp len s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 334, characters 6-17:
- 334 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 336, characters 14-25:
- 336 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 337, characters 22-33:
- 337 | Some '"' -> Stream.junk s; true
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 342, characters 6-17:
- 342 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 343, characters 22-33:
- 343 | (fun s -> match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 345, characters 8-19:
- 345 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 353, characters 6-17:
- 353 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 354, characters 22-33:
- 354 | (fun s -> match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 356, characters 12-23:
- 356 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 367, characters 4-15:
- 367 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 368, characters 13-25:
- 368 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 378, characters 6-17:
- 378 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 381, characters 14-26:
- 381 | let _ = Stream.empty s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 382, characters 15-27:
- 382 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 436, characters 12-24:
- 436 | let bp2 = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 437, characters 8-19:
- 437 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 439, characters 6-17:
- 439 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 442, characters 16-27:
- 442 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 444, characters 14-25:
- 444 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 447, characters 13-27:
- 447 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 447, characters 38-50:
- 447 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 451, characters 6-17:
- 451 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 453, characters 14-25:
- 453 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 454, characters 22-33:
- 454 | Some ')' -> Stream.junk s; push_string "*)"; loc
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 456, characters 11-25:
- 456 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 456, characters 36-48:
- 456 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 459, characters 6-17:
- 459 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 464, characters 20-32:
- 464 | match try Some (Stream.empty s) with Stream.Failure -> None with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 464, characters 41-55:
- 464 | match try Some (Stream.empty s) with Stream.Failure -> None with
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 466, characters 15-27:
- 466 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 470, characters 16-27:
- 470 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 472, characters 14-25:
- 472 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 473, characters 23-35:
- 473 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 476, characters 14-25:
- 476 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 478, characters 23-37:
- 478 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 485, characters 54-66:
- 485 | try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 504, characters 36-48:
- 504 | match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 518, characters 8-19:
- 518 | match Stream.peek cs with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 529, characters 16-30:
- 529 | | exception Stream.Failure -> n, List.make n b, List.make n e
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 532, characters 24-38:
- 532 | if len = 0 then raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 541, characters 17-31:
- 541 | | _ -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 546, characters 14-25:
- 546 | let c = Stream.next s in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 549, characters 10-24:
- 549 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 549, characters 35-47:
- 549 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 551, characters 40-52:
- 551 | get_buff len, set_loc_pos loc bp (Stream.count s)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 559, characters 43-54:
- 559 | let commit1 c = Buffer.add_char b c; Stream.junk s in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 562, characters 14-26:
- 562 | match Stream.npeek lenmarker s with
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 571, characters 48-60:
- 571 | let loc = bump_loc_line_last loc (Stream.count s) in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 575, characters 63-77:
- 575 | if not dot_gobbling && blank_or_eof s then raise Stream.Failure;
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 580, characters 22-36:
- 580 | | [] -> raise Stream.Failure
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 583, characters 45-57:
- 583 | Buffer.contents b, set_loc_pos loc bp (Stream.count s)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 590, characters 15-27:
- 590 | let l' = Stream.npeek (i + 1) s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 600, characters 6-17:
- 600 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 609, characters 15-27:
- 609 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 617, characters 10-21:
- 617 | match Stream.peek cs with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 618, characters 30-41:
- 618 | | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 619, characters 57-69:
- 619 | | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs)
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 626, characters 11-23:
- 626 | let ep = Stream.count cs in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 647, characters 50-61:
- 647 | let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 649, characters 6-17:
- 649 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 652, characters 10-24:
- 652 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 652, characters 35-47:
- 652 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 657, characters 17-29:
- 657 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 666, characters 21-33:
- 666 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 674, characters 8-19:
- 674 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 686, characters 11-23:
- 686 | let bp = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 687, characters 8-19:
- 687 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 689, characters 6-17:
- 689 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 690, characters 15-27:
- 690 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 693, characters 6-17:
- 693 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 696, characters 6-17:
- 696 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 699, characters 10-24:
- 699 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 699, characters 35-47:
- 699 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 707, characters 21-33:
- 707 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 715, characters 6-17:
- 715 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 722, characters 6-17:
- 722 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 723, characters 15-27:
- 723 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 727, characters 6-17:
- 727 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 730, characters 10-24:
- 730 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 730, characters 35-47:
- 730 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 736, characters 17-29:
- 736 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 740, characters 15-27:
- 740 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 744, characters 6-17:
- 744 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 747, characters 10-24:
- 747 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 747, characters 35-47:
- 747 | Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 749, characters 15-27:
- 749 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 753, characters 6-17:
- 753 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 755, characters 14-25:
- 755 | match Stream.peek s with
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 757, characters 12-23:
- 757 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 758, characters 21-33:
- 758 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 761, characters 12-23:
- 761 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 766, characters 11-25:
- 766 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 766, characters 36-48:
- 766 | with Stream.Failure -> raise (Stream.Error "")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 769, characters 6-17:
- 769 | Stream.junk s;
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 770, characters 15-27:
- 770 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 784, characters 23-35:
- 784 | let ep = Stream.count s in
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "parsing/cLexer.ml", line 787, characters 53-64:
- 787 | let t = process_chars ~diff_mode loc bp (Stream.next s) s in
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I printing/.printing.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I proofs/.proofs.objs/byte -intf-suffix .ml -no-alias-deps -o printing/.printing.objs/byte/proof_diffs.cmo -c -impl printing/proof_diffs.ml)
- File "printing/proof_diffs.ml", line 102, characters 15-31:
- 102 | let istr = Stream.of_string s in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/Reals/Abstract/ConstructiveReals.v
- COQC theories/QArith/Qcabs.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I pretyping/.pretyping.objs/byte -intf-suffix .ml -no-alias-deps -o interp/.interp.objs/byte/constrintern.cmo -c -impl interp/constrintern.ml)
- File "interp/constrintern.ml", line 586, characters 22-34:
- 586 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/himsg.cmo -c -impl vernac/himsg.ml)
- File "vernac/himsg.ml", line 1413, characters 4-16:
- 1413 | | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/FSets/FSetEqProperties.v
- COQC theories/FSets/FSetToFiniteSet.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/comInductive.cmo -c -impl vernac/comInductive.ml)
- File "vernac/comInductive.ml", line 365, characters 20-32:
- 365 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/proof_using.cmo -c -impl vernac/proof_using.ml)
- File "vernac/proof_using.ml", line 178, characters 94-110:
- 178 | let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/micromega/Lia.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/record.cmo -c -impl vernac/record.ml)
- File "vernac/record.ml", line 120, characters 20-32:
- 120 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")
- ^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I tactics/.tactics.objs/byte -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/byte/vernacinterp.cmo -c -impl vernac/vernacinterp.ml)
- File "vernac/vernacinterp.ml", line 189, characters 64-81:
- 189 | Pcoq.Parsable.make ~loc:(Loc.(initial (InFile longfname))) (Stream.of_channel in_chan) in
- ^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/micromega/ZArith_hints.v
- COQC theories/ZArith/Zpow_facts.v
- COQC theories/ZArith/Zgcd_alt.v
- COQC theories/ZArith/Zquot.v
- COQC theories/ZArith/Zwf.v
- COQC theories/Arith/Cantor.v
- COQC theories/Compat/Coq813.v
- COQC theories/Sorting/PermutSetoid.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/byte/vernac.cmo -c -impl toplevel/vernac.ml)
- File "toplevel/vernac.ml", line 92, characters 7-24:
- 92 | (Stream.of_channel in_chan) in
- ^^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/MSets/MSetToFiniteSet.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I topbin/.coqtop_byte_bin.eobjs/byte -I /home/opam/.opam/default/lib/ocaml/compiler-libs -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I toplevel/.toplevel.objs/byte -I vernac/.vernac.objs/byte -no-alias-deps -o topbin/.coqtop_byte_bin.eobjs/byte/dune__exe__Coqtop_byte_bin.cmo -c -impl topbin/coqtop_byte_bin.ml)
- File "topbin/coqtop_byte_bin.ml", line 22, characters 29-52:
- 22 | begin match Hashtbl.find Toploop.directive_table "rectypes" with
- ^^^^^^^^^^^^^^^^^^^^^^^
- Alert deprecated: Toploop.directive_table
- File "topbin/coqtop_byte_bin.ml", line 31, characters 42-59:
- 31 | { load_obj = (fun f -> if not (Topdirs.load_file ppf f)
- ^^^^^^^^^^^^^^^^^
- Alert deprecated: Topdirs.load_file
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -intf-suffix .ml -no-alias-deps -o toplevel/.toplevel.objs/byte/coqloop.cmo -c -impl toplevel/coqloop.ml)
- File "toplevel/coqloop.ml", line 79, characters 37-48:
- 79 | ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf));
- ^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "toplevel/coqloop.ml", line 233, characters 33-47:
- 233 | tokens = Pcoq.Parsable.make (Stream.of_list []);
- ^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/Compat/Coq812.v
- COQC theories/ZArith/ZArith.v
- COQC theories/MSets/MSetEqProperties.v
- COQC theories/Compat/Coq811.v
- COQC theories/micromega/ZifyBool.v
- COQC theories/Reals/Cauchy/PosExtra.v
- COQC theories/Reals/Cauchy/ConstructiveExtra.v
- COQC theories/micromega/ZifyComparison.v
- COQC theories/Classes/DecidableClass.v
- COQC theories/ZArith/Zdigits.v
- COQC theories/FSets/FSetAVL.v
- COQC theories/FSets/FMapPositive.v
- COQC theories/FSets/FMapAVL.v
- COQC theories/Floats/SpecFloat.v
- COQC theories/Numbers/HexadecimalFacts.v
- COQC theories/Numbers/DecimalFacts.v
- COQC theories/Numbers/Cyclic/Int31/Int31.v
- COQC theories/extraction/ExtrHaskellZNum.v
- COQC theories/extraction/ExtrOcamlZBigInt.v
- COQC theories/extraction/ExtrOcamlZInt.v
- COQC theories/extraction/ExtrOcamlIntConv.v
- COQC theories/extraction/ExtrOcamlBigIntConv.v
- COQC theories/Numbers/Cyclic/Int63/Uint63.v
- COQC theories/QArith/Qpower.v
- COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
- COQC theories/Sorting/PermutEq.v
- COQC theories/Sorting/Heap.v
- COQC theories/btauto/Algebra.v
- COQC theories/extraction/ExtrHaskellZInt.v
- COQC theories/extraction/ExtrHaskellZInteger.v
- COQC theories/FSets/FSets.v
- COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v
- COQC theories/Numbers/Cyclic/Int31/Cyclic31.v
- COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v
- COQC theories/MSets/MSets.v
- COQC theories/Reals/Abstract/ConstructiveAbs.v
- COQC theories/Reals/Cauchy/QExtra.v
- COQC theories/FSets/FMaps.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -open Gramlib -g -bin-annot -I plugins/ssr/.ssreflect_plugin.objs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I plugins/ltac/.ltac_plugin.objs/byte -I plugins/ssrmatching/.ssrmatching_plugin.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I vernac/.vernac.objs/byte -intf-suffix .ml -no-alias-deps -open Ssreflect_plugin -o plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrparser.cmo -c -impl plugins/ssr/ssrparser.ml)
- File "plugins/ssr/ssrparser.mlg", line 263, characters 28-42:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 265, characters 22-36:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 272, characters 24-38:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 274, characters 22-36:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 276, characters 19-33:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 283, characters 24-38:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 285, characters 22-36:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 286, characters 15-29:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 294, characters 31-45:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 297, characters 20-34:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 844, characters 33-47:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 853, characters 9-23:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 858, characters 12-26:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 859, characters 55-69:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 860, characters 45-59:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 2411, characters 37-51:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "plugins/ssr/ssrparser.mlg", line 2415, characters 17-31:
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/btauto/Reflect.v
- COQC theories/Numbers/DecimalPos.v
- COQC theories/Numbers/DecimalNat.v
- COQC theories/Reals/Cauchy/ConstructiveCauchyReals.v
- COQC theories/btauto/Btauto.v
- COQC theories/Reals/Abstract/ConstructiveLimits.v
- COQC theories/Numbers/DecimalN.v
- COQC theories/Numbers/DecimalZ.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I ide/coqide/.idetop.eobjs/byte -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I config/.config.objs/byte -I engine/.engine.objs/byte -I gramlib/.gramlib.objs/byte -I ide/coqide/protocol/.protocol.objs/byte -I interp/.interp.objs/byte -I kernel/.kernel.objs/byte -I kernel/byterun/.coqrun.objs/byte -I lib/.lib.objs/byte -I library/.library.objs/byte -I parsing/.parsing.objs/byte -I pretyping/.pretyping.objs/byte -I printing/.printing.objs/byte -I proofs/.proofs.objs/byte -I stm/.stm.objs/byte -I sysinit/.sysinit.objs/byte -I tactics/.tactics.objs/byte -I toplevel/.toplevel.objs/byte -I vernac/.vernac.objs/byte -no-alias-deps -o ide/coqide/.idetop.eobjs/byte/dune__exe__Idetop.cmo -c -impl ide/coqide/idetop.ml)
- File "ide/coqide/idetop.ml", line 81, characters 31-47:
- 81 | let pa = Pcoq.Parsable.make (Stream.of_string s) in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "ide/coqide/idetop.ml", line 108, characters 31-47:
- 108 | let pa = Pcoq.Parsable.make (Stream.of_string s) in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "ide/coqide/idetop.ml", line 114, characters 31-47:
- 114 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/Numbers/DecimalQ.v
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I ide/coqide/.idetop.eobjs/byte -I ide/coqide/.idetop.eobjs/native -I /home/opam/.opam/default/lib/ocaml/threads -I /home/opam/.opam/default/lib/zarith -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I ide/coqide/protocol/.protocol.objs/byte -I ide/coqide/protocol/.protocol.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I stm/.stm.objs/byte -I stm/.stm.objs/native -I sysinit/.sysinit.objs/byte -I sysinit/.sysinit.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -intf-suffix .ml -no-alias-deps -o ide/coqide/.idetop.eobjs/native/dune__exe__Idetop.cmx -c -impl ide/coqide/idetop.ml)
- File "ide/coqide/idetop.ml", line 81, characters 31-47:
- 81 | let pa = Pcoq.Parsable.make (Stream.of_string s) in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "ide/coqide/idetop.ml", line 108, characters 31-47:
- 108 | let pa = Pcoq.Parsable.make (Stream.of_string s) in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- File "ide/coqide/idetop.ml", line 114, characters 31-47:
- 114 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
- ^^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Stream
- Use the camlp-streams library instead.
- COQC theories/Numbers/HexadecimalPos.v
- COQC theories/Numbers/HexadecimalNat.v
- COQC theories/Numbers/Cyclic/Int31/Ring31.v
- COQC theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
- COQC theories/Numbers/Cyclic/Int63/Int63.v
- COQC theories/micromega/ZifyUint63.v
- COQC theories/Floats/FloatOps.v
- COQC theories/Array/PArray.v
- COQC theories/Numbers/Cyclic/Int63/Cyclic63.v
- COQC theories/Numbers/Cyclic/Int63/Sint63.v
- COQC theories/extraction/ExtrOCamlPArray.v
- COQC theories/Floats/FloatAxioms.v
- COQC theories/micromega/ZifyInt63.v
- COQC theories/Reals/Abstract/ConstructiveLUB.v
- COQC theories/Reals/Abstract/ConstructiveRealsMorphisms.v
- COQC theories/Numbers/Cyclic/Int63/Ring63.v
- COQC theories/micromega/ZifySint63.v
- COQC theories/extraction/ExtrOCamlInt63.v
- COQC theories/Reals/Abstract/ConstructiveSum.v
- COQC theories/Reals/Abstract/ConstructiveMinMax.v
- COQC theories/setoid_ring/Ncring_initial.v
- COQC theories/Reals/Abstract/ConstructivePower.v
- COQC theories/FSets/FMapFullAVL.v
- COQC theories/Numbers/HexadecimalN.v
- COQC theories/Numbers/HexadecimalZ.v
- COQC theories/Numbers/HexadecimalQ.v
- COQC theories/setoid_ring/Ncring_tac.v
- COQC theories/Reals/Cauchy/ConstructiveCauchyAbs.v
- COQC theories/setoid_ring/Cring.v
- COQC theories/setoid_ring/Integral_domain.v
- COQC theories/setoid_ring/Rings_Z.v
- COQC theories/setoid_ring/Rings_Q.v
- COQC theories/nsatz/NsatzTactic.v
- COQC theories/Reals/Cauchy/ConstructiveRcomplete.v
- COQC theories/Reals/ClassicalDedekindReals.v
- COQC theories/Reals/Rdefinitions.v
- COQC theories/Reals/Raxioms.v
- COQC theories/Reals/Rpow_def.v
- COQC theories/Numbers/DecimalR.v
- COQC theories/Numbers/HexadecimalR.v
- COQC theories/setoid_ring/RealField.v
- COQC theories/Reals/ClassicalConstructiveReals.v
- COQC theories/Reals/RIneq.v
- COQC theories/Reals/DiscrR.v
- COQC theories/Reals/R_Ifp.v
- COQC theories/Reals/SplitRmult.v
- COQC theories/QArith/Qreals.v
- COQC theories/Reals/Rlogic.v
- COQC theories/Reals/Rbase.v
- COQC theories/Reals/Rbasic_fun.v
- COQC theories/Reals/ROrderedType.v
- COQC theories/Reals/R_sqr.v
- COQC theories/Reals/SplitAbsolu.v
- COQC theories/Reals/ArithProp.v
- COQC theories/Reals/Rminmax.v
- COQC theories/Reals/Rfunctions.v
- COQC theories/micromega/RMicromega.v
- COQC theories/Reals/Rregisternames.v
- COQC theories/Reals/Rseries.v
- COQC theories/Reals/RList.v
- COQC theories/Reals/Runcountable.v
- COQC theories/micromega/Lra.v
- COQC theories/micromega/MExtraction.v
- COQC theories/Reals/SeqProp.v
- COQC theories/micromega/Fourier_util.v
- COQC theories/micromega/Psatz.v
- COQC theories/Reals/Rlimit.v
- COQC theories/Reals/Rcomplete.v
- COQC theories/Floats/FloatLemmas.v
- COQC theories/micromega/Fourier.v
- COQC theories/Reals/Rderiv.v
- COQC theories/Reals/PartSum.v
- COQC theories/Reals/Ranalysis1.v
- COQC theories/Floats/Floats.v
- COQC theories/Reals/AltSeries.v
- COQC theories/Reals/Binomial.v
- COQC theories/Reals/Rsigma.v
- COQC theories/Reals/Cauchy_prod.v
- COQC theories/Reals/Alembert.v
- COQC theories/extraction/ExtrOCamlFloats.v
- COQC theories/Reals/Rprod.v
- COQC theories/Reals/Rtopology.v
- COQC theories/Reals/Ranalysis2.v
- COQC theories/Reals/SeqSeries.v
- COQC theories/Reals/Ranalysis3.v
- COQC theories/Reals/Rtrigo_fun.v
- COQC theories/Reals/Rsqrt_def.v
- COQC theories/Reals/MVT.v
- COQC theories/Reals/Rtrigo_def.v
- COQC theories/Reals/PSeries_reg.v
- COQC theories/Reals/R_sqrt.v
- COQC theories/Reals/Rtrigo_alt.v
- COQC theories/Reals/Cos_rel.v
- COQC theories/Reals/Sqrt_reg.v
- COQC theories/Reals/Cos_plus.v
- COQC theories/Reals/Rtrigo1.v
- COQC theories/Reals/Rgeom.v
- COQC theories/Reals/Exp_prop.v
- COQC theories/Reals/Rtrigo_reg.v
- COQC theories/Reals/Rtrigo_calc.v
- COQC theories/Reals/Ranalysis4.v
- COQC theories/Reals/Rpower.v
- COQC theories/Reals/Ranalysis_reg.v
- COQC theories/Reals/Rtrigo_facts.v
- COQC theories/Reals/RiemannInt_SF.v
- COQC theories/Reals/RiemannInt.v
- COQC theories/Reals/Ranalysis5.v
- COQC theories/Reals/Ratan.v
- COQC theories/Reals/Machin.v
- COQC theories/Reals/Rtrigo.v
- COQC theories/Reals/Ranalysis.v
- COQC theories/Reals/NewtonInt.v
- COQC theories/Reals/Integration.v
- COQC theories/Reals/Reals.v
- COQC theories/setoid_ring/Rings_R.v
- COQC theories/nsatz/Nsatz.v
- make[1]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/coq.8.14.0'
-> compiled coq.8.14.0
[coq: make install]
+ /usr/bin/make "COQ_USE_DUNE=" "install" (CWD=/home/opam/.opam/default/.opam-switch/build/coq.8.14.0)
- /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build install
- make[1]: Entering directory '/home/opam/.opam/default/.opam-switch/build/coq.8.14.0'
- DUNE sources
- dune install --display=quiet --release --mandir=""/home/opam/.opam/default/man"" --prefix="/home/opam/.opam/default" coq-core
- dune install --display=quiet --release --mandir=""/home/opam/.opam/default/man"" --prefix="/home/opam/.opam/default" coqide-server
- INSTALL VOFILES
- make[1]: Leaving directory '/home/opam/.opam/default/.opam-switch/build/coq.8.14.0'
-> installed coq.8.14.0
[WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config
=== STDERR ===
2026-06-16 12:14.49: OK: build coq.8.14.0 (runc: 533.2s, disk: 211KB)
2026-06-16 12:14.49: Job succeeded