===> Building for coq-8.15.2nb19 /opt/pkg/bin/gmake --warn-undefined-variable --no-builtin-rules -f Makefile.build world gmake[1]: Entering directory '/Users/pbulk/build/lang/coq/work/coq-8.15.2' MKDIR BUILD_OUT DUNE _build/default/tools/flock/coq_flock.exe Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqdep Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 82, characters 35-46: 82 | 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 90, characters 12-26: 90 | | exception Stream.Failure -> buffer buf ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 92, characters 32-43: 92 | 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 97, characters 12-26: 97 | | 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 99, characters 33-44: 99 | 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 102, characters 12-26: 102 | | exception Stream.Failure -> () ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 104, characters 34-45: 104 | 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 116, characters 12-26: 116 | | exception Stream.Failure -> accu ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 123, characters 31-48: 123 | let res = parse_args buf [] (Stream.of_channel c) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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. DUNE sources Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQDEP VFILES DUNE sources Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqc Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 31, characters 34-42: 31 | val make : ?loc:Loc.t -> char Stream.t -> t ^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 21, characters 34-42: 21 | 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 1093, characters 15-29: 1093 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1102, characters 15-29: 1102 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1111, characters 27-41: 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1111, characters 61-75: 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1115, characters 13-27: 1115 | else raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1121, characters 6-20: 1121 | 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 1121, characters 31-43: 1121 | 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 1140, characters 4-18: 1140 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1147, characters 62-76: 1147 | 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 1149, characters 11-25: 1149 | with Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1182, characters 52-66: 1182 | DeadEnd -> (fun (strm__ : _ LStream.t) -> raise Stream.Failure) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1193, characters 53-67: 1193 | 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 1203, characters 31-45: 1203 | try p1 strm__ with Stream.Failure -> p2 strm__) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1213, characters 17-31: 1213 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1214, characters 26-38: 1214 | 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 1224, characters 43-57: 1224 | 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 1227, characters 49-63: 1227 | (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 1230, characters 34-46: 1230 | | 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 1237, characters 4-18: 1237 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1265, characters 66-80: 1265 | (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 1267, characters 44-58: 1267 | (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 1271, characters 42-56: 1271 | | DeadEnd -> fun last_a strm -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1277, characters 35-49: 1277 | try Some (ps strm) with Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1279, characters 87-101: 1279 | 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 1282, characters 26-38: 1282 | | 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 1289, characters 20-34: 1289 | | None -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1297, characters 43-57: 1297 | 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 1307, characters 40-54: 1307 | 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 1311, characters 16-30: 1311 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1312, characters 25-37: 1312 | 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 1318, characters 44-58: 1318 | 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 1325, characters 40-54: 1325 | 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 1328, characters 44-58: 1328 | (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 1336, characters 44-58: 1336 | 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 1342, characters 43-57: 1342 | 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 1353, characters 40-54: 1353 | 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 1357, characters 16-30: 1357 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1360, characters 22-36: 1360 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1361, characters 31-43: 1361 | 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 1375, characters 40-54: 1375 | 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 1378, characters 44-58: 1378 | (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 1384, characters 20-34: 1384 | Stream.Failure -> None ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1397, characters 41-55: 1397 | 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 1421, characters 20-34: 1421 | | None -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1466, characters 52-66: 1466 | [] -> (fun levn (strm__ : _ LStream.t) -> raise Stream.Failure) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1502, characters 50-64: 1502 | 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 1523, characters 57-71: 1523 | [] -> (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 1542, characters 16-30: 1542 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1553, characters 37-51: 1553 | 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 1554, characters 63-77: 1554 | | 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 1557, characters 9-21: 1557 | raise (Stream.Error ("entry [" ^ ename ^ "] is empty")) ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1622, characters 6-20: 1622 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1625, characters 6-18: 1625 | | Stream.Error _ as exc -> ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1624, characters 22-34: 1624 | 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 1662, characters 51-65: 1662 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1675, characters 51-65: 1675 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1763, characters 55-69: 1763 | 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 1764, characters 62-76: 1764 | 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 && /Users/pbulk/build/lang/coq/work/.cwrapper/bin/clang -O2 -fno-strict-aliasing -fwrapv -D_REENTRANT -pipe -Os -I/opt/pkg/include/ncurses -D_FILE_OFFSET_BITS=64 -I/opt/pkg/include/ncurses -Wall -Wno-unused -g -O2 -g -I /opt/pkg/lib/ocaml -o coq_memory.o -c coq_memory.c) coq_memory.c:114:34: warning: "scan_roots_hook" is deprecated: use "caml_scan_roots_hook" instead [-W#pragma-messages] coq_prev_scan_roots_hook = scan_roots_hook; ^ /opt/pkg/lib/ocaml/caml/compatibility.h:259:25: note: expanded from macro 'scan_roots_hook' #define scan_roots_hook CAML_DEPRECATED("scan_roots_hook", "caml_scan_roots_hook") caml_scan_roots_hook ^ /opt/pkg/lib/ocaml/caml/misc.h:58:3: note: expanded from macro 'CAML_DEPRECATED' CAML_PREPROWARNING(name1 is deprecated: use name2 instead) ^ /opt/pkg/lib/ocaml/caml/misc.h:56:31: note: expanded from macro 'CAML_PREPROWARNING' #define CAML_PREPROWARNING(x) _Pragma(CAML_MAKEWARNING2(x)) ^ <scratch space>:43:6: note: expanded from here GCC warning "\"scan_roots_hook\" is deprecated: use \"caml_scan_roots_hook\" instead" ^ coq_memory.c:115:5: warning: "scan_roots_hook" is deprecated: use "caml_scan_roots_hook" instead [-W#pragma-messages] scan_roots_hook = coq_scan_roots; ^ /opt/pkg/lib/ocaml/caml/compatibility.h:259:25: note: expanded from macro 'scan_roots_hook' #define scan_roots_hook CAML_DEPRECATED("scan_roots_hook", "caml_scan_roots_hook") caml_scan_roots_hook ^ /opt/pkg/lib/ocaml/caml/misc.h:58:3: note: expanded from macro 'CAML_DEPRECATED' CAML_PREPROWARNING(name1 is deprecated: use name2 instead) ^ /opt/pkg/lib/ocaml/caml/misc.h:56:31: note: expanded from macro 'CAML_PREPROWARNING' #define CAML_PREPROWARNING(x) _Pragma(CAML_MAKEWARNING2(x)) ^ <scratch space>:47:6: note: expanded from here GCC warning "\"scan_roots_hook\" is deprecated: use \"caml_scan_roots_hook\" instead" ^ 2 warnings generated. (cd _build/default/kernel/byterun && /Users/pbulk/build/lang/coq/work/.cwrapper/bin/clang -O2 -fno-strict-aliasing -fwrapv -D_REENTRANT -pipe -Os -I/opt/pkg/include/ncurses -D_FILE_OFFSET_BITS=64 -I/opt/pkg/include/ncurses -Wall -Wno-unused -g -O2 -g -I /opt/pkg/lib/ocaml -o coq_fix_code.o -c coq_fix_code.c) coq_fix_code.c:36:23: warning: "raise_out_of_memory" is deprecated: use "caml_raise_out_of_memory" instead [-W#pragma-messages] if (result == NULL) raise_out_of_memory (); ^ /opt/pkg/lib/ocaml/caml/compatibility.h:114:29: note: expanded from macro 'raise_out_of_memory' #define raise_out_of_memory CAML_DEPRECATED("raise_out_of_memory", "caml_raise_out_of_memory") caml_raise_out_of_memory ^ /opt/pkg/lib/ocaml/caml/misc.h:58:3: note: expanded from macro 'CAML_DEPRECATED' CAML_PREPROWARNING(name1 is deprecated: use name2 instead) ^ /opt/pkg/lib/ocaml/caml/misc.h:56:31: note: expanded from macro 'CAML_PREPROWARNING' #define CAML_PREPROWARNING(x) _Pragma(CAML_MAKEWARNING2(x)) ^ <scratch space>:438:6: note: expanded from here GCC warning "\"raise_out_of_memory\" is deprecated: use \"caml_raise_out_of_memory\" instead" ^ 1 warning generated. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I engine/.engine.objs/byte -I engine/.engine.objs/native -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 124, characters 10-18: 124 | 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 125, characters 19-29: 125 | 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 125, characters 33-43: 125 | 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 126, characters 60-70: 126 | | 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 127, characters 26-36: 127 | | _ -> 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 127, characters 42-52: 127 | | _ -> 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 127, characters 58-68: 127 | | _ -> 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 575, characters 24-36: 575 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 585, characters 22-34: 585 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 144, characters 21-35: 144 | let err () = raise Stream.Failure in ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 435, characters 12-24: 435 | let bp2 = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 436, characters 8-19: 436 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 438, characters 6-17: 438 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 441, characters 16-27: 441 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 443, characters 14-25: 443 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 446, characters 13-27: 446 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 446, characters 38-50: 446 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 450, characters 6-17: 450 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 452, characters 14-25: 452 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 453, characters 22-33: 453 | Some ')' -> Stream.junk s; push_string "*)"; loc ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 455, characters 11-25: 455 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 455, characters 36-48: 455 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 458, characters 6-17: 458 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 463, characters 20-32: 463 | 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 463, characters 41-55: 463 | 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 465, characters 15-27: 465 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 469, characters 16-27: 469 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 471, characters 14-25: 471 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 472, characters 23-35: 472 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 475, characters 14-25: 475 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 477, characters 23-37: 477 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 484, characters 54-66: 484 | 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 503, characters 36-48: 503 | 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 517, characters 8-19: 517 | match Stream.peek cs with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 528, characters 16-30: 528 | | 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 531, characters 24-38: 531 | if len = 0 then raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 540, characters 17-31: 540 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 545, characters 14-25: 545 | let c = Stream.next s in ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 548, characters 10-24: 548 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 548, characters 35-47: 548 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 550, characters 40-52: 550 | 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 558, characters 43-54: 558 | 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 561, characters 14-26: 561 | match Stream.npeek lenmarker s with ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 570, characters 48-60: 570 | 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 574, characters 63-77: 574 | 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 579, characters 22-36: 579 | | [] -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 582, characters 45-57: 582 | 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 589, characters 15-27: 589 | let l' = Stream.npeek (i + 1) s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 599, characters 6-17: 599 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 608, characters 15-27: 608 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 616, characters 10-21: 616 | match Stream.peek cs with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 617, characters 30-41: 617 | | 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 618, characters 57-69: 618 | | _ -> 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 625, characters 11-23: 625 | let ep = Stream.count cs in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 646, characters 50-61: 646 | 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 648, characters 6-17: 648 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 651, characters 10-24: 651 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 651, characters 35-47: 651 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 656, characters 17-29: 656 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 665, characters 21-33: 665 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 673, characters 8-19: 673 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 685, characters 11-23: 685 | let bp = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 686, characters 8-19: 686 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 688, characters 6-17: 688 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 689, characters 15-27: 689 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 692, characters 6-17: 692 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 695, characters 6-17: 695 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 698, characters 10-24: 698 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 698, characters 35-47: 698 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 706, characters 21-33: 706 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 714, characters 6-17: 714 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 721, characters 6-17: 721 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 722, characters 15-27: 722 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 726, characters 6-17: 726 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 729, characters 10-24: 729 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 729, characters 35-47: 729 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 735, characters 17-29: 735 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 742, characters 17-29: 742 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 745, characters 6-17: 745 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 748, characters 10-24: 748 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 748, characters 35-47: 748 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 750, characters 15-27: 750 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 754, characters 6-17: 754 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 756, characters 14-25: 756 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 758, characters 12-23: 758 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 759, characters 21-33: 759 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 762, characters 12-23: 762 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 767, characters 11-25: 767 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 767, characters 36-48: 767 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 770, characters 6-17: 770 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 771, characters 15-27: 771 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 785, characters 23-35: 785 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 788, characters 53-64: 788 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I printing/.printing.objs/byte -I printing/.printing.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 1428, characters 4-16: 1428 | | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 210, characters 94-110: 210 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 113, characters 20-32: 113 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 177, characters 9-26: 177 | (Stream.of_channel in_chan) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 93, characters 7-24: 93 | (Stream.of_channel in_chan) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/ltac/ltac_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I plugins/ltac/.ltac_plugin.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/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 /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Logic.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Datatypes.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Logic_Type.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Specif.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Decimal.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Hexadecimal.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Number.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Nat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/syntax/number_string_notation_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQCBOOT theories/Init/Byte.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Peano.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Wf.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQCBOOT theories/Init/Tactics.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/ltac/tauto_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQCBOOT theories/Init/Tauto.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/cc/cc_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/default/plugins/firstorder/firstorder_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQCBOOT theories/Init/Prelude.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/Bool.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Basics.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/Init.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Tactics.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Relations/Relation_Definitions.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/RelationClasses.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/Morphisms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/CRelationClasses.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/CMorphisms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/Morphisms_Prop.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/Equivalence.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/SetoidTactics.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ssr/ssrclasses.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ssr/ssrunder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ssr/ssrsetoid.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Setoids/Setoid.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/Equalities.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Relations/Relation_Operators.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Relations/Operators_Properties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Relations/Relations.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/Orders.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NumPrelude.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrdersTac.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrdersFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/GenericMinMax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZAxioms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZBase.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZAdd.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZMul.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Decidable.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZAddOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZMulOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZParity.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZPow.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZSqrt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZLog.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZDiv.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZGcd.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZBits.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NAxioms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZProperties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NBase.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NAdd.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NAddOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NMulOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NSub.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NMaxMin.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NParity.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NPow.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NSqrt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NLog.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NDiv.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NGcd.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NLcm.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NBits.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NProperties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/PeanoNat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Le.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Lt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Plus.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Gt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Minus.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Mult.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Between.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/EqdepFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Eqdep_dec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Peano_dec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Compare_dec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Factorial.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/EqNat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Wf_nat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Arith_base.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/BinNums.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/PArith/BinPosDef.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/PArith/BinPos.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/BinNatDef.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/BinNat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/PArith/Pnat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/Nnat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ring_theory.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/ring/ring_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/Lists/List.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/BinList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZAxioms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZBase.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZAdd.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZMul.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZLt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZAddOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZMulOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZMaxMin.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZParity.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZPow.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZDivFloor.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZGcd.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZLcm.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZBits.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZProperties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/BinIntDef.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/BinInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ring_polynom.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Lists/ListTactics.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zeven.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zcompare.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zorder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/Sumbool.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/ZArith_dec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zbool.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/InitialRing.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ring_tac.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ring_base.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ring.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/ArithRing.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Arith.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Bool_nat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/OrderedRing.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/Ndiv_def.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/Nsqrt_def.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/Ngcd_def.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Vectors/Fin.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Vectors/VectorDef.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Vectors/VectorSpec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Vectors/VectorEq.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Vectors/Vector.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/Bvector.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Strings/Byte.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Strings/Ascii.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Strings/String.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Strings/ByteVector.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/Ndigits.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/NArithRing.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/NArith.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Env.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/EnvRing.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Refl.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Tauto.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/RingMicromega.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zminmax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zmin.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zmax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Znat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zabs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/auxiliary.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zmisc.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Wf_Z.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zhints.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/ZArith_base.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zpow_def.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/ZArithRing.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZCoeff.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Ztac.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Max.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Min.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyClasses.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/micromega/zify_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/micromega/ZifyInst.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Zify.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/omega/PreOmega.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zcomplements.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zdiv.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Znumtheory.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/QArith_base.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Field_theory.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Field_tac.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Field.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qfield.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qring.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qreduction.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/QArith.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/VarMap.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZMicromega.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/DeclConstant.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/micromega/micromega_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/micromega/Lia.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Cantor.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Compare.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Even.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Div2.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Arith/Euclid.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Unicode/Utf8_core.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Unicode/Utf8.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Abstract/CarryType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Abstract/DoubleType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zpower.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zpow_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zgcd_alt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/omega/OmegaLemmas.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZArith_hints.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/ZArith.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int63/PrimInt63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int63/Uint63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Array/PArray.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/BoolEq.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/BoolOrder.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/DecBool.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/IfProp.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Bool/Zerob.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/CEquivalence.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/DecidableClass.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Utils.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/extraction/extraction_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/extraction/Extraction.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/FunctionalExtensionality.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Wf.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Eqdep.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/JMeq.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Equality.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ProofIrrelevanceFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ProofIrrelevance.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Subset.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Combinators.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Syntax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Program/Program.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/EquivDec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/Morphisms_Relations.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Relations_1.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/Sorted.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Lists/SetoidList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/RelationPairs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/SetoidClass.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Classes/SetoidDec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Compat/AdmitAxiom.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Compat/Coq815.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Compat/Coq814.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Compat/Coq813.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/funind/funind_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/funind/FunInd.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/DecidableType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrderedType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMapInterface.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMapList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Int.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMapAVL.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/Ndec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrderedTypeEx.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/DecidableTypeEx.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMapFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/funind/Recdef.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMapFullAVL.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMapPositive.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMapWeakList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrderedTypeAlt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FMaps.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetInterface.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetInterface.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetCompat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetGenTree.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetAVL.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrdersAlt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetAVL.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetBridge.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetDecide.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetProperties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetEqProperties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/EqualitiesFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrdersLists.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetPositive.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Ensembles.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Constructive_sets.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Finite_sets.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetToFiniteSet.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetWeakList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSetWeakList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/FSets/FSets.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Floats/FloatClass.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Floats/SpecFloat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Floats/PrimFloat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Floats/FloatOps.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Floats/FloatAxioms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/QMicromega.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/HLevels.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qabs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qpower.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qround.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ConstructiveEpsilon.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Lqa.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/PArith/POrderedType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/PArith/PArith.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy/PosExtra.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy/QExtra.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy/ConstructiveExtra.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy/ConstructiveCauchyReals.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructiveReals.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy/ConstructiveCauchyAbs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/QOrderedType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qminmax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy/ConstructiveRcomplete.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/ClassicalDedekindReals.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructiveAbs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructiveLimits.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructiveLUB.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rdefinitions.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Raxioms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rpow_def.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/RealField.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/RIneq.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/R_Ifp.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rbasic_fun.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/R_sqr.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/SplitAbsolu.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/SplitRmult.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/ArithProp.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rfunctions.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qreals.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/RMicromega.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rregisternames.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Lra.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Psatz.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Floats/FloatLemmas.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Floats/Floats.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Lists/ListDec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Lists/ListSet.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/FinFun.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/Permutation.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Lists/SetoidPermutation.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Lists/Streams.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Lists/StreamMemo.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Adjointification.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Berardi.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/PropExtensionalityFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Hurkens.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ClassicalFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ChoiceFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Classical_Prop.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Classical_Pred_Type.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Classical.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ClassicalUniqueChoice.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/RelationalChoice.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ClassicalChoice.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Description.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ClassicalDescription.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ClassicalEpsilon.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Diaconescu.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/Epsilon.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ExtensionalFunctionRepresentative.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/ExtensionalityFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/IndefiniteDescription.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/PropExtensionality.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/PropFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/SetIsType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/SetoidChoice.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/StrictProp.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/WeakFan.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Logic/WKL.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetDecide.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetProperties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetEqProperties.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Structures/OrdersEx.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetPositive.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetRBT.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSetToFiniteSet.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/MSets/MSets.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/NArith/Ndist.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/AltBinNotations.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NaryFunctions.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int31/Int31.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int31/Cyclic31.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int31/Ring31.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int63/Cyclic63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int63/Int63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int63/Ring63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/Int63/Sint63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalPos.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalN.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalNat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalZ.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalQ.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalR.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/DecimalString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalFacts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalPos.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalN.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalNat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalZ.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalQ.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalR.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/HexadecimalString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Abstract/ZDivEucl.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/Binary/ZBinary.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/NatInt/NZDomain.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NStrongRec.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NDefOps.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Abstract/NIso.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Binary/NBinary.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Numbers/Natural/Peano/NPeano.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qcanon.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/QArith/Qcabs.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructiveRealsMorphisms.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructiveMinMax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructiveSum.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Abstract/ConstructivePower.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/DiscrR.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rbase.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rseries.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/SeqProp.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rcomplete.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/PartSum.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Alembert.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/AltSeries.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Binomial.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cauchy_prod.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/ClassicalConstructiveReals.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rsigma.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rprod.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/SeqSeries.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo_fun.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo_def.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cos_rel.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Cos_plus.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo_alt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rlimit.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rderiv.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ranalysis1.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rsqrt_def.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/RList.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtopology.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/MVT.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/PSeries_reg.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo1.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Exp_prop.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ranalysis2.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ranalysis3.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo_reg.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/R_sqrt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo_calc.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rgeom.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Sqrt_reg.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ranalysis4.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rpower.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ranalysis_reg.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/RiemannInt_SF.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/RiemannInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ranalysis5.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ratan.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Machin.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rtrigo.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Ranalysis.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/NewtonInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Integration.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/ROrderedType.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Fourier_util.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/Fourier.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Reals.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rlogic.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Rminmax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Reals/Runcountable.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Classical_sets.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Partial_Order.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Cpo.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Relations_1_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Powerset.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Powerset_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Powerset_Classical_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Finite_sets_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Image.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Infinite_sets.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Integers.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Permut.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Multiset.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Relations_2.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Relations_2_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Relations_3.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Relations_3_facts.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sets/Uniset.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/CPermutation.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/PermutSetoid.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/Mergesort.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/Sorting.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/Heap.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Sorting/PermutEq.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Strings/BinaryString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Strings/HexString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Strings/OctalString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Disjoint_Union.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Inclusion.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Inverse_Image.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Transitive_Closure.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Lexicographic_Exponentiation.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Lexicographic_Product.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Union.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Well_Ordering.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/Wellfounded/Wellfounded.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zdigits.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zeuclid.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zpow_alt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zquot.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ZArith/Zwf.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/btauto/Algebra.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/btauto/Reflect.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/btauto/btauto_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/btauto/Btauto.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/derive/derive_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/derive/Derive.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellBasic.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellNatNum.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellNatInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellNatInteger.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellZNum.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellZInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrHaskellZInteger.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOCamlFloats.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOCamlInt63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOCamlPArray.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlBasic.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlChar.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlIntConv.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlNatBigInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlNatInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlNativeString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlString.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlZBigInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/extraction/ExtrOcamlZInt.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/MExtraction.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyBool.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyComparison.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyUint63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyInt63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyN.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyNat.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifyPow.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/micromega/ZifySint63.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Algebra_syntax.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ncring.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ncring_polynom.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ncring_initial.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Ncring_tac.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Cring.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Integral_domain.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/nsatz/nsatz_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/nsatz/NsatzTactic.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/nsatz/Nsatz.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/rtauto/Bintree.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/rtauto/rtauto_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/rtauto/Rtauto.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Rings_Q.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Rings_R.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/setoid_ring/Rings_Z.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/ssrmatching/ssrmatching_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC theories/ssrmatching/ssrmatching.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/ssr/ssreflect_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/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 /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 843, characters 33-47: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 852, characters 9-23: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 857, characters 12-26: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 858, characters 55-69: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 859, characters 45-59: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2409, characters 37-51: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2413, characters 17-31: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. COQC theories/ssr/ssreflect.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ssr/ssrfun.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC theories/ssr/ssrbool.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/default/plugins/ltac2/ltac2_plugin.cmxs Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. COQC user-contrib/Ltac2/Init.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Int.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Message.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Control.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Bool.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Array.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Char.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Constr.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Std.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Env.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/List.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Fresh.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Ident.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Ind.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Ltac1.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Option.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Pattern.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Printf.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/String.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Notations.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] COQC user-contrib/Ltac2/Ltac2.v Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins [cannot-open-dir,filesystem] DUNE _build/install/default/bin/coqproofworker.opt Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqtacticworker.opt Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqqueryworker.opt Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqtop Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqchk Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I checker/.coq_checklib.objs/byte -I checker/.coq_checklib.objs/native -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 220, characters 4-18: 220 | | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "checker/checker.ml", line 222, characters 4-16: 222 | | Stream.Error txt -> ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. DUNE _build/install/default/bin/csdpcert Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqnative Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/votour Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqdoc Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coqwc Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/coq_makefile Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/default/tools/CoqMakefile.in Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/install/default/bin/ocamllibdep Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/default/doc/tools/docgram/doc_grammar.exe Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/default/coq-core.install Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 82, characters 35-46: 82 | 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 90, characters 12-26: 90 | | exception Stream.Failure -> buffer buf ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 92, characters 32-43: 92 | 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 97, characters 12-26: 97 | | 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 99, characters 33-44: 99 | 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 102, characters 12-26: 102 | | exception Stream.Failure -> () ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 104, characters 34-45: 104 | 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 116, characters 12-26: 116 | | exception Stream.Failure -> accu ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 123, characters 31-48: 123 | let res = parse_args buf [] (Stream.of_channel c) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 21, characters 34-42: 21 | 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 1093, characters 15-29: 1093 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1102, characters 15-29: 1102 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1111, characters 27-41: 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1111, characters 61-75: 1111 | | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1115, characters 13-27: 1115 | else raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1121, characters 6-20: 1121 | 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 1121, characters 31-43: 1121 | 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 1140, characters 4-18: 1140 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1147, characters 62-76: 1147 | 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 1149, characters 11-25: 1149 | with Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1182, characters 52-66: 1182 | DeadEnd -> (fun (strm__ : _ LStream.t) -> raise Stream.Failure) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1193, characters 53-67: 1193 | 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 1203, characters 31-45: 1203 | try p1 strm__ with Stream.Failure -> p2 strm__) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1213, characters 17-31: 1213 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1214, characters 26-38: 1214 | 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 1224, characters 43-57: 1224 | 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 1227, characters 49-63: 1227 | (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 1230, characters 34-46: 1230 | | 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 1237, characters 4-18: 1237 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1265, characters 66-80: 1265 | (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 1267, characters 44-58: 1267 | (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 1271, characters 42-56: 1271 | | DeadEnd -> fun last_a strm -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1277, characters 35-49: 1277 | try Some (ps strm) with Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1279, characters 87-101: 1279 | 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 1282, characters 26-38: 1282 | | 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 1289, characters 20-34: 1289 | | None -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1297, characters 43-57: 1297 | 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 1307, characters 40-54: 1307 | 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 1311, characters 16-30: 1311 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1312, characters 25-37: 1312 | 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 1318, characters 44-58: 1318 | 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 1325, characters 40-54: 1325 | 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 1328, characters 44-58: 1328 | (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 1336, characters 44-58: 1336 | 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 1342, characters 43-57: 1342 | 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 1353, characters 40-54: 1353 | 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 1357, characters 16-30: 1357 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1360, characters 22-36: 1360 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1361, characters 31-43: 1361 | 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 1375, characters 40-54: 1375 | 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 1378, characters 44-58: 1378 | (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 1384, characters 20-34: 1384 | Stream.Failure -> None ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1397, characters 41-55: 1397 | 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 1421, characters 20-34: 1421 | | None -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1466, characters 52-66: 1466 | [] -> (fun levn (strm__ : _ LStream.t) -> raise Stream.Failure) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1502, characters 50-64: 1502 | 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 1523, characters 57-71: 1523 | [] -> (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 1542, characters 16-30: 1542 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1553, characters 37-51: 1553 | 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 1554, characters 63-77: 1554 | | 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 1557, characters 9-21: 1557 | raise (Stream.Error ("entry [" ^ ename ^ "] is empty")) ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1622, characters 6-20: 1622 | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1625, characters 6-18: 1625 | | Stream.Error _ as exc -> ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1624, characters 22-34: 1624 | 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 1662, characters 51-65: 1662 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1675, characters 51-65: 1675 | (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "gramlib/grammar.ml", line 1763, characters 55-69: 1763 | 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 1764, characters 62-76: 1764 | e.econtinue <- (fun _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure); ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I engine/.engine.objs/byte -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 124, characters 10-18: 124 | 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 125, characters 19-29: 125 | 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 125, characters 33-43: 125 | 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 126, characters 60-70: 126 | | 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 127, characters 26-36: 127 | | _ -> 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 127, characters 42-52: 127 | | _ -> 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 127, characters 58-68: 127 | | _ -> 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 575, characters 24-36: 575 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 144, characters 21-35: 144 | let err () = raise Stream.Failure in ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 435, characters 12-24: 435 | let bp2 = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 436, characters 8-19: 436 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 438, characters 6-17: 438 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 441, characters 16-27: 441 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 443, characters 14-25: 443 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 446, characters 13-27: 446 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 446, characters 38-50: 446 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 450, characters 6-17: 450 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 452, characters 14-25: 452 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 453, characters 22-33: 453 | Some ')' -> Stream.junk s; push_string "*)"; loc ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 455, characters 11-25: 455 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 455, characters 36-48: 455 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 458, characters 6-17: 458 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 463, characters 20-32: 463 | 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 463, characters 41-55: 463 | 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 465, characters 15-27: 465 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 469, characters 16-27: 469 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 471, characters 14-25: 471 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 472, characters 23-35: 472 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 475, characters 14-25: 475 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 477, characters 23-37: 477 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 484, characters 54-66: 484 | 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 503, characters 36-48: 503 | 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 517, characters 8-19: 517 | match Stream.peek cs with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 528, characters 16-30: 528 | | 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 531, characters 24-38: 531 | if len = 0 then raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 540, characters 17-31: 540 | | _ -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 545, characters 14-25: 545 | let c = Stream.next s in ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 548, characters 10-24: 548 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 548, characters 35-47: 548 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 550, characters 40-52: 550 | 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 558, characters 43-54: 558 | 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 561, characters 14-26: 561 | match Stream.npeek lenmarker s with ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 570, characters 48-60: 570 | 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 574, characters 63-77: 574 | 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 579, characters 22-36: 579 | | [] -> raise Stream.Failure ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 582, characters 45-57: 582 | 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 589, characters 15-27: 589 | let l' = Stream.npeek (i + 1) s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 599, characters 6-17: 599 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 608, characters 15-27: 608 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 616, characters 10-21: 616 | match Stream.peek cs with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 617, characters 30-41: 617 | | 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 618, characters 57-69: 618 | | _ -> 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 625, characters 11-23: 625 | let ep = Stream.count cs in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 646, characters 50-61: 646 | 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 648, characters 6-17: 648 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 651, characters 10-24: 651 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 651, characters 35-47: 651 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 656, characters 17-29: 656 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 665, characters 21-33: 665 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 673, characters 8-19: 673 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 685, characters 11-23: 685 | let bp = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 686, characters 8-19: 686 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 688, characters 6-17: 688 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 689, characters 15-27: 689 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 692, characters 6-17: 692 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 695, characters 6-17: 695 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 698, characters 10-24: 698 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 698, characters 35-47: 698 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 706, characters 21-33: 706 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 714, characters 6-17: 714 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 721, characters 6-17: 721 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 722, characters 15-27: 722 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 726, characters 6-17: 726 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 729, characters 10-24: 729 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 729, characters 35-47: 729 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 735, characters 17-29: 735 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 742, characters 17-29: 742 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 745, characters 6-17: 745 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 748, characters 10-24: 748 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 748, characters 35-47: 748 | Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 750, characters 15-27: 750 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 754, characters 6-17: 754 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 756, characters 14-25: 756 | match Stream.peek s with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 758, characters 12-23: 758 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 759, characters 21-33: 759 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 762, characters 12-23: 762 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 767, characters 11-25: 767 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 767, characters 36-48: 767 | with Stream.Failure -> raise (Stream.Error "") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 770, characters 6-17: 770 | Stream.junk s; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 771, characters 15-27: 771 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 785, characters 23-35: 785 | let ep = Stream.count s in ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "parsing/cLexer.ml", line 788, characters 53-64: 788 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I printing/.printing.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 585, characters 22-34: 585 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 210, characters 94-110: 210 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 1428, characters 4-16: 1428 | | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 177, characters 9-26: 177 | (Stream.of_channel in_chan) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 113, characters 20-32: 113 | 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 && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 93, characters 7-24: 93 | (Stream.of_channel in_chan) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -open Gramlib -g -bin-annot -I plugins/ssr/.ssreflect_plugin.objs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 843, characters 33-47: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 852, characters 9-23: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 857, characters 12-26: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 858, characters 55-69: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 859, characters 45-59: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2409, characters 37-51: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2413, characters 17-31: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. DUNE _build/default/coqide-server.install Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I ide/coqide/.idetop.eobjs/byte -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -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 85, characters 36-52: 85 | let pa = Pcoq.Parsable.make ~loc (Stream.of_string s) in ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "ide/coqide/idetop.ml", line 112, characters 31-47: 112 | 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 118, characters 31-47: 118 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I ide/coqide/.idetop.eobjs/byte -I ide/coqide/.idetop.eobjs/native -I /opt/pkg/lib/ocaml/site-lib/zarith -I /opt/pkg/lib/ocaml/threads -I boot/.boot.objs/byte -I boot/.boot.objs/native -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 85, characters 36-52: 85 | let pa = Pcoq.Parsable.make ~loc (Stream.of_string s) in ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "ide/coqide/idetop.ml", line 112, characters 31-47: 112 | 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 118, characters 31-47: 118 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. DUNE _build/install/default/bin/coqide Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /Users/pbulk/build/lang/coq/work/.buildlink/bin/ocamlmklib -g -o ide/coqide/coqide_gui_stubs ide/coqide/coqide_os_stubs.o) warning: /System/Volumes/Data/Applications/Xcode-13.4.1.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: archive library: ide/coqide/libcoqide_gui_stubs.a the table of contents is empty (no object file members in the library define global symbols) DUNE _build/install/default/share/coq/default.bindings Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE _build/default/coqide.install Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. DUNE revision Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. gmake[1]: Leaving directory '/Users/pbulk/build/lang/coq/work/coq-8.15.2'