==> Building on chimchar ==> Checking for remote environment... ==> Syncing package to remote host... sending incremental file list ./ PKGBUILD 2,099 46% 0.00kB/s 0:00:00 4,506 100% 2.30MB/s 0:00:00 (xfr#1, to-chk=1/3) coq-8.16.1-1.log 318 100% 310.55kB/s 0:00:00 318 100% 310.55kB/s 0:00:00 (xfr#2, to-chk=0/3) sent 1,162 bytes received 99 bytes 2,522.00 bytes/sec total size is 4,701 speedup is 3.73 ==> Patching arch to riscv64... ==> Running extra-riscv64-build -- -d /home/felix/packages/riscv64-pkg-cache:/var/cache/pacman/pkg -l felix13 on remote host... [?25l:: Synchronizing package databases... core downloading... extra downloading... community downloading... :: Starting full system upgrade... there is nothing to do [?25h==> Building in chroot for [extra] (riscv64)... ==> Synchronizing chroot copy [/var/lib/archbuild/extra-riscv64/root] -> [felix13]...done ==> Making package: coq 8.16.1-1 (Fri Feb 17 01:13:41 2023) ==> Retrieving sources...  -> Downloading coq-8.16.1.tar.gz... % Total % Received % Xferd Average Speed Time Time Time Current Dload Upload Total Spent Left Speed 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 0 0 0 0 0 0 0 0 --:--:-- 0:00:01 --:--:-- 0 100 194k 0 194k 0 0 96332 0 --:--:-- 0:00:02 --:--:-- 226k 100 5656k 0 5656k 0 0 1800k 0 --:--:-- 0:00:03 --:--:-- 2931k 100 7227k 0 7227k 0 0 2161k 0 --:--:-- 0:00:03 --:--:-- 3391k ==> Validating source files with sha512sums... coq-8.16.1.tar.gz ... Passed ==> Making package: coq 8.16.1-1 (Fri Feb 17 01:14:32 2023) ==> Checking runtime dependencies... ==> Installing missing dependencies... [?25lresolving dependencies... looking for conflicting packages... Package (3) New Version Net Change Download Size extra/ocaml-compiler-libs 4.14.0-1 139.50 MiB 34.76 MiB extra/ocaml 4.14.0-1 313.92 MiB 61.85 MiB community/ocaml-findlib 1.9.6-1 6.45 MiB 0.90 MiB Total Download Size: 97.52 MiB Total Installed Size: 459.87 MiB :: Proceed with installation? [Y/n] :: Retrieving packages... ocaml-4.14.0-1-riscv64 downloading... ocaml-compiler-libs-4.14.0-1-riscv64 downloading... ocaml-findlib-1.9.6-1-riscv64 downloading... checking keyring... checking package integrity... loading package files... checking for file conflicts... :: Processing package changes... installing ocaml... Optional dependencies for ocaml ncurses: advanced ncurses features [installed] tk: advanced tk features installing ocaml-compiler-libs... installing ocaml-findlib... [?25h==> Checking buildtime dependencies... ==> Installing missing dependencies... [?25lresolving dependencies... :: There are 3 providers available for java-environment>=6: :: Repository extra 1) jdk-openjdk 2) jdk11-openjdk 3) jdk17-openjdk Enter a number (default=1): looking for conflicting packages... warning: dependency cycle detected: warning: harfbuzz will be installed before its freetype2 dependency warning: dependency cycle detected: warning: mesa will be installed before its libglvnd dependency Package (218) New Version Net Change Download Size extra/adobe-source-code-pro-fonts 2.038ro+1.058it+1.018var-1 1.86 MiB extra/adwaita-cursors 43-2 11.53 MiB extra/adwaita-icon-theme 43-2 4.77 MiB extra/aom 3.6.0-1 4.43 MiB core/argon2 20190702-4 0.08 MiB extra/at-spi2-core 2.46.0-2 3.79 MiB extra/avahi 0.8+22+gfd482a7-3 1.70 MiB extra/bc 1.07.1-4 0.14 MiB 0.08 MiB extra/cairo 1.17.8-2 1.33 MiB extra/cantarell-fonts 1:0.303.1-1 0.19 MiB core/cryptsetup 2.6.1-1 2.50 MiB community/cython 0.29.33-1 7.53 MiB extra/dav1d 1.0.0-1 0.55 MiB core/dbus 1.14.6-1 0.77 MiB extra/dconf 0.40.0-2 0.42 MiB extra/default-cursors 2-1 0.00 MiB extra/desktop-file-utils 0.26-2 0.18 MiB core/device-mapper 2.03.18-5 0.67 MiB community/duktape 2.7.0-5 0.73 MiB extra/enchant 2.3.3-2 0.17 MiB extra/ffcall 2.4-2 0.61 MiB extra/fontconfig 2:2.14.2-1 1.00 MiB extra/freetype2 2.13.0-1 1.53 MiB extra/fribidi 1.0.12-1 0.20 MiB extra/gd 2.3.3-6 0.55 MiB extra/gdk-pixbuf2 2.42.10-2 2.90 MiB extra/giflib 5.2.1-2 0.22 MiB extra/glib-networking 1:2.74.0-1 0.59 MiB extra/graphite 1:1.3.14-3 0.17 MiB extra/gsettings-desktop-schemas 43.0-1 4.85 MiB extra/gtk-update-icon-cache 1:4.8.3-3 0.03 MiB extra/gtk2 2.24.33-2 35.47 MiB community/gtkspell3 3.0.10-2 0.19 MiB 0.06 MiB extra/harfbuzz 7.0.0-1 3.41 MiB extra/harfbuzz-icu 7.0.0-1 0.01 MiB 0.01 MiB extra/hicolor-icon-theme 0.17-2 0.05 MiB extra/http-parser 2.9.4-1 0.06 MiB core/hwdata 0.367-1 8.65 MiB extra/ijs 0.35-5 0.11 MiB core/iptables 1:1.8.9-1 1.74 MiB extra/iso-codes 4.12.0-1 18.35 MiB extra/java-environment-common 3-5 0.00 MiB extra/java-runtime-common 3-5 0.01 MiB extra/jbig2dec 0.19-1 0.12 MiB extra/jdk-openjdk 19.0.2.u7-2 240.04 MiB 224.91 MiB extra/jre-openjdk 19.0.2.u7-2 0.37 MiB 0.16 MiB extra/jre-openjdk-headless 19.0.2.u7-2 170.67 MiB extra/json-glib 1.6.6-2 0.92 MiB core/kbd 2.5.1-1 2.88 MiB core/kmod 30-3.1 0.24 MiB extra/lablgtk2 2.18.12-2 18.41 MiB 2.69 MiB extra/lcms2 2.14-2 0.58 MiB community/libavif 0.11.1-1 0.29 MiB extra/libcloudproviders 0.3.1+r8+g3a229ee-1 0.46 MiB extra/libcolord 1.4.6-1 1.20 MiB extra/libcups 1:2.4.2-5 0.74 MiB extra/libdaemon 0.14-5 0.05 MiB extra/libdatrie 0.2.13-2 0.05 MiB extra/libde265 1.0.11-1 0.57 MiB extra/libdrm 2.4.115-1 1.10 MiB core/libedit 20210910_3.1-2 0.23 MiB extra/libepoxy 1.5.10-1 2.67 MiB extra/libgit2 1:1.5.1-2 2.26 MiB extra/libglvnd 1.6.0-1 3.70 MiB extra/libheif 1.15.0-1 0.70 MiB 0.26 MiB extra/libice 1.1.1-1 0.33 MiB extra/libidn 1.41-1 0.75 MiB extra/libjpeg-turbo 2.1.4-2 1.38 MiB extra/liblqr 0.4.2-3 0.07 MiB core/libmnl 1.0.5-1 0.03 MiB extra/libnet 1:1.1.6-1 0.28 MiB core/libnetfilter_conntrack 1.0.9-1 0.14 MiB core/libnfnetlink 1.0.2-1 0.04 MiB core/libnftnl 1.2.4-1 0.22 MiB core/libnl 3.7.0-3 1.69 MiB core/libnsl 2.0.0-2 0.06 MiB extra/libomxil-bellagio 0.9.3-4 0.54 MiB extra/libpaper 1.1.28-2 0.08 MiB core/libpcap 1.10.3-1 0.58 MiB extra/libpciaccess 0.17-1 0.05 MiB extra/libpng 1.6.39-1 0.50 MiB extra/libproxy 0.4.18-2 0.22 MiB extra/libraqm 0.10.0-1 0.16 MiB extra/librsvg 2:2.55.1-1 12.25 MiB extra/libsigsegv 2.14-2 0.02 MiB extra/libsm 1.2.4-1 0.25 MiB extra/libsoup3 3.2.2-1 1.84 MiB extra/libstemmer 2.2.0-2 0.80 MiB extra/libsynctex 2022.62885-3 0.12 MiB extra/libthai 0.1.29-2 0.64 MiB extra/libtiff 4.5.0-1 6.01 MiB extra/libunwind 1.6.2-2 0.22 MiB extra/libwebp 1.3.0-2 0.73 MiB extra/libx11 1.8.4-1 9.84 MiB extra/libxau 1.0.11-1 0.02 MiB extra/libxaw 1.0.14-1 1.55 MiB extra/libxcb 1.15-2 3.60 MiB extra/libxcomposite 0.4.6-1 0.02 MiB extra/libxcursor 1.2.1-3 0.06 MiB extra/libxdamage 1.1.6-1 0.01 MiB extra/libxdmcp 1.1.4-1 0.12 MiB extra/libxext 1.3.5-1 0.29 MiB extra/libxfixes 6.0.0-2 0.03 MiB extra/libxft 2.3.7-1 0.11 MiB extra/libxi 1.8-2 0.46 MiB extra/libxinerama 1.1.5-1 0.02 MiB extra/libxkbcommon 1.5.0-1 0.70 MiB extra/libxmu 1.1.4-1 0.32 MiB extra/libxpm 3.5.15-1 0.13 MiB extra/libxrandr 1.5.3-1 0.06 MiB extra/libxrender 0.9.11-1 0.08 MiB extra/libxshmfence 1.3.2-1 0.01 MiB extra/libxt 1.2.1-1 1.91 MiB extra/libxtst 1.2.4-1 0.11 MiB extra/libxxf86vm 1.1.5-1 0.03 MiB extra/libyaml 0.2.5-2 0.15 MiB community/libyuv r2322+3aebf69d-1 1.06 MiB extra/llvm-libs 15.0.7-1 99.58 MiB extra/lm_sensors 1:3.6.0.r41.g31d1f125-2 0.41 MiB core/lzo 2.10-5 0.34 MiB extra/mesa 22.3.4-1 54.39 MiB extra/netpbm 10.73.42-2 5.14 MiB core/nspr 4.35-1 0.67 MiB core/nss 3.88.1-1 4.04 MiB community/ocaml-cairo 0.6.4-1 2.31 MiB 0.41 MiB extra/openjpeg2 2.5.0-2 13.14 MiB extra/pango 1:1.50.12-1 2.17 MiB extra/perl-error 0.17029-4 0.04 MiB extra/perl-file-which 1.27-2 0.02 MiB 0.01 MiB extra/perl-mailtools 2.21-6 0.11 MiB extra/perl-timedate 2.33-4 0.08 MiB extra/pixman 0.42.2-1 0.40 MiB extra/poppler 23.02.0-1 5.40 MiB extra/poppler-data 0.4.12-1 12.34 MiB core/popt 1.19-1 0.55 MiB extra/potrace 1.16-2 0.15 MiB community/python-autocommand 2.2.2-1 0.07 MiB community/python-babel 2.11.0-1 29.16 MiB extra/python-chardet 5.1.0-1 2.49 MiB community/python-docutils 1:0.19-2 4.26 MiB community/python-fastjsonschema 2.16.2-1 0.20 MiB extra/python-idna 3.4-1 0.67 MiB community/python-imagesize 1.4.1-2 0.03 MiB community/python-inflect 6.0.2-1 0.28 MiB community/python-jaraco.context 4.3.0-1 0.03 MiB community/python-jaraco.functools 3.5.2-1 0.05 MiB community/python-jaraco.text 3.11.1-1 0.07 MiB community/python-jinja 1:3.1.2-2 1.28 MiB community/python-latexcodec 2.0.1-5 0.13 MiB 0.03 MiB extra/python-markupsafe 2.1.2-1 0.06 MiB community/python-more-itertools 9.0.0-1 0.49 MiB extra/python-ordered-set 4.1.0-1 0.06 MiB extra/python-packaging 23.0-1 0.32 MiB extra/python-platformdirs 2.6.2-1 0.12 MiB community/python-ptyprocess 0.7.0-4 0.06 MiB community/python-pybtex 0.24.0-4 1.11 MiB 0.17 MiB community/python-pybtex-docutils 1.0.2-1 0.03 MiB 0.01 MiB community/python-pydantic 1.10.4-1 5.81 MiB community/python-pygments 2.14.0-2 12.19 MiB community/python-pytz 2022.7-1 0.14 MiB extra/python-requests 2.28.1-1 0.45 MiB extra/python-setuptools 1:67.3.0-1 3.33 MiB extra/python-six 1.16.0-6 0.09 MiB community/python-snowballstemmer 2.2.0-3 1.78 MiB community/python-soupsieve 2.4-1 0.32 MiB 0.06 MiB community/python-sphinx-alabaster-theme 0.7.13-1 0.04 MiB community/python-sphinxcontrib-applehelp 1.0.4-1 0.25 MiB community/python-sphinxcontrib-devhelp 1.0.2-9 0.13 MiB community/python-sphinxcontrib-htmlhelp 2.0.1-1 0.16 MiB community/python-sphinxcontrib-jsmath 1.0.1-12 0.01 MiB community/python-sphinxcontrib-qthelp 1.0.3-9 0.16 MiB community/python-sphinxcontrib-serializinghtml 1.1.5-4 0.13 MiB extra/python-tomli 2.0.1-1 0.08 MiB extra/python-trove-classifiers 2023.2.8-1 0.11 MiB community/python-typing_extensions 4.5.0-1 0.23 MiB 0.04 MiB extra/python-urllib3 1.26.7-5 0.69 MiB extra/python-validate-pyproject 0.12.1-1 0.22 MiB community/python-yaml 6.0-1 0.68 MiB extra/rav1e 0.6.3-1 4.33 MiB core/run-parts 5.5-1 0.04 MiB extra/shared-mime-info 2.2+13+ga2ffb28-1 4.51 MiB extra/svt-av1 1.4.1-1 3.34 MiB core/systemd 252.5-1 26.00 MiB extra/t1lib 5.1.2-8 1.07 MiB extra/texlive-core 2022.63035-1 392.93 MiB 149.09 MiB extra/tracker3 3.4.2-2 2.79 MiB extra/vulkan-icd-loader 1.3.240-1 0.43 MiB extra/wayland 1.21.0-2 0.72 MiB extra/x265 3.5-3 3.62 MiB extra/xcb-proto 1.15.2-2 0.88 MiB extra/xkeyboard-config 2.38-1 6.52 MiB extra/xorgproto 2022.2-1 1.43 MiB extra/zziplib 0.13.72-1 0.26 MiB community/antlr4 4.11.1-1 3.39 MiB 2.84 MiB community/dune 3.6.2-1 40.06 MiB 9.20 MiB community/fig2dev 3.2.8.b-1 0.68 MiB 0.28 MiB community/gendesk 1.0.9-3 6.28 MiB extra/ghostscript 10.0.0-4 37.85 MiB extra/git 2.39.2-1 33.03 MiB extra/gtk3 1:3.24.36-1 47.73 MiB community/gtksourceview3 1:3.24.11+r28+g73e57b57-1 3.83 MiB 0.60 MiB community/hevea 2.36-1 7.19 MiB 1.37 MiB extra/imagemagick 7.1.0.62-1 20.46 MiB 8.27 MiB community/lablgtk3 3.1.3-1 67.97 MiB 13.63 MiB community/ocaml-num 1.4-6 1.72 MiB 0.39 MiB community/ocaml-zarith 1.12-5 0.99 MiB 0.33 MiB core/python 3.10.9-1 81.37 MiB community/python-antlr4 4.11.1-1 0.96 MiB 0.19 MiB community/python-beautifulsoup4 4.11.2-1 1.15 MiB 0.20 MiB community/python-pexpect 4.8.0-6 0.31 MiB community/python-sphinx 5.3.0-1 15.45 MiB community/python-sphinx_rtd_theme 1.1.1-1 3.44 MiB 2.49 MiB community/python-sphinxcontrib-bibtex 2.5.0-1 0.28 MiB 0.06 MiB extra/texlive-bin 2022.62885-3 46.23 MiB extra/texlive-fontsextra 2022.62977-1 1371.14 MiB 508.30 MiB extra/texlive-latexextra 2022.63034-1 62.82 MiB 14.58 MiB extra/texlive-pictures 2022.62992-1 63.11 MiB 12.49 MiB extra/texlive-science 2022.62977-1 17.17 MiB 3.58 MiB Total Download Size: 956.77 MiB Total Installed Size: 3275.71 MiB :: Proceed with installation? [Y/n] :: Retrieving packages... texlive-fontsextra-2022.62977-1-any downloading... jdk-openjdk-19.0.2.u7-2-riscv64 downloading... texlive-core-2022.63035-1-any downloading... texlive-latexextra-2022.63034-1-any downloading... lablgtk3-3.1.3-1-riscv64 downloading... texlive-pictures-2022.62992-1-any downloading... dune-3.6.2-1-riscv64 downloading... imagemagick-7.1.0.62-1-riscv64 downloading... texlive-science-2022.62977-1-any downloading... antlr4-4.11.1-1-any downloading... lablgtk2-2.18.12-2-riscv64 downloading... python-sphinx_rtd_theme-1.1.1-1-any downloading... hevea-2.36-1-riscv64 downloading... gtksourceview3-1:3.24.11+r28+g73e57b57-1-riscv64 downloading... ocaml-cairo-0.6.4-1-riscv64 downloading... ocaml-num-1.4-6-riscv64 downloading... ocaml-zarith-1.12-5-riscv64 downloading... fig2dev-3.2.8.b-1-riscv64 downloading... libheif-1.15.0-1-riscv64 downloading... python-beautifulsoup4-4.11.2-1-any downloading... python-antlr4-4.11.1-1-any downloading... python-pybtex-0.24.0-4-any downloading... jre-openjdk-19.0.2.u7-2-riscv64 downloading... bc-1.07.1-4-riscv64 downloading... python-soupsieve-2.4-1-any downloading... gtkspell3-3.0.10-2-riscv64 downloading... python-sphinxcontrib-bibtex-2.5.0-1-any downloading... python-typing_extensions-4.5.0-1-any downloading... python-latexcodec-2.0.1-5-any downloading... perl-file-which-1.27-2-any downloading... python-pybtex-docutils-1.0.2-1-any downloading... harfbuzz-icu-7.0.0-1-riscv64 downloading... checking keyring... checking package integrity... loading package files... checking for file conflicts... :: Processing package changes... installing ocaml-num... installing ocaml-zarith... installing hicolor-icon-theme... installing libpng... installing libjpeg-turbo... Optional dependencies for libjpeg-turbo java-runtime>11: for TurboJPEG Java wrapper [pending] installing libtiff... Optional dependencies for libtiff freeglut: for using tiffgt installing shared-mime-info... installing gdk-pixbuf2... Optional dependencies for gdk-pixbuf2 libwmf: Load .wmf and .apm libopenraw: Load .dng, .cr2, .crw, .nef, .orf, .pef, .arw, .erf, .mrw, and .raf libavif: Load .avif [pending] libheif: Load .heif, .heic, and .avif [pending] libjxl: Load .jxl librsvg: Load .svg, .svgz, and .svg.gz [pending] webp-pixbuf-loader: Load .webp installing graphite... Optional dependencies for graphite graphite-docs: Documentation installing harfbuzz... installing freetype2... installing fontconfig... Creating fontconfig configuration... Rebuilding fontconfig cache... installing xcb-proto... installing libxdmcp... installing libxau... installing libxcb... installing xorgproto... installing libx11... installing libxext... installing libxrender... installing lzo... installing pixman... installing cairo... installing libdatrie... installing libthai... installing libxft... installing fribidi... installing pango... installing librsvg... installing gtk-update-icon-cache... installing adwaita-cursors... installing adwaita-icon-theme... installing dbus... installing libxi... installing libxfixes... installing libxtst... installing device-mapper... installing popt... installing argon2... installing cryptsetup... installing libmnl... installing libnftnl... installing libnl... installing libpcap... installing libnfnetlink... installing libnetfilter_conntrack... installing iptables... installing kbd... installing kmod... installing hwdata... installing systemd... warning: directory permissions differ on /var/log/journal/ filesystem: 755 package: 2755 Creating group 'sys' with GID 3. Creating group 'mem' with GID 8. Creating group 'ftp' with GID 11. Creating group 'mail' with GID 12. Creating group 'log' with GID 19. Creating group 'smmsp' with GID 25. Creating group 'proc' with GID 26. Creating group 'games' with GID 50. Creating group 'lock' with GID 54. Creating group 'network' with GID 90. Creating group 'floppy' with GID 94. Creating group 'scanner' with GID 96. Creating group 'power' with GID 98. Creating group 'nobody' with GID 65534. Creating group 'adm' with GID 999. Creating group 'wheel' with GID 998. Creating group 'utmp' with GID 997. Creating group 'audio' with GID 996. Creating group 'disk' with GID 995. Creating group 'input' with GID 994. Creating group 'kmem' with GID 993. Creating group 'kvm' with GID 992. Creating group 'lp' with GID 991. Creating group 'optical' with GID 990. Creating group 'render' with GID 989. Creating group 'sgx' with GID 988. Creating group 'storage' with GID 987. Creating group 'tty' with GID 5. Creating group 'uucp' with GID 986. Creating group 'video' with GID 985. Creating group 'users' with GID 984. Creating group 'systemd-journal' with GID 983. Creating group 'rfkill' with GID 982. Creating group 'bin' with GID 1. Creating user 'bin' (n/a) with UID 1 and GID 1. Creating group 'daemon' with GID 2. Creating user 'daemon' (n/a) with UID 2 and GID 2. Creating user 'mail' (n/a) with UID 8 and GID 12. Creating user 'ftp' (n/a) with UID 14 and GID 11. Creating group 'http' with GID 33. Creating user 'http' (n/a) with UID 33 and GID 33. Creating user 'nobody' (Kernel Overflow User) with UID 65534 and GID 65534. Creating group 'dbus' with GID 81. Creating user 'dbus' (System Message Bus) with UID 81 and GID 81. Creating group 'systemd-coredump' with GID 981. Creating user 'systemd-coredump' (systemd Core Dumper) with UID 981 and GID 981. Creating group 'systemd-network' with GID 980. Creating user 'systemd-network' (systemd Network Management) with UID 980 and GID 980. Creating group 'systemd-oom' with GID 979. Creating user 'systemd-oom' (systemd Userspace OOM Killer) with UID 979 and GID 979. Creating group 'systemd-journal-remote' with GID 978. Creating user 'systemd-journal-remote' (systemd Journal Remote) with UID 978 and GID 978. Creating group 'systemd-resolve' with GID 977. Creating user 'systemd-resolve' (systemd Resolver) with UID 977 and GID 977. Creating group 'systemd-timesync' with GID 976. Creating user 'systemd-timesync' (systemd Time Synchronization) with UID 976 and GID 976. Creating group 'tss' with GID 975. Creating user 'tss' (tss user for tpm2) with UID 975 and GID 975. Creating group 'uuidd' with GID 68. Creating user 'uuidd' (n/a) with UID 68 and GID 68. Created symlink /etc/systemd/system/getty.target.wants/getty@tty1.service → /usr/lib/systemd/system/getty@.service. Created symlink /etc/systemd/system/multi-user.target.wants/remote-fs.target → /usr/lib/systemd/system/remote-fs.target. Optional dependencies for systemd libmicrohttpd: remote journald capabilities quota-tools: kernel-level quota management systemd-sysvcompat: symlink package to provide sysvinit binaries polkit: allow administration as unprivileged user curl: systemd-journal-upload, machinectl pull-tar and pull-raw [installed] gnutls: systemd-journal-gatewayd and systemd-journal-remote [installed] libbpf: support BPF programs libfido2: unlocking LUKS2 volumes with FIDO2 token tpm2-tss: unlocking LUKS2 volumes with TPM2 [installed] installing at-spi2-core... Optional dependencies for at-spi2-core dbus-broker: Alternative bus implementation installing cantarell-fonts... installing dconf... installing desktop-file-utils... installing iso-codes... installing libcloudproviders... installing lcms2... installing libcolord... installing libdaemon... installing avahi... Optional dependencies for avahi gtk3: avahi-discover, avahi-discover-standalone, bshell, bssh, bvnc [pending] qt5-base: qt5 bindings libevent: libevent bindings [installed] nss-mdns: NSS support for mDNS python-twisted: avahi-bookmarks python-gobject: avahi-bookmarks, avahi-discover python-dbus: avahi-bookmarks, avahi-discover installing libcups... installing libpciaccess... installing libdrm... installing default-cursors... Optional dependencies for default-cursors adwaita-cursors: default cursor theme [installed] installing wayland... installing libxxf86vm... installing libxdamage... installing libxshmfence... installing libomxil-bellagio... installing libunwind... installing libedit... installing llvm-libs... installing lm_sensors... Optional dependencies for lm_sensors rrdtool: for logging with sensord perl: for sensor detection and configuration convert [installed] installing vulkan-icd-loader... Optional dependencies for vulkan-icd-loader vulkan-driver: packaged vulkan driver installing mesa... Optional dependencies for mesa opengl-man-pages: for the OpenGL API man pages mesa-vdpau: for accelerated video playback libva-mesa-driver: for accelerated video playback installing libglvnd... installing libepoxy... installing libxcomposite... installing libxcursor... installing libxinerama... installing xkeyboard-config... installing libxkbcommon... Optional dependencies for libxkbcommon libxkbcommon-x11: xkbcli interactive-x11 wayland: xkbcli interactive-wayland [installed] installing libxrandr... installing json-glib... installing duktape... installing libproxy... Optional dependencies for libproxy networkmanager: NetworkManager configuration module perl: Perl bindings [installed] python: Python 3.x bindings [pending] libproxy-webkit: PAC proxy support (via WebKit) pacrunner: PAC proxy support (via pacrunner) installing adobe-source-code-pro-fonts... installing gsettings-desktop-schemas... installing glib-networking... installing libsoup3... Optional dependencies for libsoup3 samba: Windows Domain SSO installing libstemmer... installing tracker3... Optional dependencies for tracker3 libsoup: Alternative remoting backend installing gtk3... Optional dependencies for gtk3 evince: Default print preview command installing gtksourceview3... installing dune... Optional dependencies for dune ocaml: Dune standard library [installed] installing perl-error... installing perl-timedate... installing perl-mailtools... installing git... Optional dependencies for git tk: gitk and git gui perl-libwww: git svn perl-term-readkey: git svn and interactive.singlekey setting perl-io-socket-ssl: git send-email TLS support perl-authen-sasl: git send-email TLS support perl-mediawiki-api: git mediawiki support perl-datetime-format-iso8601: git mediawiki support perl-lwp-protocol-https: git mediawiki https support perl-cgi: gitweb (web interface) support python: git svn & git p4 [pending] subversion: git svn org.freedesktop.secrets: keyring credential helper libsecret: libsecret credential helper [installed] installing enchant... Optional dependencies for enchant aspell: for aspell based spell checking support hunspell: for hunspell based spell checking support libvoikko: for libvoikko based spell checking support hspell: for hspell based spell checking support nuspell: for nuspell based spell checking support installing gtkspell3... installing gtk2... Optional dependencies for gtk2 gnome-themes-standard: Default widget theme adwaita-icon-theme: Default icon theme [installed] python: gtk-builder-convert [pending] installing lablgtk2... Optional dependencies for lablgtk2 ocaml: for using the tools [installed] installing ocaml-cairo... installing lablgtk3... Optional dependencies for lablgtk3 ocaml: for using the tools [installed] installing gendesk... installing libice... installing libsm... installing libxt... installing libxmu... installing libxpm... installing libxaw... installing t1lib... installing giflib... installing libwebp... installing aom... installing dav1d... Optional dependencies for dav1d dav1d-doc: HTML documentation installing http-parser... installing libgit2... installing rav1e... installing svt-av1... installing libyuv... installing libavif... installing libde265... Optional dependencies for libde265 ffmpeg: for sherlock265 qt5-base: for sherlock265 sdl: dec265 YUV overlay output installing x265... installing libheif... Optional dependencies for libheif libjpeg: for heif-convert and heif-enc [installed] libpng: for heif-convert and heif-enc [installed] installing gd... Optional dependencies for gd perl: bdftogd script [installed] installing openjpeg2... installing nspr... installing nss... installing poppler... Optional dependencies for poppler poppler-data: highly recommended encoding data to display PDF documents with certain encodings and characters [pending] installing ffcall... installing libsigsegv... installing zziplib... installing harfbuzz-icu... installing potrace... installing run-parts... installing libpaper... installing libsynctex... installing texlive-bin... Optional dependencies for texlive-bin ed: for texconfig biber: for bibliography processing installing texlive-core... >>> updmap custom entries should go into /etc/texmf/web2c/updmap-local.cfg >>> fmtutil custom entries should go into /etc/texmf/web2c/fmtutil-local.cnf NB: To setup ConTeXt and the lua(la)tex font db, see http://wiki.archlinux.org/index.php/TeX_Live Optional dependencies for texlive-core dialog: for texconfig ghostscript: for epstopdf, epspdf and other ConTeXt tools [pending] java-runtime: for utilities like arara, texplate [pending] perl-tk: for texdoctk psutils: to manipulate the output of dvips python: for de-macro, dviasm, pythontex [pending] ruby: for old ConTeXT MkII and epspdf t1utils: can be useful when installing Type1 fonts wdiff: for texdiff installing perl-file-which... installing texlive-latexextra... Optional dependencies for texlive-latexextra inkscape: required for svg package java-environment: to use pdfannotextractor [pending] python-pygments: for pygmentex [pending] texlive-genericextra: required for calctab package [installed] texlive-pictures: required for overpic package [pending] installing texlive-pictures... installing texlive-fontsextra... installing texlive-science... Optional dependencies for texlive-science texlive-latexextra: required for algorithm2e package [installed] installing bc... installing netpbm... installing jbig2dec... installing ijs... installing libidn... installing poppler-data... installing ghostscript... Optional dependencies for ghostscript texlive-core: needed for dvipdf [installed] gtk3: needed for gsx [installed] installing fig2dev... installing liblqr... installing libraqm... installing imagemagick... Optional dependencies for imagemagick ghostscript: PS/PDF support [installed] libheif: HEIF support [installed] libjxl: JPEG XL support libraw: DNG support librsvg: SVG support [installed] libwebp: WEBP support [installed] libwmf: WMF support libxml2: Magick Scripting Language [installed] libzip: OpenRaster support ocl-icd: OpenCL support openexr: OpenEXR support openjpeg2: JPEG2000 support [installed] djvulibre: DJVU support pango: Text rendering [installed] installing hevea... installing libnsl... installing python... Optional dependencies for python python-setuptools [pending] python-pip sqlite [installed] mpdecimal: for decimal xz: for lzma [installed] tk: for tkinter installing python-pytz... installing python-babel... installing python-docutils... installing python-imagesize... installing python-markupsafe... installing python-jinja... Optional dependencies for python-jinja python-babel: for i18n support [installed] installing python-packaging... installing python-pygments... installing python-urllib3... Optional dependencies for python-urllib3 python-pysocks: SOCKS support python-brotli: Brotli support python-pyopenssl: security support python-idna: security support [pending] installing python-chardet... installing python-idna... installing python-requests... Optional dependencies for python-requests python-pysocks: SOCKS proxy support installing python-snowballstemmer... Optional dependencies for python-snowballstemmer python-pystemmer: for improved performance installing python-sphinx-alabaster-theme... installing python-sphinxcontrib-applehelp... installing python-sphinxcontrib-devhelp... installing python-sphinxcontrib-htmlhelp... installing python-sphinxcontrib-jsmath... installing python-sphinxcontrib-qthelp... installing python-sphinxcontrib-serializinghtml... installing python-sphinx... Optional dependencies for python-sphinx imagemagick: for ext.imgconverter [installed] texlive-latexextra: for generation of PDF documentation [installed] installing python-sphinx_rtd_theme... installing python-ptyprocess... installing python-pexpect... installing python-soupsieve... installing python-beautifulsoup4... Optional dependencies for python-beautifulsoup4 python-chardet: to autodetect character encodings [installed] python-lxml: alternative HTML parser python-html5lib: alternative HTML parser installing python-more-itertools... installing python-jaraco.functools... installing python-jaraco.context... installing python-autocommand... installing cython... installing python-typing_extensions... installing python-pydantic... Optional dependencies for python-pydantic python-dotenv: for .env file support python-email-validator: for email validation installing python-inflect... installing python-jaraco.text... installing python-ordered-set... installing python-platformdirs... installing python-tomli... installing python-fastjsonschema... installing python-trove-classifiers... installing python-validate-pyproject... installing python-setuptools... installing python-six... installing libyaml... installing python-yaml... installing python-latexcodec... installing python-pybtex... installing python-pybtex-docutils... installing python-sphinxcontrib-bibtex... installing java-runtime-common... For the complete set of Java binaries to be available in your PATH, you need to re-login or source /etc/profile.d/jre.sh Please note that this package does not support forcing JAVA_HOME as former package java-common did installing libnet... installing jre-openjdk-headless... Optional dependencies for jre-openjdk-headless java-rhino: for some JavaScript support installing jre-openjdk... when you use a non-reparenting window manager, set _JAVA_AWT_WM_NONREPARENTING=1 in /etc/profile.d/jre.sh Optional dependencies for jre-openjdk alsa-lib: for basic sound support gtk2: for the Gtk+ 2 look and feel - desktop usage [installed] gtk3: for the Gtk+ 3 look and feel - desktop usage [installed] installing java-environment-common... installing jdk-openjdk... installing antlr4... installing python-antlr4... :: Running post-transaction hooks... ( 1/24) Creating system user accounts... Creating group 'avahi' with GID 974. Creating user 'avahi' (Avahi mDNS/DNS-SD daemon) with UID 974 and GID 974. Creating group 'git' with GID 973. Creating user 'git' (git daemon user) with UID 973 and GID 973. ( 2/24) Updating journal message catalog... ( 3/24) Reloading system manager configuration... Skipped: Current root is not booted. ( 4/24) Updating udev hardware database... ( 5/24) Applying kernel sysctl settings... Skipped: Current root is not booted. ( 6/24) Creating temporary files... ( 7/24) Reloading device manager configuration... Skipped: Device manager is not running. ( 8/24) Arming ConditionNeedsUpdate... ( 9/24) Updating the MIME type database... (10/24) Updating fontconfig configuration... (11/24) Reloading system bus configuration... Skipped: Current root is not booted. (12/24) Warn about old perl modules (13/24) Updating fontconfig cache... (14/24) Probing GDK-Pixbuf loader modules... (15/24) Updating GIO module cache... (16/24) Compiling GSettings XML schema files... (17/24) Probing GTK2 input method modules... (18/24) Probing GTK3 input method modules... (19/24) Updating icon theme caches... (20/24) Updating TeXLive filename database... (21/24) Updating the info directory file... (22/24) Updating TeXLive format files... fmtutil [ERROR]: not building luajittex due to missing engine: luajittex fmtutil [ERROR]: not building luajithbtex due to missing engine: luajithbtex error: command failed to execute correctly (23/24) Updating TeXLive font maps... (24/24) Updating the desktop file MIME type cache... [?25h==> Retrieving sources...  -> Found coq-8.16.1.tar.gz ==> WARNING: Skipping all source file integrity checks. ==> Extracting sources...  -> Extracting coq-8.16.1.tar.gz with bsdtar ==> Starting build()... [coqide] Generating desktop file... ok find . ! -name . '(' -name '.*' -type d -o -name 'debian' -o -name "${GIT_DIR}" -o -name '_build' -o -name '_build_ci' -o -name '_build_boot' -o -name '_install_ci' -o -name 'gramlib' -o -name 'user-contrib' -o -name 'test-suite' -o -name 'plugin_tutorial' ')' -prune -o '(' -name '*.d' ')' -exec rm -f {} + find test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' \) -exec rm -f {} + rm -f META.coq META.coq-core revision ide/coqide/default.bindings ide/coqide/default_bindings_src.exe \ kernel/genOpcodeFiles.exe config/coq_config.ml config/coq_config.py config/Makefile config/dune.c_flags rm -f coqpp/coqpp_parse.ml rm -f coqpp/coqpp_parse.mli coqpp/coqpp_lex.ml ide/coqide/coq_lex.ml \ ide/coqide/coqide_os_specific.ml ide/coqide/protocol/xml_lexer.ml ide/coqide/utf8_convert.ml \ ide/coqide/config_lexer.ml kernel/byterun/coq_arity.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h kernel/float64.ml kernel/uint63.ml \ kernel/vmopcodes.ml parsing/g_constr.ml parsing/g_prim.ml toplevel/g_toplevel.ml \ user-contrib/Ltac2/g_ltac2.ml \ vernac/g_proofs.ml plugins/btauto/g_btauto.ml plugins/cc/g_congruence.ml \ plugins/derive/g_derive.ml plugins/extraction/g_extraction.ml plugins/firstorder/g_ground.ml \ plugins/funind/g_indfun.ml plugins/ltac/coretactics.ml plugins/ltac/extraargs.ml plugins/ltac/extratactics.ml \ plugins/ltac/g_auto.ml plugins/ltac/g_class.ml plugins/ltac/g_eqdecide.ml plugins/ltac/g_obligations.ml \ plugins/ltac/profile_ltac_tactics.ml \ plugins/micromega/g_micromega.ml plugins/micromega/g_zify.ml plugins/ltac/g_ltac.ml plugins/nsatz/g_nsatz.ml \ plugins/ring/g_ring.ml plugins/ltac/g_tactic.ml \ plugins/ltac/g_rewrite.ml plugins/rtauto/g_rtauto.ml \ plugins/ssr/ssrvernac.ml plugins/ssrmatching/g_ssrmatching.ml plugins/ssr/ssrparser.ml \ plugins/syntax/g_number_string.ml tools/coqdep_lexer.ml \ tools/coqwc.ml tools/coqdoc/cpretty.ml tools/ocamllibdep.ml vernac/g_vernac.ml find theories \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' \ -o -name '*.glob' -o -name '*.aux' \) -exec rm -f {} + find test-suite -name .coq-native -empty -exec rm -rf {} + find . \( -name '*.cmi' -o -name '*.cmx' -o -name '*.o' -o -name '*.a' \ -o -name '*.cmxa' -o -name '*.cmxs' -o -name '*.aux' \) -exec rm -f {} + dune clean You have OCaml 4.14.0. Good! You have OCamlfind 1.9.6. Good! You have native-code compilation. Good! You have the Zarith library 1.12 installed. Good! LablGtk3 and LablGtkSourceView3 found (3.1.2), with native threads: => native CoqIDE will be built. Architecture : Linux Sys.os_type : Unix OCaml version : 4.14.0 OCaml binaries in : /usr/bin/ OCaml library in : /usr/lib/ocaml Native dynamic link support : true Lablgtk3 library in : CoqIDE : opt Documentation : All Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & Coq web site : http://coq.inria.fr/ Bytecode VM enabled : true Native Compiler enabled : ondemand Paths for true installation: - Coq will be copied in /usr - the Coq library will be copied in /usr/lib/coq - the Coqide configuration files will be copied in /etc/xdg/coq/ - the Coqide data files will be copied in /usr/share/coq - the Coq man pages will be copied in /usr/share/man - documentation prefix path for all Coq packages will be copied in /usr/share/doc If anything is wrong above, please restart './configure'. *Warning* To compile the system for a new architecture don't forget to do a 'make clean' before './configure'. make: Entering directory '/build/coq/src/coq-8.16.1/doc/tools/coqrst/notations' antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g make: Leaving directory '/build/coq/src/coq-8.16.1/doc/tools/coqrst/notations' /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build coq coqide revision refman-html doc-stdlib make[1]: Entering directory '/build/coq/src/coq-8.16.1' DUNE revision MKDIR BUILD_OUT DUNE _build/install/default/bin/coqdep DUNE sources (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /usr/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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /usr/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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /usr/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 86, characters 35-46: 86 | 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 94, characters 12-26: 94 | | exception Stream.Failure -> buffer buf ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 96, characters 32-43: 96 | 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 101, characters 12-26: 101 | | 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 103, characters 33-44: 103 | 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 106, characters 12-26: 106 | | exception Stream.Failure -> () ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 108, characters 34-45: 108 | 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 120, characters 12-26: 120 | | exception Stream.Failure -> accu ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 127, characters 31-48: 127 | let res = parse_args buf [] (Stream.of_channel c) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I lib/.lib.objs/byte -I lib/.lib.objs/native -I /usr/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. (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I tools/coqdep/.coqdeplib.objs/byte -I tools/coqdep/.coqdeplib.objs/native -I /usr/lib/ocaml/findlib -I /usr/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 Coqdeplib -o tools/coqdep/.coqdeplib.objs/native/coqdeplib__Common.cmx -c -impl tools/coqdep/common.ml) File "tools/coqdep/common.ml", line 254, characters 4-16: 254 | | Stream.Error msg -> Error.cannot_parse_meta_file package msg ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. COQDEP VFILES DUNE sources DUNE _build/install/default/bin/coqc DUNE _build/default/plugins/ltac/ltac_plugin.cmxs DUNE _build/default/plugins/syntax/number_string_notation_plugin.cmxs DUNE _build/default/plugins/ltac/tauto_plugin.cmxs DUNE _build/default/plugins/cc/cc_plugin.cmxs DUNE _build/default/plugins/firstorder/firstorder_plugin.cmxs DUNE _build/default/plugins/ring/ring_plugin.cmxs DUNE _build/default/plugins/micromega/zify_plugin.cmxs (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /usr/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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /usr/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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /usr/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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I /usr/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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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/kernel/byterun && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -march=rv64gc -mabi=lp64d -O2 -pipe -fexceptions -Wp,-D_FORTIFY_SOURCE=2 -Wformat -Werror=format-security -fstack-clash-protection -flto=auto -ffat-lto-objects -D_FILE_OFFSET_BITS=64 -Wall -Wno-unused -g -O2 -g -I /usr/lib/ocaml -o coq_interp.o -c coq_interp.c) coq_interp.c: In function ‘coq_interprete’: coq_interp.c:301:20: warning: storing the address of local variable ‘coq_lbl_ACC0’ in ‘coq_instr_base’ [-Wdangling-pointer=] 301 | coq_instr_base = coq_Jumptbl_base; | ^ coq_interp.c:74:26: note: ‘coq_lbl_ACC0’ declared here 74 | # define Instruct(name) coq_lbl_##name: | ^~~~~~~~ In file included from coq_interp.c:28: coq_fix_code.h:20:15: note: ‘coq_instr_base’ declared here 20 | extern char * coq_instr_base; | ^~~~~~~~~~~~~~ (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I interp/.interp.objs/byte -I interp/.interp.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 584, characters 22-34: 584 | 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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I printing/.printing.objs/byte -I printing/.printing.objs/native -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 1439, characters 4-16: 1439 | | 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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 212, characters 25-41: 212 | (Pcoq.Parsable.make (Stream.of_string ("( "^us^" )"))) ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 416, characters 20-32: 416 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "vernac/comInductive.ml", line 718, characters 20-32: 718 | 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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 103, characters 20-32: 103 | 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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 176, characters 9-26: 176 | (Stream.of_channel in_chan) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I toplevel/.toplevel.objs/byte -I toplevel/.toplevel.objs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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. DUNE _build/default/plugins/micromega/micromega_plugin.cmxs (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I plugins/ltac/.ltac_plugin.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/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 /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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. DUNE _build/default/plugins/extraction/extraction_plugin.cmxs DUNE _build/default/plugins/derive/derive_plugin.cmxs DUNE _build/default/plugins/nsatz/nsatz_plugin.cmxs DUNE _build/default/plugins/rtauto/rtauto_plugin.cmxs DUNE _build/default/plugins/ssrmatching/ssrmatching_plugin.cmxs DUNE _build/default/plugins/btauto/btauto_plugin.cmxs DUNE _build/default/plugins/funind/funind_plugin.cmxs DUNE _build/default/plugins/ssr/ssreflect_plugin.cmxs (cd _build/default && /usr/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 /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 845, characters 33-47: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 854, characters 9-23: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 859, characters 12-26: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 860, characters 55-69: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 861, characters 45-59: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2417, characters 37-51: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2421, characters 17-31: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. DUNE _build/default/plugins/ltac2/ltac2_plugin.cmxs DUNE _build/install/default/bin/coqproofworker.opt DUNE _build/install/default/bin/coqtacticworker.opt DUNE _build/install/default/bin/coqqueryworker.opt DUNE _build/install/default/bin/coqtop DUNE _build/install/default/bin/coqchk DUNE _build/install/default/bin/csdpcert DUNE _build/install/default/bin/coqnative DUNE _build/install/default/bin/votour DUNE _build/install/default/bin/coqdoc DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty DUNE _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I checker/.coq_checklib.objs/byte -I checker/.coq_checklib.objs/native -I /usr/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 226, characters 4-18: 226 | | Stream.Failure -> ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "checker/checker.ml", line 228, characters 4-16: 228 | | Stream.Error txt -> ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. DUNE _build/install/default/bin/coqwc DUNE _build/install/default/bin/coq_makefile DUNE _build/default/tools/CoqMakefile.in DUNE _build/install/default/bin/ocamllibdep DUNE _build/default/doc/tools/docgram/doc_grammar.exe DUNE _build/default/coq-core.install DUNE _build/default/coqide-server.install DUNE _build/install/default/bin/coqide DUNE _build/install/default/bin/coqidetop.opt DUNE _build/install/default/share/coq/default.bindings make[1]: 'revision' is up to date. DUNE _build/default/coqide.install AGGREGATE _build_vo/default/doc/unreleased.rst printf '\\newcommand{\\coqversion}{8.16.1}' > doc/common/version.tex export COQLIB=_build/install/default/lib/coq-core && _build/install/default/bin/coqdoc -q --gallina --body-only --latex --stdout \ -R _build_vo/default//lib/coq/theories Coq >> _build_vo/default/doc/stdlib//Library.coqdoc.tex COQCBOOT theories/Init/Notations.v COQCBOOT theories/Init/Ltac.v ./doc/stdlib/make-library-index _build_vo/default/doc/stdlib//index-list.html doc/stdlib/hidden-files Building file index-list.prehtml... COQCBOOT theories/Init/Logic.v (cd _build_vo/default/doc/stdlib/;\ latex -interaction=batchmode Library;\ latex -interaction=batchmode Library > /dev/null;\ /build/coq/src/coq-8.16.1/doc/tools/show_latex_messages -no-overfull Library.log) This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022/Arch Linux) (preloaded format=latex) restricted \write18 enabled. entering extended mode (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /usr/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 86, characters 35-46: 86 | 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 94, characters 12-26: 94 | | exception Stream.Failure -> buffer buf ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 96, characters 32-43: 96 | 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 101, characters 12-26: 101 | | 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 103, characters 33-44: 103 | 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 106, characters 12-26: 106 | | exception Stream.Failure -> () ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 108, characters 34-45: 108 | 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 120, characters 12-26: 120 | | exception Stream.Failure -> accu ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "lib/coqProject_file.ml", line 127, characters 31-48: 127 | let res = parse_args buf [] (Stream.of_channel c) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /usr/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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I lib/.lib.objs/byte -I /usr/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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /usr/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. LaTeX Warning: You have requested package `../../lib/coq-core/tools/coqdoc/coqd (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I gramlib/.gramlib.objs/byte -I /usr/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. COQCBOOT theories/Init/Datatypes.v (cd `dirname _build_vo/default/doc/stdlib//Library.dvi`; dvips -q -o `basename _build_vo/default/doc/stdlib//Library.ps` `basename _build_vo/default/doc/stdlib//Library.dvi`) (cd _build_vo/default/doc/stdlib/;\ pdflatex -interaction=batchmode Library;\ /build/coq/src/coq-8.16.1/doc/tools/show_latex_messages -no-overfull Library.log) This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022/Arch Linux) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I parsing/.parsing.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I printing/.printing.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I interp/.interp.objs/byte -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 584, characters 22-34: 584 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. LaTeX Warning: You have requested package `../../lib/coq-core/tools/coqdoc/coqd (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 1439, characters 4-16: 1439 | | 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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 212, characters 25-41: 212 | (Pcoq.Parsable.make (Stream.of_string ("( "^us^" )"))) ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 416, characters 20-32: 416 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "vernac/comInductive.ml", line 718, characters 20-32: 718 | 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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 176, characters 9-26: 176 | (Stream.of_channel in_chan) in ^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I vernac/.vernac.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 103, characters 20-32: 103 | 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 && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I toplevel/.toplevel.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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. COQCBOOT theories/Init/Specif.v (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -open Gramlib -g -bin-annot -I plugins/ssr/.ssreflect_plugin.objs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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 845, characters 33-47: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 854, characters 9-23: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 859, characters 12-26: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 860, characters 55-69: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 861, characters 45-59: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2417, characters 37-51: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "plugins/ssr/ssrparser.mlg", line 2421, characters 17-31: Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. COQCBOOT theories/Init/Wf.v COQCBOOT theories/Init/Tactics.v COQCBOOT theories/Init/Tauto.v COQCBOOT theories/Init/Decimal.v COQCBOOT theories/Init/Hexadecimal.v COQCBOOT theories/Init/Number.v COQCBOOT theories/Init/Nat.v COQCBOOT theories/Init/Byte.v COQCBOOT theories/Init/Peano.v COQCBOOT theories/Init/Prelude.v COQC theories/Bool/Bool.v COQC theories/Program/Basics.v COQC theories/Program/Tactics.v COQC theories/Relations/Relation_Definitions.v COQC theories/ssr/ssrclasses.v COQC theories/Relations/Relation_Operators.v COQC theories/Logic/Decidable.v COQC theories/Logic/EqdepFacts.v COQC theories/Numbers/BinNums.v COQC theories/Bool/Sumbool.v COQC theories/micromega/ZifyClasses.v COQC theories/extraction/Extraction.v COQC theories/Logic/FunctionalExtensionality.v COQC theories/Logic/Eqdep.v COQC theories/Logic/ProofIrrelevanceFacts.v COQC theories/Sets/Relations_1.v COQC theories/Unicode/Utf8_core.v COQC theories/extraction/ExtrOcamlBasic.v COQC theories/extraction/ExtrHaskellBasic.v COQC theories/Numbers/Cyclic/Abstract/CarryType.v COQC theories/Floats/FloatClass.v (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I ide/coqide/.idetop.eobjs/byte -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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/.platform_specific.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 96, characters 36-52: 96 | 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 123, characters 31-47: 123 | 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 129, characters 31-47: 129 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. COQC theories/Logic/HLevels.v COQC theories/Logic/PropExtensionalityFacts.v COQC theories/Logic/Hurkens.v COQC theories/Logic/ExtensionalFunctionRepresentative.v COQC theories/Logic/RelationalChoice.v (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I ide/coqide/.idetop.eobjs/byte -I ide/coqide/.idetop.eobjs/native -I /usr/lib/ocaml/findlib -I /usr/lib/ocaml/threads -I /usr/lib/ocaml/zarith -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/.platform_specific.objs/byte -I ide/coqide/.platform_specific.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 96, characters 36-52: 96 | 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 123, characters 31-47: 123 | 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 129, characters 31-47: 129 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in ^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. COQC theories/Logic/SetIsType.v COQC theories/Logic/PropFacts.v COQC theories/Logic/ExtensionalityFacts.v COQC theories/Logic/Adjointification.v COQC theories/Logic/Berardi.v COQC theories/Logic/StrictProp.v COQC theories/derive/Derive.v COQC theories/setoid_ring/Algebra_syntax.v COQC theories/Wellfounded/Transitive_Closure.v COQC theories/Wellfounded/Inverse_Image.v COQC theories/Wellfounded/Well_Ordering.v COQC theories/Wellfounded/Disjoint_Union.v COQC theories/Wellfounded/Inclusion.v COQC theories/Compat/Coq816.v COQC theories/Compat/AdmitAxiom.v COQC theories/Numbers/AltBinNotations.v COQC theories/ssrmatching/ssrmatching.v COQC theories/Lists/Streams.v COQC theories/Bool/IfProp.v COQC theories/Bool/BoolEq.v COQC theories/Bool/DecBool.v COQC theories/funind/FunInd.v COQC theories/Sets/Ensembles.v COQC theories/Sets/Relations_1_facts.v COQC theories/Sets/Permut.v COQC theories/Sets/Relations_2.v COQC user-contrib/Ltac2/Init.v COQC theories/Classes/Init.v COQC theories/ssr/ssrunder.v COQC theories/Relations/Operators_Properties.v COQC theories/Logic/Eqdep_dec.v COQC theories/PArith/BinPosDef.v COQC theories/Program/Utils.v COQC theories/Logic/JMeq.v COQC theories/Logic/ProofIrrelevance.v COQC theories/Program/Combinators.v COQC theories/Unicode/Utf8.v COQC theories/Numbers/Cyclic/Int63/PrimInt63.v COQC theories/Wellfounded/Union.v COQC theories/Wellfounded/Lexicographic_Product.v COQC theories/Compat/Coq815.v COQC theories/Lists/StreamMemo.v COQC theories/Sets/Partial_Order.v COQC theories/Sets/Constructive_sets.v COQC theories/Sets/Uniset.v COQC theories/Sets/Relations_3.v COQC theories/Sets/Relations_2_facts.v COQC theories/ssr/ssreflect.v COQC user-contrib/Ltac2/Ident.v COQC user-contrib/Ltac2/Message.v COQC user-contrib/Ltac2/Char.v COQC user-contrib/Ltac2/Constr.v COQC user-contrib/Ltac2/Std.v COQC user-contrib/Ltac2/Ltac1.v COQC user-contrib/Ltac2/Control.v COQC user-contrib/Ltac2/Int.v COQC user-contrib/Ltac2/Bool.v COQC user-contrib/Ltac2/Ind.v COQC user-contrib/Ltac2/Option.v COQC user-contrib/Ltac2/String.v COQC theories/Classes/RelationClasses.v COQC theories/Classes/CRelationClasses.v COQC theories/Relations/Relations.v COQC theories/Program/Wf.v COQC theories/Program/Equality.v COQC theories/Floats/PrimFloat.v COQC theories/Compat/Coq814.v COQC theories/Sets/Cpo.v COQC theories/Sets/Finite_sets.v COQC theories/Sets/Relations_3_facts.v COQC theories/ssr/ssrfun.v COQC user-contrib/Ltac2/Printf.v COQC user-contrib/Ltac2/Env.v COQC user-contrib/Ltac2/Pattern.v COQC user-contrib/Ltac2/List.v COQC user-contrib/Ltac2/Array.v COQC theories/Classes/Morphisms.v COQC theories/Classes/CMorphisms.v COQC theories/ssr/ssrsetoid.v COQC theories/Program/Subset.v COQC theories/Sets/Powerset.v COQC theories/ssr/ssrbool.v COQC user-contrib/Ltac2/Fresh.v COQC user-contrib/Ltac2/Notations.v COQC theories/Classes/Morphisms_Prop.v COQC theories/Classes/Equivalence.v COQC theories/Classes/CEquivalence.v COQC theories/Sets/Powerset_facts.v COQC user-contrib/Ltac2/Ltac2.v COQC theories/Classes/SetoidTactics.v COQC theories/Setoids/Setoid.v COQC theories/Numbers/NumPrelude.v COQC theories/Structures/Equalities.v COQC theories/Structures/Orders.v COQC theories/Structures/OrdersTac.v COQC theories/Bool/BoolOrder.v COQC theories/Structures/OrdersFacts.v COQC theories/Structures/GenericMinMax.v COQC theories/Numbers/NatInt/NZAxioms.v COQC theories/Numbers/NatInt/NZBase.v COQC theories/Numbers/NatInt/NZAdd.v COQC theories/Numbers/NatInt/NZOrder.v COQC theories/Numbers/NatInt/NZMul.v COQC theories/Numbers/NatInt/NZAddOrder.v COQC theories/Numbers/NatInt/NZMulOrder.v COQC theories/Numbers/NatInt/NZParity.v COQC theories/Numbers/NatInt/NZPow.v COQC theories/Numbers/NatInt/NZSqrt.v COQC theories/Numbers/NatInt/NZDiv.v COQC theories/Numbers/NatInt/NZGcd.v COQC theories/Numbers/NatInt/NZProperties.v COQC theories/Numbers/NatInt/NZLog.v Done COQC theories/Numbers/NatInt/NZBits.v COQC theories/Numbers/Natural/Abstract/NAxioms.v COQC theories/Numbers/Integer/Abstract/ZAxioms.v COQC theories/Numbers/Natural/Abstract/NBase.v COQC theories/Numbers/Integer/Abstract/ZBase.v COQC theories/Numbers/Integer/Abstract/ZAdd.v COQC theories/Numbers/Natural/Abstract/NAdd.v COQC theories/Numbers/Natural/Abstract/NIso.v COQC theories/Numbers/Natural/Abstract/NOrder.v COQC theories/Numbers/Integer/Abstract/ZMul.v COQC theories/Numbers/Integer/Abstract/ZLt.v COQC theories/Numbers/Natural/Abstract/NAddOrder.v COQC theories/Numbers/Integer/Abstract/ZAddOrder.v COQC theories/Numbers/Natural/Abstract/NMulOrder.v COQC theories/Numbers/Natural/Abstract/NSub.v COQC theories/Numbers/Integer/Abstract/ZMulOrder.v COQC theories/Numbers/Natural/Abstract/NMaxMin.v COQC theories/Numbers/Natural/Abstract/NParity.v COQC theories/Numbers/Natural/Abstract/NSqrt.v COQC theories/Numbers/Natural/Abstract/NDiv.v COQC theories/Numbers/Natural/Abstract/NGcd.v COQC theories/Numbers/Natural/Abstract/NStrongRec.v COQC theories/Numbers/Integer/Abstract/ZMaxMin.v COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v COQC theories/Numbers/Integer/Abstract/ZParity.v COQC theories/Numbers/Natural/Abstract/NPow.v COQC theories/Numbers/Natural/Abstract/NLog.v COQC theories/Numbers/Natural/Abstract/NLcm.v COQC theories/Numbers/Natural/Abstract/NBits.v COQC theories/Numbers/Integer/Abstract/ZPow.v COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v COQC theories/Numbers/Integer/Abstract/ZDivFloor.v COQC theories/Numbers/Integer/Abstract/ZGcd.v COQC theories/Numbers/Integer/Abstract/ZDivEucl.v COQC theories/Numbers/Integer/Abstract/ZBits.v COQC theories/Numbers/Integer/Abstract/ZLcm.v COQC theories/Numbers/Natural/Abstract/NProperties.v COQC theories/Arith/PeanoNat.v COQC theories/Arith/Arith_prebase.v COQC theories/Arith/EqNat.v COQC theories/Lists/List.v COQC theories/Arith/Max.v COQC theories/Arith/Min.v COQC theories/Arith/Even.v COQC theories/Arith/Le.v COQC theories/Arith/Lt.v COQC theories/Arith/Plus.v COQC theories/Arith/Minus.v COQC theories/Arith/Between.v COQC theories/Arith/Peano_dec.v COQC theories/Arith/Gt.v COQC theories/Arith/Mult.v COQC theories/PArith/BinPos.v COQC theories/Numbers/NatInt/NZDomain.v COQC theories/Sets/Multiset.v COQC theories/Numbers/Integer/Abstract/ZProperties.v COQC theories/Arith/Compare_dec.v COQC theories/Arith/Factorial.v COQC theories/Arith/Div2.v COQC theories/Numbers/Natural/Peano/NPeano.v COQC theories/Arith/Wf_nat.v COQC theories/Arith/Bool_nat.v COQC theories/Arith/Arith_base.v COQC theories/Arith/Euclid.v COQC theories/Logic/ClassicalFacts.v COQC theories/funind/Recdef.v COQC theories/Vectors/Fin.v COQC theories/Arith/Compare.v COQC theories/Logic/PropExtensionality.v COQC theories/Logic/Classical_Prop.v COQC theories/Vectors/VectorDef.v COQC theories/Logic/Classical_Pred_Type.v COQC theories/Logic/Classical.v COQC theories/Logic/ClassicalUniqueChoice.v COQC theories/Sets/Classical_sets.v COQC theories/NArith/BinNatDef.v COQC theories/PArith/Pnat.v COQC theories/PArith/POrderedType.v COQC theories/Sets/Powerset_Classical_facts.v COQC theories/NArith/BinNat.v COQC theories/PArith/PArith.v COQC theories/Lists/ListDec.v COQC theories/Logic/WeakFan.v COQC theories/Wellfounded/Lexicographic_Exponentiation.v COQC theories/rtauto/Bintree.v COQC theories/Numbers/NaryFunctions.v COQC theories/Lists/ListSet.v COQC theories/Sets/Finite_sets_facts.v COQC theories/setoid_ring/BinList.v COQC theories/Lists/ListTactics.v COQC theories/Vectors/VectorSpec.v COQC theories/micromega/Refl.v COQC theories/Sorting/Sorted.v COQC theories/Logic/FinFun.v COQC theories/Wellfounded/Wellfounded.v COQC theories/rtauto/Rtauto.v COQC theories/Sets/Image.v COQC theories/Lists/SetoidList.v COQC theories/NArith/Nnat.v COQC theories/setoid_ring/Ring_theory.v COQC theories/ZArith/BinIntDef.v COQC theories/NArith/Ndiv_def.v COQC theories/NArith/Nsqrt_def.v COQC theories/NArith/Ngcd_def.v COQC theories/Vectors/VectorEq.v COQC theories/micromega/Tauto.v COQC theories/Numbers/Natural/Binary/NBinary.v COQC theories/Sorting/Permutation.v COQC theories/Sets/Infinite_sets.v COQC theories/ZArith/BinInt.v COQC theories/Strings/Byte.v COQC theories/Vectors/Vector.v COQC theories/Bool/Bvector.v COQC theories/Sets/Integers.v COQC theories/Program/Syntax.v COQC theories/Program/Program.v COQC theories/Classes/Morphisms_Relations.v COQC theories/Classes/SetoidClass.v COQC theories/Classes/EquivDec.v COQC theories/Sorting/Mergesort.v COQC theories/Sorting/CPermutation.v COQC theories/Classes/RelationPairs.v COQC theories/Structures/DecidableType.v COQC theories/Structures/OrderedType.v COQC theories/Lists/SetoidPermutation.v COQC theories/Sorting/Sorting.v COQC theories/Structures/EqualitiesFacts.v COQC theories/Numbers/Natural/Abstract/NDefOps.v COQC theories/MSets/MSetInterface.v COQC theories/Structures/OrderedTypeAlt.v COQC theories/Structures/OrdersAlt.v COQC theories/FSets/FSetInterface.v COQC theories/FSets/FMapInterface.v COQC theories/setoid_ring/Ring_polynom.v COQC theories/ZArith/Zeven.v COQC theories/ZArith/Zcompare.v COQC theories/ZArith/Znat.v COQC theories/ZArith/Zpow_def.v COQC theories/micromega/Env.v COQC theories/Numbers/Cyclic/Abstract/DoubleType.v COQC theories/Structures/OrdersLists.v COQC theories/Numbers/Integer/Binary/ZBinary.v COQC theories/ZArith/Zpow_alt.v COQC theories/ZArith/Zeuclid.v COQC theories/ZArith/Int.v COQC theories/FSets/FMapList.v COQC theories/FSets/FSetBridge.v COQC theories/FSets/FMapWeakList.v COQC theories/MSets/MSetWeakList.v COQC theories/MSets/MSetList.v COQC theories/ZArith/Zorder.v COQC theories/omega/OmegaLemmas.v COQC theories/micromega/EnvRing.v COQC theories/ZArith/ZArith_dec.v COQC theories/ZArith/Zminmax.v COQC theories/ZArith/Zmin.v COQC theories/ZArith/Zmax.v COQC theories/ZArith/Zabs.v COQC theories/ZArith/auxiliary.v COQC theories/ZArith/Zmisc.v COQC theories/ZArith/Zbool.v COQC theories/ZArith/Wf_Z.v COQC theories/ZArith/Zhints.v COQC theories/ZArith/ZArith_base.v COQC theories/micromega/VarMap.v COQC theories/setoid_ring/Ncring.v COQC theories/setoid_ring/InitialRing.v COQC theories/setoid_ring/Ncring_polynom.v COQC theories/Strings/Ascii.v COQC theories/setoid_ring/Ring_tac.v COQC theories/setoid_ring/Ring_base.v COQC theories/setoid_ring/Ring.v COQC theories/setoid_ring/ArithRing.v COQC theories/micromega/OrderedRing.v COQC theories/setoid_ring/NArithRing.v COQC theories/setoid_ring/ZArithRing.v COQC theories/setoid_ring/Field_theory.v COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v COQC theories/micromega/Ztac.v COQC theories/ZArith/Zcomplements.v COQC theories/QArith/QArith_base.v COQC theories/Arith/Arith.v COQC theories/ZArith/Zdiv.v COQC theories/ZArith/Zpower.v COQC theories/micromega/ZifyInst.v COQC theories/Classes/SetoidDec.v COQC theories/extraction/ExtrHaskellNatNum.v COQC theories/extraction/ExtrOcamlNatBigInt.v COQC theories/Logic/ConstructiveEpsilon.v COQC theories/extraction/ExtrOcamlNatInt.v COQC theories/Logic/ChoiceFacts.v COQC theories/Logic/WKL.v COQC theories/micromega/ZifyPow.v COQC theories/Bool/Zerob.v COQC theories/MSets/MSetGenTree.v COQC theories/micromega/Zify.v COQC theories/Strings/String.v COQC theories/ZArith/Znumtheory.v COQC theories/extraction/ExtrHaskellNatInt.v COQC theories/extraction/ExtrHaskellNatInteger.v COQC theories/QArith/QOrderedType.v COQC theories/micromega/ZifyN.v COQC theories/micromega/ZifyNat.v COQC theories/Strings/OctalString.v COQC theories/Strings/HexString.v COQC theories/Strings/BinaryString.v COQC theories/omega/PreOmega.v COQC theories/Strings/ByteVector.v COQC theories/micromega/DeclConstant.v COQC theories/extraction/ExtrHaskellString.v COQC theories/extraction/ExtrOcamlChar.v COQC theories/QArith/Qminmax.v COQC theories/Logic/ClassicalChoice.v COQC theories/Logic/Description.v COQC theories/Logic/IndefiniteDescription.v COQC theories/Logic/Epsilon.v COQC theories/Logic/ClassicalEpsilon.v COQC theories/Logic/ClassicalDescription.v COQC theories/Logic/Diaconescu.v COQC theories/Structures/OrdersEx.v COQC theories/Numbers/DecimalString.v COQC theories/Numbers/HexadecimalString.v COQC theories/NArith/Ndigits.v COQC theories/extraction/ExtrOcamlString.v COQC theories/extraction/ExtrOcamlNativeString.v COQC theories/Logic/SetoidChoice.v COQC theories/MSets/MSetAVL.v COQC theories/MSets/MSetRBT.v COQC theories/NArith/NArith.v COQC theories/QArith/Qreduction.v COQC theories/NArith/Ndec.v COQC theories/NArith/Ndist.v COQC theories/MSets/MSetPositive.v COQC theories/micromega/RingMicromega.v COQC theories/Structures/OrderedTypeEx.v COQC theories/setoid_ring/Field_tac.v COQC theories/setoid_ring/Field.v COQC theories/QArith/Qfield.v COQC theories/Structures/DecidableTypeEx.v COQC theories/FSets/FSetPositive.v COQC theories/QArith/Qring.v COQC theories/FSets/FSetFacts.v COQC theories/MSets/MSetFacts.v COQC theories/FSets/FMapFacts.v COQC theories/micromega/ZCoeff.v COQC theories/QArith/QArith.v COQC theories/FSets/FSetDecide.v COQC theories/micromega/ZMicromega.v COQC theories/micromega/QMicromega.v COQC theories/QArith/Qabs.v COQC theories/QArith/Qround.v COQC theories/QArith/Qcanon.v COQC theories/FSets/FSetCompat.v COQC theories/MSets/MSetDecide.v COQC theories/micromega/Lqa.v COQC theories/Reals/Abstract/ConstructiveReals.v COQC theories/FSets/FSetProperties.v COQC theories/FSets/FSetWeakList.v COQC theories/FSets/FSetList.v COQC theories/micromega/Lia.v COQC theories/QArith/Qcabs.v COQC theories/micromega/ZArith_hints.v COQC theories/ZArith/Zpow_facts.v COQC theories/ZArith/Zgcd_alt.v COQC theories/Arith/Cantor.v COQC theories/ZArith/Zquot.v COQC theories/ZArith/Zwf.v COQC theories/Sorting/PermutSetoid.v COQC theories/MSets/MSetProperties.v COQC theories/ZArith/ZArith.v COQC theories/QArith/Qpower.v COQC theories/Reals/Cauchy/PosExtra.v COQC theories/Reals/Cauchy/ConstructiveExtra.v COQC theories/Numbers/DecimalFacts.v COQC theories/Numbers/HexadecimalFacts.v COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v COQC theories/Numbers/Cyclic/Int31/Int31.v COQC theories/micromega/ZifyBool.v COQC theories/micromega/ZifyComparison.v COQC theories/ZArith/Zdigits.v COQC theories/Sorting/Heap.v COQC theories/Sorting/PermutEq.v COQC theories/FSets/FSetAVL.v COQC theories/FSets/FMapAVL.v COQC theories/FSets/FSetToFiniteSet.v COQC theories/FSets/FMapPositive.v COQC theories/FSets/FSetEqProperties.v COQC theories/Classes/DecidableClass.v COQC theories/extraction/ExtrHaskellZNum.v COQC theories/extraction/ExtrOcamlZInt.v COQC theories/extraction/ExtrOcamlIntConv.v COQC theories/Numbers/Cyclic/Int63/Uint63.v COQC theories/extraction/ExtrHaskellZInteger.v COQC theories/extraction/ExtrOcamlZBigInt.v COQC theories/Floats/SpecFloat.v COQC theories/Reals/Cauchy/QExtra.v COQC theories/Reals/Abstract/ConstructiveAbs.v COQC theories/Numbers/DecimalPos.v COQC theories/Numbers/DecimalNat.v COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v COQC theories/Numbers/Cyclic/Int31/Cyclic31.v COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v COQC theories/btauto/Algebra.v COQC theories/FSets/FMaps.v COQC theories/FSets/FSets.v COQC theories/MSets/MSetEqProperties.v COQC theories/MSets/MSetToFiniteSet.v COQC theories/extraction/ExtrHaskellZInt.v COQC theories/Reals/Cauchy/ConstructiveCauchyReals.v COQC theories/Reals/Abstract/ConstructiveLimits.v COQC theories/Numbers/HexadecimalNat.v COQC theories/Numbers/DecimalN.v COQC theories/Numbers/HexadecimalPos.v COQC theories/Numbers/DecimalZ.v COQC theories/Numbers/Cyclic/Int63/Cyclic63.v COQC theories/micromega/ZifyUint63.v COQC theories/btauto/Reflect.v COQC theories/Reals/Abstract/ConstructiveRealsMorphisms.v COQC theories/MSets/MSets.v COQC theories/Numbers/Cyclic/Int63/Sint63.v COQC theories/Floats/FloatOps.v COQC theories/Reals/Abstract/ConstructiveLUB.v COQC theories/Array/PArray.v COQC theories/setoid_ring/Ncring_initial.v COQC theories/Numbers/DecimalQ.v COQC theories/Numbers/Cyclic/Int31/Ring31.v COQC theories/Numbers/Cyclic/Int63/Ring63.v COQC theories/btauto/Btauto.v COQC theories/Floats/FloatAxioms.v COQC theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v COQC theories/extraction/ExtrOCamlPArray.v COQC theories/Reals/Abstract/ConstructiveSum.v COQC theories/Reals/Abstract/ConstructiveMinMax.v COQC theories/extraction/ExtrOCamlInt63.v COQC theories/micromega/ZifySint63.v COQC theories/FSets/FMapFullAVL.v COQC theories/Reals/Abstract/ConstructivePower.v COQC theories/Numbers/HexadecimalN.v COQC theories/Numbers/HexadecimalZ.v COQC theories/Numbers/HexadecimalQ.v COQC theories/setoid_ring/Ncring_tac.v COQC theories/Reals/Cauchy/ConstructiveCauchyAbs.v COQC theories/setoid_ring/Cring.v COQC theories/setoid_ring/Integral_domain.v COQC theories/nsatz/NsatzTactic.v COQC theories/setoid_ring/Rings_Q.v COQC theories/setoid_ring/Rings_Z.v COQC theories/Reals/Cauchy/ConstructiveRcomplete.v COQC theories/Reals/ClassicalDedekindReals.v COQC theories/Reals/Rdefinitions.v COQC theories/Reals/Raxioms.v COQC theories/Reals/Rpow_def.v COQC theories/Numbers/HexadecimalR.v COQC theories/Numbers/DecimalR.v COQC theories/setoid_ring/RealField.v COQC theories/Reals/ClassicalConstructiveReals.v COQC theories/Reals/RIneq.v COQC theories/Reals/R_Ifp.v COQC theories/Reals/SplitRmult.v COQC theories/QArith/Qreals.v COQC theories/Reals/DiscrR.v COQC theories/Reals/Rlogic.v COQC theories/Reals/Rbase.v COQC theories/Reals/ROrderedType.v COQC theories/Reals/Rbasic_fun.v COQC theories/Reals/R_sqr.v COQC theories/Reals/SplitAbsolu.v COQC theories/Reals/ArithProp.v COQC theories/Reals/Rminmax.v COQC theories/Reals/Rfunctions.v COQC theories/micromega/RMicromega.v COQC theories/Reals/Rregisternames.v COQC theories/Reals/Rseries.v COQC theories/Reals/RList.v COQC theories/Reals/Runcountable.v COQC theories/Reals/SeqProp.v COQC theories/micromega/Lra.v COQC theories/micromega/MExtraction.v COQC theories/micromega/Psatz.v COQC theories/Reals/Rlimit.v COQC theories/micromega/Fourier_util.v COQC theories/micromega/Fourier.v COQC theories/Floats/FloatLemmas.v COQC theories/Reals/Rcomplete.v COQC theories/Reals/Rderiv.v COQC theories/Reals/PartSum.v COQC theories/Reals/Ranalysis1.v COQC theories/Floats/Floats.v COQC theories/Reals/AltSeries.v COQC theories/Reals/Binomial.v COQC theories/Reals/Rsigma.v COQC theories/Reals/Cauchy_prod.v COQC theories/Reals/Alembert.v COQC theories/extraction/ExtrOCamlFloats.v COQC theories/Reals/Rprod.v COQC theories/Reals/Rtopology.v COQC theories/Reals/Ranalysis2.v COQC theories/Reals/SeqSeries.v COQC theories/Reals/Ranalysis3.v COQC theories/Reals/MVT.v COQC theories/Reals/Rtrigo_fun.v COQC theories/Reals/Rsqrt_def.v COQC theories/Reals/Rtrigo_def.v COQC theories/Reals/PSeries_reg.v COQC theories/Reals/R_sqrt.v COQC theories/Reals/Rtrigo_alt.v COQC theories/Reals/Cos_rel.v COQC theories/Reals/Sqrt_reg.v COQC theories/Reals/Cos_plus.v COQC theories/Reals/Rtrigo1.v COQC theories/Reals/Exp_prop.v COQC theories/Reals/Rtrigo_reg.v COQC theories/Reals/Rtrigo_calc.v COQC theories/Reals/Rgeom.v COQC theories/Reals/Ranalysis4.v COQC theories/Reals/Rpower.v COQC theories/Reals/Ranalysis_reg.v COQC theories/Reals/Rtrigo_facts.v COQC theories/Reals/RiemannInt_SF.v COQC theories/Reals/RiemannInt.v COQC theories/Reals/Ranalysis5.v COQC theories/Reals/Ratan.v COQC theories/Reals/Machin.v COQC theories/Reals/Rtrigo.v COQC theories/Reals/Ranalysis.v COQC theories/Reals/NewtonInt.v COQC theories/Reals/Integration.v COQC theories/Reals/Reals.v COQC theories/nsatz/Nsatz.v COQC theories/setoid_ring/Rings_R.v rm -rf _build_vo/default/doc/stdlib/html/ mkdir -p -p _build_vo/default/doc/stdlib/html/ SPHINXBUILD doc/sphinx (html) COQDOC VFILES Running Sphinx v5.3.0 WARNING: Invalid configuration value found: 'language = None'. Update your configuration to a valid language code. Falling back to 'en' (English). making output directory... done checking bibtex cache... out of date parsing bibtex file /build/coq/src/coq-8.16.1/doc/sphinx/biblio.bib... parsed 55 entries Copying /build/coq/src/coq-8.16.1/doc/sphinx/index.html.rst to /build/coq/src/coq-8.16.1/doc/sphinx/index.rst Copying /build/coq/src/coq-8.16.1/doc/sphinx/zebibliography.html.rst to /build/coq/src/coq-8.16.1/doc/sphinx/zebibliography.rst building [mo]: targets for 0 po files that are out of date building [html]: targets for 75 source files that are out of date updating environment: [new config] 77 added, 0 changed, 0 removed reading sources... [ 1%] addendum/canonical-structures reading sources... [ 2%] addendum/extended-pattern-matching reading sources... [ 3%] addendum/extraction Duplicate cmd name: Extraction reading sources... [ 5%] addendum/generalized-rewriting reading sources... [ 6%] addendum/implicit-coercions reading sources... [ 7%] addendum/micromega reading sources... [ 9%] addendum/miscellaneous-extensions reading sources... [ 10%] addendum/nsatz reading sources... [ 11%] addendum/parallel-proof-processing reading sources... [ 12%] addendum/program reading sources... [ 14%] addendum/ring reading sources... [ 15%] addendum/sprop reading sources... [ 16%] addendum/type-classes reading sources... [ 18%] addendum/universe-polymorphism mv _build_vo/default/doc/stdlib/html//index.html _build_vo/default/doc/stdlib/html//genindex.html mkdir -p -p _build_vo/default/doc/stdlib/html/ cat doc/common/styles/html/coqremote/header.html _build_vo/default/doc/stdlib//index-list.html > _build_vo/default/doc/stdlib/html//index.html cat doc/common/styles/html/coqremote/footer.html >> _build_vo/default/doc/stdlib/html//index.html reading sources... [ 19%] appendix/history-and-changes/index reading sources... [ 20%] appendix/indexes/index reading sources... [ 22%] changes reading sources... [ 23%] coq-attrindex reading sources... [ 24%] coq-cmdindex reading sources... [ 25%] coq-exnindex reading sources... [ 27%] coq-optindex reading sources... [ 28%] coq-tacindex reading sources... [ 29%] genindex reading sources... [ 31%] history reading sources... [ 32%] index reading sources... [ 33%] language/cic reading sources... [ 35%] language/coq-library reading sources... [ 36%] language/core/assumptions reading sources... [ 37%] language/core/basic reading sources... [ 38%] language/core/coinductive reading sources... [ 40%] language/core/conversion reading sources... [ 41%] language/core/definitions reading sources... [ 42%] language/core/index reading sources... [ 44%] language/core/inductive reading sources... [ 45%] language/core/modules reading sources... [ 46%] language/core/primitive reading sources... [ 48%] language/core/records reading sources... [ 49%] language/core/sections reading sources... [ 50%] language/core/sorts reading sources... [ 51%] language/core/variants reading sources... [ 53%] language/extensions/arguments-command reading sources... [ 54%] language/extensions/canonical reading sources... [ 55%] language/extensions/evars reading sources... [ 57%] language/extensions/implicit-arguments reading sources... [ 58%] language/extensions/index reading sources... [ 59%] language/extensions/match reading sources... [ 61%] language/gallina-extensions reading sources... [ 62%] language/gallina-specification-language reading sources... [ 63%] language/module-system reading sources... [ 64%] license reading sources... [ 66%] practical-tools/coq-commands reading sources... [ 67%] practical-tools/coqide reading sources... [ 68%] practical-tools/utilities reading sources... [ 70%] proof-engine/ltac Extension error: /build/coq/src/coq-8.16.1/doc/sphinx/proof-engine/ltac.rst:2463: Error while sending the following to coqtop: tac. coqtop output: Full error text: Timeout exceeded. command: /build/coq/src/coq-8.16.1/_build/install/default/bin/coqtop args: [b'/build/coq/src/coq-8.16.1/_build/install/default/bin/coqtop', b'-q', b'-color', b'on'] buffer (last 100 chars): '' before (last 100 chars): '' after: match: None match_index: None exitstatus: None flag_eof: False pid: 59403 child_fd: 7 closed: False timeout: 30 delimiter: logfile: None logfile_read: None logfile_send: None maxread: 2000 ignorecase: False searchwindowsize: None delaybeforesend: 0 delayafterclose: 0.1 delayafterterminate: 0.1 searcher: searcher_re: 0: re.compile('\r\n[^< \r\n]+ < ') Duplicate exn name: Not equal Duplicate exn name: Not equal (due to universes) make[1]: *** [Makefile.doc:84: refman-html] Error 2 make[1]: Leaving directory '/build/coq/src/coq-8.16.1' make: *** [Makefile.make:122: submake] Error 2 ==> ERROR: A failure occurred in build().  Aborting... ==> ERROR: Build failed, check /var/lib/archbuild/extra-riscv64/felix13/build receiving incremental file list coq-8.16.1-1-riscv64-build.log sent 43 bytes received 22,381 bytes 44,848.00 bytes/sec total size is 202,994 speedup is 9.05