Go to:
Gentoo Home
Documentation
Forums
Lists
Bugs
Planet
Store
Wiki
Get Gentoo!
Gentoo's Bugzilla – Attachment 782702 Details for
Bug 849638
sci-mathematics/coq-8.15.2 - Error: No rule found for topbin/coqc_bin.exe
Home
|
New
–
[Ex]
|
Browse
|
Search
|
Privacy Policy
|
[?]
|
Reports
|
Requests
|
Help
|
New Account
|
Log In
[x]
|
Forgot Password
Login:
[x]
sci-mathematics:coq-8.15.2:20220604-011345.log
sci-mathematics:coq-8.15.2:20220604-011345.log (text/plain), 166.92 KB, created by
Toralf Förster
on 2022-06-04 07:15:37 UTC
(
hide
)
Description:
sci-mathematics:coq-8.15.2:20220604-011345.log
Filename:
MIME Type:
Creator:
Toralf Förster
Created:
2022-06-04 07:15:37 UTC
Size:
166.92 KB
patch
obsolete
> * Package: sci-mathematics/coq-8.15.2 > * Repository: gentoo > * Maintainer: sci-mathematics@gentoo.org > * Upstream: https://github.com/coq/coq/issues/ > * USE: abi_x86_64 amd64 elibc_glibc kernel_linux userland_GNU > * FEATURES: network-sandbox preserve-libs sandbox userpriv usersandbox > >>>> Unpacking source... >>>> Unpacking coq-8.15.2.tar.gz to /var/tmp/portage/sci-mathematics/coq-8.15.2/work >>>> Source unpacked in /var/tmp/portage/sci-mathematics/coq-8.15.2/work >>>> Preparing source in /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2 ... >>>> Source prepared. >>>> Configuring source in /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2 ... >Configure options: -prefix /usr -libdir /usr/lib64/coq -mandir /usr/share/man -docdir /usr/share/doc/coq-8.15.2 -datadir /usr/share/coq -configdir /etc/xdg/coq -with-doc no -byte-only -coqide no >You have OCaml 4.14.0. Good! >You have OCamlfind 1.9.3. Good! >You have the Zarith library 1.12 installed. Good! >CoqIde manually disabled: >=> no CoqIDE will be built. > > Architecture : Linux > Sys.os_type : Unix > OCaml version : 4.14.0 > OCaml binaries in : /usr/bin/ > OCaml library in : /usr/lib64/ocaml > CoqIDE : no > Documentation : None > Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & > Coq web site : http://coq.inria.fr/ > Bytecode VM enabled : true > Native Compiler enabled : ondemand > > Paths for true installation: > - Coq will be copied in /usr > - the Coq library will be copied in /usr/lib64/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/coq-8.15.2 > >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'. >>>> Source configured. >>>> Compiling source in /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2 ... >make -j4 STRIP=true VERBOSE=1 COQ_USE_DUNE= world >make --warn-undefined-variable --no-builtin-rules -f Makefile.build world >make[1]: Entering directory '/var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2' >mkdir -p _build_vo/default/ >mkdir -p _build_vo/default//lib/coq >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqdep >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2/_build/install/default/bin/ bin >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2/_build/install/default/bin/ _build_vo/default//bin >flock .dune.lock dune build --display=quiet --release @all-src >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2/_build/install/default/lib/coq-core/ _build_vo/default//lib/coq-core >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2/_build/install/default/lib/coqide-server/ _build_vo/default//lib/coqide-server >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2/_build/install/default/lib/stublibs/ _build_vo/default//lib/stublibs >mkdir -p _build_vo/default//lib/coq/theories/ssrmatching >mkdir -p _build_vo/default//lib/coq/theories/ssr >cp -a theories/ssrmatching/ssrmatching.v _build_vo/default//lib/coq/theories/ssrmatching/ssrmatching.v >cp -a theories/ssr/ssrunder.v _build_vo/default//lib/coq/theories/ssr/ssrunder.v >mkdir -p _build_vo/default//lib/coq/theories/ssr >cp -a theories/ssr/ssrsetoid.v _build_vo/default//lib/coq/theories/ssr/ssrsetoid.v >mkdir -p _build_vo/default//lib/coq/theories/ssr >cp -a theories/ssr/ssrfun.v _build_vo/default//lib/coq/theories/ssr/ssrfun.v >mkdir -p _build_vo/default//lib/coq/theories/ssr >cp -a theories/ssr/ssreflect.v _build_vo/default//lib/coq/theories/ssr/ssreflect.v >mkdir -p _build_vo/default//lib/coq/theories/ssr >cp -a theories/ssr/ssrclasses.v _build_vo/default//lib/coq/theories/ssr/ssrclasses.v >mkdir -p _build_vo/default//lib/coq/theories/ssr >cp -a theories/ssr/ssrbool.v _build_vo/default//lib/coq/theories/ssr/ssrbool.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/ZArithRing.v _build_vo/default//lib/coq/theories/setoid_ring/ZArithRing.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Rings_Z.v _build_vo/default//lib/coq/theories/setoid_ring/Rings_Z.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Rings_R.v _build_vo/default//lib/coq/theories/setoid_ring/Rings_R.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Rings_Q.v _build_vo/default//lib/coq/theories/setoid_ring/Rings_Q.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ring_theory.v _build_vo/default//lib/coq/theories/setoid_ring/Ring_theory.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ring_tac.v _build_vo/default//lib/coq/theories/setoid_ring/Ring_tac.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ring_polynom.v _build_vo/default//lib/coq/theories/setoid_ring/Ring_polynom.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ring_base.v _build_vo/default//lib/coq/theories/setoid_ring/Ring_base.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ring.v _build_vo/default//lib/coq/theories/setoid_ring/Ring.v >cp -a theories/setoid_ring/RealField.v _build_vo/default//lib/coq/theories/setoid_ring/RealField.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ncring_tac.v _build_vo/default//lib/coq/theories/setoid_ring/Ncring_tac.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ncring_polynom.v _build_vo/default//lib/coq/theories/setoid_ring/Ncring_polynom.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ncring_initial.v _build_vo/default//lib/coq/theories/setoid_ring/Ncring_initial.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Ncring.v _build_vo/default//lib/coq/theories/setoid_ring/Ncring.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/NArithRing.v _build_vo/default//lib/coq/theories/setoid_ring/NArithRing.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Integral_domain.v _build_vo/default//lib/coq/theories/setoid_ring/Integral_domain.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/InitialRing.v _build_vo/default//lib/coq/theories/setoid_ring/InitialRing.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Field_theory.v _build_vo/default//lib/coq/theories/setoid_ring/Field_theory.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Field_tac.v _build_vo/default//lib/coq/theories/setoid_ring/Field_tac.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Field.v _build_vo/default//lib/coq/theories/setoid_ring/Field.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/Cring.v _build_vo/default//lib/coq/theories/setoid_ring/Cring.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/BinList.v _build_vo/default//lib/coq/theories/setoid_ring/BinList.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >cp -a theories/setoid_ring/ArithRing.v _build_vo/default//lib/coq/theories/setoid_ring/ArithRing.v >cp -a theories/setoid_ring/Algebra_syntax.v _build_vo/default//lib/coq/theories/setoid_ring/Algebra_syntax.v >mkdir -p _build_vo/default//lib/coq/theories/rtauto >cp -a theories/rtauto/Rtauto.v _build_vo/default//lib/coq/theories/rtauto/Rtauto.v >mkdir -p _build_vo/default//lib/coq/theories/rtauto >cp -a theories/rtauto/Bintree.v _build_vo/default//lib/coq/theories/rtauto/Bintree.v >mkdir -p _build_vo/default//lib/coq/theories/omega >cp -a theories/omega/PreOmega.v _build_vo/default//lib/coq/theories/omega/PreOmega.v >mkdir -p _build_vo/default//lib/coq/theories/omega >cp -a theories/omega/OmegaLemmas.v _build_vo/default//lib/coq/theories/omega/OmegaLemmas.v >mkdir -p _build_vo/default//lib/coq/theories/nsatz >cp -a theories/nsatz/NsatzTactic.v _build_vo/default//lib/coq/theories/nsatz/NsatzTactic.v >mkdir -p _build_vo/default//lib/coq/theories/nsatz >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/nsatz/Nsatz.v _build_vo/default//lib/coq/theories/nsatz/Nsatz.v >cp -a theories/micromega/Ztac.v _build_vo/default//lib/coq/theories/micromega/Ztac.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyUint63.v _build_vo/default//lib/coq/theories/micromega/ZifyUint63.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifySint63.v _build_vo/default//lib/coq/theories/micromega/ZifySint63.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyPow.v _build_vo/default//lib/coq/theories/micromega/ZifyPow.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyNat.v _build_vo/default//lib/coq/theories/micromega/ZifyNat.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyN.v _build_vo/default//lib/coq/theories/micromega/ZifyN.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyInt63.v _build_vo/default//lib/coq/theories/micromega/ZifyInt63.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyInst.v _build_vo/default//lib/coq/theories/micromega/ZifyInst.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyComparison.v _build_vo/default//lib/coq/theories/micromega/ZifyComparison.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyClasses.v _build_vo/default//lib/coq/theories/micromega/ZifyClasses.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZifyBool.v _build_vo/default//lib/coq/theories/micromega/ZifyBool.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Zify.v _build_vo/default//lib/coq/theories/micromega/Zify.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZMicromega.v _build_vo/default//lib/coq/theories/micromega/ZMicromega.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZCoeff.v _build_vo/default//lib/coq/theories/micromega/ZCoeff.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/ZArith_hints.v _build_vo/default//lib/coq/theories/micromega/ZArith_hints.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/VarMap.v _build_vo/default//lib/coq/theories/micromega/VarMap.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Tauto.v _build_vo/default//lib/coq/theories/micromega/Tauto.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/RingMicromega.v _build_vo/default//lib/coq/theories/micromega/RingMicromega.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Refl.v _build_vo/default//lib/coq/theories/micromega/Refl.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/RMicromega.v _build_vo/default//lib/coq/theories/micromega/RMicromega.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/QMicromega.v _build_vo/default//lib/coq/theories/micromega/QMicromega.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Psatz.v _build_vo/default//lib/coq/theories/micromega/Psatz.v >cp -a theories/micromega/OrderedRing.v _build_vo/default//lib/coq/theories/micromega/OrderedRing.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/MExtraction.v _build_vo/default//lib/coq/theories/micromega/MExtraction.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Lra.v _build_vo/default//lib/coq/theories/micromega/Lra.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Lqa.v _build_vo/default//lib/coq/theories/micromega/Lqa.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Lia.v _build_vo/default//lib/coq/theories/micromega/Lia.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Fourier_util.v _build_vo/default//lib/coq/theories/micromega/Fourier_util.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Fourier.v _build_vo/default//lib/coq/theories/micromega/Fourier.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/EnvRing.v _build_vo/default//lib/coq/theories/micromega/EnvRing.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/Env.v _build_vo/default//lib/coq/theories/micromega/Env.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/DeclConstant.v _build_vo/default//lib/coq/theories/micromega/DeclConstant.v >mkdir -p _build_vo/default//lib/coq/theories/funind >mkdir -p _build_vo/default//lib/coq/theories/funind >cp -a theories/funind/Recdef.v _build_vo/default//lib/coq/theories/funind/Recdef.v >cp -a theories/funind/FunInd.v _build_vo/default//lib/coq/theories/funind/FunInd.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/Extraction.v _build_vo/default//lib/coq/theories/extraction/Extraction.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlZInt.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlZInt.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlZBigInt.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlZBigInt.v >cp -a theories/extraction/ExtrOcamlString.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlString.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlNativeString.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlNativeString.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlNatInt.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlNatInt.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlNatBigInt.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlNatBigInt.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlIntConv.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlIntConv.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlChar.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlChar.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOcamlBasic.v _build_vo/default//lib/coq/theories/extraction/ExtrOcamlBasic.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOCamlPArray.v _build_vo/default//lib/coq/theories/extraction/ExtrOCamlPArray.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOCamlInt63.v _build_vo/default//lib/coq/theories/extraction/ExtrOCamlInt63.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrOCamlFloats.v _build_vo/default//lib/coq/theories/extraction/ExtrOCamlFloats.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellZNum.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellZNum.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellZInteger.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellZInteger.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellZInt.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellZInt.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellString.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellString.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellNatNum.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellNatNum.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellNatInteger.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellNatInteger.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellNatInt.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellNatInt.v >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellBasic.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellBasic.v >mkdir -p _build_vo/default//lib/coq/theories/derive >cp -a theories/derive/Derive.v _build_vo/default//lib/coq/theories/derive/Derive.v >mkdir -p _build_vo/default//lib/coq/theories/btauto >cp -a theories/btauto/Reflect.v _build_vo/default//lib/coq/theories/btauto/Reflect.v >mkdir -p _build_vo/default//lib/coq/theories/btauto >cp -a theories/btauto/Btauto.v _build_vo/default//lib/coq/theories/btauto/Btauto.v >mkdir -p _build_vo/default//lib/coq/theories/btauto >cp -a theories/btauto/Algebra.v _build_vo/default//lib/coq/theories/btauto/Algebra.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/auxiliary.v _build_vo/default//lib/coq/theories/ZArith/auxiliary.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zwf.v _build_vo/default//lib/coq/theories/ZArith/Zwf.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zquot.v _build_vo/default//lib/coq/theories/ZArith/Zquot.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zpower.v _build_vo/default//lib/coq/theories/ZArith/Zpower.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zpow_facts.v _build_vo/default//lib/coq/theories/ZArith/Zpow_facts.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zpow_def.v _build_vo/default//lib/coq/theories/ZArith/Zpow_def.v >cp -a theories/ZArith/Zpow_alt.v _build_vo/default//lib/coq/theories/ZArith/Zpow_alt.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zorder.v _build_vo/default//lib/coq/theories/ZArith/Zorder.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Znumtheory.v _build_vo/default//lib/coq/theories/ZArith/Znumtheory.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Znat.v _build_vo/default//lib/coq/theories/ZArith/Znat.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zmisc.v _build_vo/default//lib/coq/theories/ZArith/Zmisc.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zminmax.v _build_vo/default//lib/coq/theories/ZArith/Zminmax.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zmin.v _build_vo/default//lib/coq/theories/ZArith/Zmin.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zmax.v _build_vo/default//lib/coq/theories/ZArith/Zmax.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zhints.v _build_vo/default//lib/coq/theories/ZArith/Zhints.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zgcd_alt.v _build_vo/default//lib/coq/theories/ZArith/Zgcd_alt.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zeven.v _build_vo/default//lib/coq/theories/ZArith/Zeven.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zeuclid.v _build_vo/default//lib/coq/theories/ZArith/Zeuclid.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zdiv.v _build_vo/default//lib/coq/theories/ZArith/Zdiv.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zdigits.v _build_vo/default//lib/coq/theories/ZArith/Zdigits.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zcomplements.v _build_vo/default//lib/coq/theories/ZArith/Zcomplements.v >cp -a theories/ZArith/Zcompare.v _build_vo/default//lib/coq/theories/ZArith/Zcompare.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zbool.v _build_vo/default//lib/coq/theories/ZArith/Zbool.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zabs.v _build_vo/default//lib/coq/theories/ZArith/Zabs.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/ZArith_dec.v _build_vo/default//lib/coq/theories/ZArith/ZArith_dec.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/ZArith_base.v _build_vo/default//lib/coq/theories/ZArith/ZArith_base.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/ZArith.v _build_vo/default//lib/coq/theories/ZArith/ZArith.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Wf_Z.v _build_vo/default//lib/coq/theories/ZArith/Wf_Z.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Int.v _build_vo/default//lib/coq/theories/ZArith/Int.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/BinIntDef.v _build_vo/default//lib/coq/theories/ZArith/BinIntDef.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/ZArith/BinInt.v _build_vo/default//lib/coq/theories/ZArith/BinInt.v >cp -a theories/Wellfounded/Wellfounded.v _build_vo/default//lib/coq/theories/Wellfounded/Wellfounded.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/Wellfounded/Well_Ordering.v _build_vo/default//lib/coq/theories/Wellfounded/Well_Ordering.v >cp -a theories/Wellfounded/Union.v _build_vo/default//lib/coq/theories/Wellfounded/Union.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/Wellfounded/Transitive_Closure.v _build_vo/default//lib/coq/theories/Wellfounded/Transitive_Closure.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/Wellfounded/Lexicographic_Product.v _build_vo/default//lib/coq/theories/Wellfounded/Lexicographic_Product.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/Wellfounded/Lexicographic_Exponentiation.v _build_vo/default//lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/Wellfounded/Inverse_Image.v _build_vo/default//lib/coq/theories/Wellfounded/Inverse_Image.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/Wellfounded/Inclusion.v _build_vo/default//lib/coq/theories/Wellfounded/Inclusion.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >cp -a theories/Wellfounded/Disjoint_Union.v _build_vo/default//lib/coq/theories/Wellfounded/Disjoint_Union.v >mkdir -p _build_vo/default//lib/coq/theories/Vectors >cp -a theories/Vectors/VectorSpec.v _build_vo/default//lib/coq/theories/Vectors/VectorSpec.v >mkdir -p _build_vo/default//lib/coq/theories/Vectors >cp -a theories/Vectors/VectorEq.v _build_vo/default//lib/coq/theories/Vectors/VectorEq.v >mkdir -p _build_vo/default//lib/coq/theories/Vectors >mkdir -p _build_vo/default//lib/coq/theories/Vectors >cp -a theories/Vectors/VectorDef.v _build_vo/default//lib/coq/theories/Vectors/VectorDef.v >cp -a theories/Vectors/Vector.v _build_vo/default//lib/coq/theories/Vectors/Vector.v >mkdir -p _build_vo/default//lib/coq/theories/Vectors >cp -a theories/Vectors/Fin.v _build_vo/default//lib/coq/theories/Vectors/Fin.v >mkdir -p _build_vo/default//lib/coq/theories/Unicode >cp -a theories/Unicode/Utf8_core.v _build_vo/default//lib/coq/theories/Unicode/Utf8_core.v >mkdir -p _build_vo/default//lib/coq/theories/Unicode >cp -a theories/Unicode/Utf8.v _build_vo/default//lib/coq/theories/Unicode/Utf8.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/OrdersTac.v _build_vo/default//lib/coq/theories/Structures/OrdersTac.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/OrdersLists.v _build_vo/default//lib/coq/theories/Structures/OrdersLists.v >cp -a theories/Structures/OrdersFacts.v _build_vo/default//lib/coq/theories/Structures/OrdersFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/OrdersEx.v _build_vo/default//lib/coq/theories/Structures/OrdersEx.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/OrdersAlt.v _build_vo/default//lib/coq/theories/Structures/OrdersAlt.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/Orders.v _build_vo/default//lib/coq/theories/Structures/Orders.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/OrderedTypeEx.v _build_vo/default//lib/coq/theories/Structures/OrderedTypeEx.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/OrderedTypeAlt.v _build_vo/default//lib/coq/theories/Structures/OrderedTypeAlt.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/OrderedType.v _build_vo/default//lib/coq/theories/Structures/OrderedType.v >cp -a theories/Structures/GenericMinMax.v _build_vo/default//lib/coq/theories/Structures/GenericMinMax.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/EqualitiesFacts.v _build_vo/default//lib/coq/theories/Structures/EqualitiesFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/Equalities.v _build_vo/default//lib/coq/theories/Structures/Equalities.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/DecidableTypeEx.v _build_vo/default//lib/coq/theories/Structures/DecidableTypeEx.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/DecidableType.v _build_vo/default//lib/coq/theories/Structures/DecidableType.v >mkdir -p _build_vo/default//lib/coq/theories/Strings >cp -a theories/Strings/String.v _build_vo/default//lib/coq/theories/Strings/String.v >mkdir -p _build_vo/default//lib/coq/theories/Strings >cp -a theories/Strings/OctalString.v _build_vo/default//lib/coq/theories/Strings/OctalString.v >mkdir -p _build_vo/default//lib/coq/theories/Strings >mkdir -p _build_vo/default//lib/coq/theories/Strings >cp -a theories/Strings/HexString.v _build_vo/default//lib/coq/theories/Strings/HexString.v >cp -a theories/Strings/ByteVector.v _build_vo/default//lib/coq/theories/Strings/ByteVector.v >mkdir -p _build_vo/default//lib/coq/theories/Strings >cp -a theories/Strings/Byte.v _build_vo/default//lib/coq/theories/Strings/Byte.v >mkdir -p _build_vo/default//lib/coq/theories/Strings >cp -a theories/Strings/BinaryString.v _build_vo/default//lib/coq/theories/Strings/BinaryString.v >mkdir -p _build_vo/default//lib/coq/theories/Strings >cp -a theories/Strings/Ascii.v _build_vo/default//lib/coq/theories/Strings/Ascii.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/Sorting.v _build_vo/default//lib/coq/theories/Sorting/Sorting.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/Sorted.v _build_vo/default//lib/coq/theories/Sorting/Sorted.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/Permutation.v _build_vo/default//lib/coq/theories/Sorting/Permutation.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/PermutSetoid.v _build_vo/default//lib/coq/theories/Sorting/PermutSetoid.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/PermutEq.v _build_vo/default//lib/coq/theories/Sorting/PermutEq.v >cp -a theories/Sorting/Mergesort.v _build_vo/default//lib/coq/theories/Sorting/Mergesort.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/Heap.v _build_vo/default//lib/coq/theories/Sorting/Heap.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/CPermutation.v _build_vo/default//lib/coq/theories/Sorting/CPermutation.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Uniset.v _build_vo/default//lib/coq/theories/Sets/Uniset.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Relations_3_facts.v _build_vo/default//lib/coq/theories/Sets/Relations_3_facts.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Relations_3.v _build_vo/default//lib/coq/theories/Sets/Relations_3.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Relations_2_facts.v _build_vo/default//lib/coq/theories/Sets/Relations_2_facts.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Relations_2.v _build_vo/default//lib/coq/theories/Sets/Relations_2.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Relations_1_facts.v _build_vo/default//lib/coq/theories/Sets/Relations_1_facts.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Relations_1.v _build_vo/default//lib/coq/theories/Sets/Relations_1.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Powerset_facts.v _build_vo/default//lib/coq/theories/Sets/Powerset_facts.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Powerset_Classical_facts.v _build_vo/default//lib/coq/theories/Sets/Powerset_Classical_facts.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Powerset.v _build_vo/default//lib/coq/theories/Sets/Powerset.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Permut.v _build_vo/default//lib/coq/theories/Sets/Permut.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Partial_Order.v _build_vo/default//lib/coq/theories/Sets/Partial_Order.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Multiset.v _build_vo/default//lib/coq/theories/Sets/Multiset.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Integers.v _build_vo/default//lib/coq/theories/Sets/Integers.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Infinite_sets.v _build_vo/default//lib/coq/theories/Sets/Infinite_sets.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Image.v _build_vo/default//lib/coq/theories/Sets/Image.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Finite_sets_facts.v _build_vo/default//lib/coq/theories/Sets/Finite_sets_facts.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Finite_sets.v _build_vo/default//lib/coq/theories/Sets/Finite_sets.v >cp -a theories/Sets/Ensembles.v _build_vo/default//lib/coq/theories/Sets/Ensembles.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Cpo.v _build_vo/default//lib/coq/theories/Sets/Cpo.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Constructive_sets.v _build_vo/default//lib/coq/theories/Sets/Constructive_sets.v >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Classical_sets.v _build_vo/default//lib/coq/theories/Sets/Classical_sets.v >mkdir -p _build_vo/default//lib/coq/theories/Setoids >cp -a theories/Setoids/Setoid.v _build_vo/default//lib/coq/theories/Setoids/Setoid.v >mkdir -p _build_vo/default//lib/coq/theories/Relations >cp -a theories/Relations/Relations.v _build_vo/default//lib/coq/theories/Relations/Relations.v >mkdir -p _build_vo/default//lib/coq/theories/Relations >mkdir -p _build_vo/default//lib/coq/theories/Relations >cp -a theories/Relations/Relation_Operators.v _build_vo/default//lib/coq/theories/Relations/Relation_Operators.v >cp -a theories/Relations/Relation_Definitions.v _build_vo/default//lib/coq/theories/Relations/Relation_Definitions.v >mkdir -p _build_vo/default//lib/coq/theories/Relations >cp -a theories/Relations/Operators_Properties.v _build_vo/default//lib/coq/theories/Relations/Operators_Properties.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Sqrt_reg.v _build_vo/default//lib/coq/theories/Reals/Sqrt_reg.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/SplitRmult.v _build_vo/default//lib/coq/theories/Reals/SplitRmult.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/SplitAbsolu.v _build_vo/default//lib/coq/theories/Reals/SplitAbsolu.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/SeqSeries.v _build_vo/default//lib/coq/theories/Reals/SeqSeries.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/SeqProp.v _build_vo/default//lib/coq/theories/Reals/SeqProp.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Runcountable.v _build_vo/default//lib/coq/theories/Reals/Runcountable.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rtrigo_reg.v _build_vo/default//lib/coq/theories/Reals/Rtrigo_reg.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rtrigo_fun.v _build_vo/default//lib/coq/theories/Reals/Rtrigo_fun.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rtrigo_facts.v _build_vo/default//lib/coq/theories/Reals/Rtrigo_facts.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rtrigo_def.v _build_vo/default//lib/coq/theories/Reals/Rtrigo_def.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rtrigo_calc.v _build_vo/default//lib/coq/theories/Reals/Rtrigo_calc.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rtrigo_alt.v _build_vo/default//lib/coq/theories/Reals/Rtrigo_alt.v >cp -a theories/Reals/Rtrigo1.v _build_vo/default//lib/coq/theories/Reals/Rtrigo1.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rtrigo.v _build_vo/default//lib/coq/theories/Reals/Rtrigo.v >cp -a theories/Reals/Rtopology.v _build_vo/default//lib/coq/theories/Reals/Rtopology.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rsqrt_def.v _build_vo/default//lib/coq/theories/Reals/Rsqrt_def.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rsigma.v _build_vo/default//lib/coq/theories/Reals/Rsigma.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rseries.v _build_vo/default//lib/coq/theories/Reals/Rseries.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rregisternames.v _build_vo/default//lib/coq/theories/Reals/Rregisternames.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rprod.v _build_vo/default//lib/coq/theories/Reals/Rprod.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rpower.v _build_vo/default//lib/coq/theories/Reals/Rpower.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rpow_def.v _build_vo/default//lib/coq/theories/Reals/Rpow_def.v >cp -a theories/Reals/Rminmax.v _build_vo/default//lib/coq/theories/Reals/Rminmax.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rlogic.v _build_vo/default//lib/coq/theories/Reals/Rlogic.v >cp -a theories/Reals/Rlimit.v _build_vo/default//lib/coq/theories/Reals/Rlimit.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/RiemannInt_SF.v _build_vo/default//lib/coq/theories/Reals/RiemannInt_SF.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/RiemannInt.v _build_vo/default//lib/coq/theories/Reals/RiemannInt.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rgeom.v _build_vo/default//lib/coq/theories/Reals/Rgeom.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rfunctions.v _build_vo/default//lib/coq/theories/Reals/Rfunctions.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Reals.v _build_vo/default//lib/coq/theories/Reals/Reals.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rderiv.v _build_vo/default//lib/coq/theories/Reals/Rderiv.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rdefinitions.v _build_vo/default//lib/coq/theories/Reals/Rdefinitions.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rcomplete.v _build_vo/default//lib/coq/theories/Reals/Rcomplete.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rbasic_fun.v _build_vo/default//lib/coq/theories/Reals/Rbasic_fun.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rbase.v _build_vo/default//lib/coq/theories/Reals/Rbase.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Raxioms.v _build_vo/default//lib/coq/theories/Reals/Raxioms.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ratan.v _build_vo/default//lib/coq/theories/Reals/Ratan.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ranalysis_reg.v _build_vo/default//lib/coq/theories/Reals/Ranalysis_reg.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ranalysis5.v _build_vo/default//lib/coq/theories/Reals/Ranalysis5.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ranalysis4.v _build_vo/default//lib/coq/theories/Reals/Ranalysis4.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ranalysis3.v _build_vo/default//lib/coq/theories/Reals/Ranalysis3.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ranalysis2.v _build_vo/default//lib/coq/theories/Reals/Ranalysis2.v >cp -a theories/Reals/Ranalysis1.v _build_vo/default//lib/coq/theories/Reals/Ranalysis1.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ranalysis.v _build_vo/default//lib/coq/theories/Reals/Ranalysis.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/R_sqrt.v _build_vo/default//lib/coq/theories/Reals/R_sqrt.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/R_sqr.v _build_vo/default//lib/coq/theories/Reals/R_sqr.v >cp -a theories/Reals/R_Ifp.v _build_vo/default//lib/coq/theories/Reals/R_Ifp.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/ROrderedType.v _build_vo/default//lib/coq/theories/Reals/ROrderedType.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/RList.v _build_vo/default//lib/coq/theories/Reals/RList.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/RIneq.v _build_vo/default//lib/coq/theories/Reals/RIneq.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/PartSum.v _build_vo/default//lib/coq/theories/Reals/PartSum.v >cp -a theories/Reals/PSeries_reg.v _build_vo/default//lib/coq/theories/Reals/PSeries_reg.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/NewtonInt.v _build_vo/default//lib/coq/theories/Reals/NewtonInt.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Machin.v _build_vo/default//lib/coq/theories/Reals/Machin.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/MVT.v _build_vo/default//lib/coq/theories/Reals/MVT.v >cp -a theories/Reals/Integration.v _build_vo/default//lib/coq/theories/Reals/Integration.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Exp_prop.v _build_vo/default//lib/coq/theories/Reals/Exp_prop.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/DiscrR.v _build_vo/default//lib/coq/theories/Reals/DiscrR.v >cp -a theories/Reals/Cos_rel.v _build_vo/default//lib/coq/theories/Reals/Cos_rel.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Cos_plus.v _build_vo/default//lib/coq/theories/Reals/Cos_plus.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/ClassicalDedekindReals.v _build_vo/default//lib/coq/theories/Reals/ClassicalDedekindReals.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/ClassicalConstructiveReals.v _build_vo/default//lib/coq/theories/Reals/ClassicalConstructiveReals.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Cauchy_prod.v _build_vo/default//lib/coq/theories/Reals/Cauchy_prod.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Cauchy >cp -a theories/Reals/Cauchy/QExtra.v _build_vo/default//lib/coq/theories/Reals/Cauchy/QExtra.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Cauchy >cp -a theories/Reals/Cauchy/PosExtra.v _build_vo/default//lib/coq/theories/Reals/Cauchy/PosExtra.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Cauchy >cp -a theories/Reals/Cauchy/ConstructiveRcomplete.v _build_vo/default//lib/coq/theories/Reals/Cauchy/ConstructiveRcomplete.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Cauchy >mkdir -p _build_vo/default//lib/coq/theories/Reals/Cauchy >cp -a theories/Reals/Cauchy/ConstructiveExtra.v _build_vo/default//lib/coq/theories/Reals/Cauchy/ConstructiveExtra.v >cp -a theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v _build_vo/default//lib/coq/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Cauchy >cp -a theories/Reals/Cauchy/ConstructiveCauchyReals.v _build_vo/default//lib/coq/theories/Reals/Cauchy/ConstructiveCauchyReals.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Cauchy >cp -a theories/Reals/Cauchy/ConstructiveCauchyAbs.v _build_vo/default//lib/coq/theories/Reals/Cauchy/ConstructiveCauchyAbs.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Binomial.v _build_vo/default//lib/coq/theories/Reals/Binomial.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/ArithProp.v _build_vo/default//lib/coq/theories/Reals/ArithProp.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/AltSeries.v _build_vo/default//lib/coq/theories/Reals/AltSeries.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >cp -a theories/Reals/Alembert.v _build_vo/default//lib/coq/theories/Reals/Alembert.v >cp -a theories/Reals/Abstract/ConstructiveSum.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveSum.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >cp -a theories/Reals/Abstract/ConstructiveRealsMorphisms.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveRealsMorphisms.v >cp -a theories/Reals/Abstract/ConstructiveReals.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveReals.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >cp -a theories/Reals/Abstract/ConstructivePower.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructivePower.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >cp -a theories/Reals/Abstract/ConstructiveMinMax.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveMinMax.v >cp -a theories/Reals/Abstract/ConstructiveLimits.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveLimits.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >cp -a theories/Reals/Abstract/ConstructiveLUB.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveLUB.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >cp -a theories/Reals/Abstract/ConstructiveAbs.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveAbs.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qround.v _build_vo/default//lib/coq/theories/QArith/Qround.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qring.v _build_vo/default//lib/coq/theories/QArith/Qring.v >cp -a theories/QArith/Qreduction.v _build_vo/default//lib/coq/theories/QArith/Qreduction.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qreals.v _build_vo/default//lib/coq/theories/QArith/Qreals.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qpower.v _build_vo/default//lib/coq/theories/QArith/Qpower.v >cp -a theories/QArith/Qminmax.v _build_vo/default//lib/coq/theories/QArith/Qminmax.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qfield.v _build_vo/default//lib/coq/theories/QArith/Qfield.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qcanon.v _build_vo/default//lib/coq/theories/QArith/Qcanon.v >cp -a theories/QArith/Qcabs.v _build_vo/default//lib/coq/theories/QArith/Qcabs.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qabs.v _build_vo/default//lib/coq/theories/QArith/Qabs.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/QOrderedType.v _build_vo/default//lib/coq/theories/QArith/QOrderedType.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/QArith_base.v _build_vo/default//lib/coq/theories/QArith/QArith_base.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/QArith.v _build_vo/default//lib/coq/theories/QArith/QArith.v >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Wf.v _build_vo/default//lib/coq/theories/Program/Wf.v >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Utils.v _build_vo/default//lib/coq/theories/Program/Utils.v >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Tactics.v _build_vo/default//lib/coq/theories/Program/Tactics.v >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Syntax.v _build_vo/default//lib/coq/theories/Program/Syntax.v >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Subset.v _build_vo/default//lib/coq/theories/Program/Subset.v >mkdir -p _build_vo/default//lib/coq/theories/Program >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Program.v _build_vo/default//lib/coq/theories/Program/Program.v >cp -a theories/Program/Equality.v _build_vo/default//lib/coq/theories/Program/Equality.v >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Combinators.v _build_vo/default//lib/coq/theories/Program/Combinators.v >mkdir -p _build_vo/default//lib/coq/theories/Program >cp -a theories/Program/Basics.v _build_vo/default//lib/coq/theories/Program/Basics.v >mkdir -p _build_vo/default//lib/coq/theories/PArith >mkdir -p _build_vo/default//lib/coq/theories/PArith >cp -a theories/PArith/Pnat.v _build_vo/default//lib/coq/theories/PArith/Pnat.v >cp -a theories/PArith/POrderedType.v _build_vo/default//lib/coq/theories/PArith/POrderedType.v >mkdir -p _build_vo/default//lib/coq/theories/PArith >cp -a theories/PArith/PArith.v _build_vo/default//lib/coq/theories/PArith/PArith.v >mkdir -p _build_vo/default//lib/coq/theories/PArith >cp -a theories/PArith/BinPosDef.v _build_vo/default//lib/coq/theories/PArith/BinPosDef.v >mkdir -p _build_vo/default//lib/coq/theories/PArith >cp -a theories/PArith/BinPos.v _build_vo/default//lib/coq/theories/PArith/BinPos.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/NumPrelude.v _build_vo/default//lib/coq/theories/Numbers/NumPrelude.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Peano >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Binary >cp -a theories/Numbers/Natural/Peano/NPeano.v _build_vo/default//lib/coq/theories/Numbers/Natural/Peano/NPeano.v >cp -a theories/Numbers/Natural/Binary/NBinary.v _build_vo/default//lib/coq/theories/Numbers/Natural/Binary/NBinary.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NSub.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NSub.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NStrongRec.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NStrongRec.v >cp -a theories/Numbers/Natural/Abstract/NSqrt.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NSqrt.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NProperties.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NProperties.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NPow.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NPow.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NParity.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NParity.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NOrder.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NMulOrder.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NMulOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NMaxMin.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NMaxMin.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NLog.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NLog.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NLcm.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NLcm.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NIso.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NIso.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NGcd.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NGcd.v >cp -a theories/Numbers/Natural/Abstract/NDiv.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NDiv.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NDefOps.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NDefOps.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NBits.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NBits.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NBase.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NBase.v >cp -a theories/Numbers/Natural/Abstract/NAxioms.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NAxioms.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >cp -a theories/Numbers/Natural/Abstract/NAddOrder.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NAddOrder.v >cp -a theories/Numbers/Natural/Abstract/NAdd.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NAdd.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZSqrt.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZSqrt.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZProperties.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZProperties.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZPow.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZPow.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZParity.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZParity.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZOrder.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZMulOrder.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZMulOrder.v >cp -a theories/Numbers/NatInt/NZMul.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZMul.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZLog.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZLog.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZGcd.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZGcd.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZDomain.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZDomain.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZDiv.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZDiv.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZBits.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZBits.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZBase.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZBase.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZAxioms.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZAxioms.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZAddOrder.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZAddOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/NatInt >cp -a theories/Numbers/NatInt/NZAdd.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZAdd.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/NatPairs >cp -a theories/Numbers/NaryFunctions.v _build_vo/default//lib/coq/theories/Numbers/NaryFunctions.v >cp -a theories/Numbers/Integer/NatPairs/ZNatPairs.v _build_vo/default//lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Binary >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Binary/ZBinary.v _build_vo/default//lib/coq/theories/Numbers/Integer/Binary/ZBinary.v >cp -a theories/Numbers/Integer/Abstract/ZSgnAbs.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZProperties.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZProperties.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZPow.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZPow.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZParity.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZParity.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZMulOrder.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZMul.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZMul.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZMaxMin.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZMaxMin.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZLt.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZLt.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZLcm.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZLcm.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZGcd.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZGcd.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZDivTrunc.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.v >cp -a theories/Numbers/Integer/Abstract/ZDivFloor.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZDivFloor.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZDivEucl.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZDivEucl.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZBits.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZBits.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZBase.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZBase.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZAxioms.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZAxioms.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZAddOrder.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZAddOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract >cp -a theories/Numbers/Integer/Abstract/ZAdd.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZAdd.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalZ.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalZ.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalString.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalString.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalR.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalR.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalQ.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalQ.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalPos.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalPos.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalNat.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalNat.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalN.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalN.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/HexadecimalFacts.v _build_vo/default//lib/coq/theories/Numbers/HexadecimalFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalZ.v _build_vo/default//lib/coq/theories/Numbers/DecimalZ.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalString.v _build_vo/default//lib/coq/theories/Numbers/DecimalString.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalR.v _build_vo/default//lib/coq/theories/Numbers/DecimalR.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalQ.v _build_vo/default//lib/coq/theories/Numbers/DecimalQ.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalPos.v _build_vo/default//lib/coq/theories/Numbers/DecimalPos.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalNat.v _build_vo/default//lib/coq/theories/Numbers/DecimalNat.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalN.v _build_vo/default//lib/coq/theories/Numbers/DecimalN.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/DecimalFacts.v _build_vo/default//lib/coq/theories/Numbers/DecimalFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/ZModulo >cp -a theories/Numbers/Cyclic/ZModulo/ZModulo.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63 >cp -a theories/Numbers/Cyclic/Int63/Uint63.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63/Uint63.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63 >cp -a theories/Numbers/Cyclic/Int63/Sint63.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63/Sint63.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63 >cp -a theories/Numbers/Cyclic/Int63/Ring63.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63/Ring63.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63 >cp -a theories/Numbers/Cyclic/Int63/PrimInt63.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63/PrimInt63.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63 >cp -a theories/Numbers/Cyclic/Int63/Int63.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63/Int63.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63 >cp -a theories/Numbers/Cyclic/Int63/Cyclic63.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int63/Cyclic63.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int31 >cp -a theories/Numbers/Cyclic/Int31/Ring31.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int31/Ring31.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int31 >cp -a theories/Numbers/Cyclic/Int31/Int31.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int31/Int31.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int31 >cp -a theories/Numbers/Cyclic/Int31/Cyclic31.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Int31/Cyclic31.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract >cp -a theories/Numbers/Cyclic/Abstract/NZCyclic.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract >cp -a theories/Numbers/Cyclic/Abstract/DoubleType.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract/DoubleType.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract >cp -a theories/Numbers/Cyclic/Abstract/CyclicAxioms.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/Cyclic/Abstract/CarryType.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract/CarryType.v >cp -a theories/Numbers/BinNums.v _build_vo/default//lib/coq/theories/Numbers/BinNums.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/Numbers/AltBinNotations.v _build_vo/default//lib/coq/theories/Numbers/AltBinNotations.v >cp -a theories/NArith/Nsqrt_def.v _build_vo/default//lib/coq/theories/NArith/Nsqrt_def.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/Nnat.v _build_vo/default//lib/coq/theories/NArith/Nnat.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/Ngcd_def.v _build_vo/default//lib/coq/theories/NArith/Ngcd_def.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/Ndiv_def.v _build_vo/default//lib/coq/theories/NArith/Ndiv_def.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/Ndist.v _build_vo/default//lib/coq/theories/NArith/Ndist.v >cp -a theories/NArith/Ndigits.v _build_vo/default//lib/coq/theories/NArith/Ndigits.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/Ndec.v _build_vo/default//lib/coq/theories/NArith/Ndec.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/NArith.v _build_vo/default//lib/coq/theories/NArith/NArith.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/BinNatDef.v _build_vo/default//lib/coq/theories/NArith/BinNatDef.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >cp -a theories/NArith/BinNat.v _build_vo/default//lib/coq/theories/NArith/BinNat.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSets.v _build_vo/default//lib/coq/theories/MSets/MSets.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetWeakList.v _build_vo/default//lib/coq/theories/MSets/MSetWeakList.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetToFiniteSet.v _build_vo/default//lib/coq/theories/MSets/MSetToFiniteSet.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetRBT.v _build_vo/default//lib/coq/theories/MSets/MSetRBT.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetProperties.v _build_vo/default//lib/coq/theories/MSets/MSetProperties.v >cp -a theories/MSets/MSetPositive.v _build_vo/default//lib/coq/theories/MSets/MSetPositive.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetList.v _build_vo/default//lib/coq/theories/MSets/MSetList.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetInterface.v _build_vo/default//lib/coq/theories/MSets/MSetInterface.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetGenTree.v _build_vo/default//lib/coq/theories/MSets/MSetGenTree.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetFacts.v _build_vo/default//lib/coq/theories/MSets/MSetFacts.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetEqProperties.v _build_vo/default//lib/coq/theories/MSets/MSetEqProperties.v >cp -a theories/MSets/MSetDecide.v _build_vo/default//lib/coq/theories/MSets/MSetDecide.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >cp -a theories/MSets/MSetAVL.v _build_vo/default//lib/coq/theories/MSets/MSetAVL.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/WeakFan.v _build_vo/default//lib/coq/theories/Logic/WeakFan.v >cp -a theories/Logic/WKL.v _build_vo/default//lib/coq/theories/Logic/WKL.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/StrictProp.v _build_vo/default//lib/coq/theories/Logic/StrictProp.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/SetoidChoice.v _build_vo/default//lib/coq/theories/Logic/SetoidChoice.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/SetIsType.v _build_vo/default//lib/coq/theories/Logic/SetIsType.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/RelationalChoice.v _build_vo/default//lib/coq/theories/Logic/RelationalChoice.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/PropFacts.v _build_vo/default//lib/coq/theories/Logic/PropFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/PropExtensionalityFacts.v _build_vo/default//lib/coq/theories/Logic/PropExtensionalityFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/PropExtensionality.v _build_vo/default//lib/coq/theories/Logic/PropExtensionality.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ProofIrrelevanceFacts.v _build_vo/default//lib/coq/theories/Logic/ProofIrrelevanceFacts.v >cp -a theories/Logic/ProofIrrelevance.v _build_vo/default//lib/coq/theories/Logic/ProofIrrelevance.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/JMeq.v _build_vo/default//lib/coq/theories/Logic/JMeq.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/IndefiniteDescription.v _build_vo/default//lib/coq/theories/Logic/IndefiniteDescription.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Hurkens.v _build_vo/default//lib/coq/theories/Logic/Hurkens.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/HLevels.v _build_vo/default//lib/coq/theories/Logic/HLevels.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/FunctionalExtensionality.v _build_vo/default//lib/coq/theories/Logic/FunctionalExtensionality.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/FinFun.v _build_vo/default//lib/coq/theories/Logic/FinFun.v >cp -a theories/Logic/ExtensionalityFacts.v _build_vo/default//lib/coq/theories/Logic/ExtensionalityFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ExtensionalFunctionRepresentative.v _build_vo/default//lib/coq/theories/Logic/ExtensionalFunctionRepresentative.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Eqdep_dec.v _build_vo/default//lib/coq/theories/Logic/Eqdep_dec.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/EqdepFacts.v _build_vo/default//lib/coq/theories/Logic/EqdepFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Eqdep.v _build_vo/default//lib/coq/theories/Logic/Eqdep.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Epsilon.v _build_vo/default//lib/coq/theories/Logic/Epsilon.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Diaconescu.v _build_vo/default//lib/coq/theories/Logic/Diaconescu.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Description.v _build_vo/default//lib/coq/theories/Logic/Description.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Decidable.v _build_vo/default//lib/coq/theories/Logic/Decidable.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ConstructiveEpsilon.v _build_vo/default//lib/coq/theories/Logic/ConstructiveEpsilon.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Classical_Prop.v _build_vo/default//lib/coq/theories/Logic/Classical_Prop.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Classical_Pred_Type.v _build_vo/default//lib/coq/theories/Logic/Classical_Pred_Type.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ClassicalUniqueChoice.v _build_vo/default//lib/coq/theories/Logic/ClassicalUniqueChoice.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ClassicalFacts.v _build_vo/default//lib/coq/theories/Logic/ClassicalFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ClassicalEpsilon.v _build_vo/default//lib/coq/theories/Logic/ClassicalEpsilon.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ClassicalDescription.v _build_vo/default//lib/coq/theories/Logic/ClassicalDescription.v >cp -a theories/Logic/ClassicalChoice.v _build_vo/default//lib/coq/theories/Logic/ClassicalChoice.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Classical.v _build_vo/default//lib/coq/theories/Logic/Classical.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/ChoiceFacts.v _build_vo/default//lib/coq/theories/Logic/ChoiceFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Berardi.v _build_vo/default//lib/coq/theories/Logic/Berardi.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Adjointification.v _build_vo/default//lib/coq/theories/Logic/Adjointification.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/Streams.v _build_vo/default//lib/coq/theories/Lists/Streams.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/StreamMemo.v _build_vo/default//lib/coq/theories/Lists/StreamMemo.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/SetoidPermutation.v _build_vo/default//lib/coq/theories/Lists/SetoidPermutation.v >cp -a theories/Lists/SetoidList.v _build_vo/default//lib/coq/theories/Lists/SetoidList.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/ListTactics.v _build_vo/default//lib/coq/theories/Lists/ListTactics.v >cp -a theories/Lists/ListSet.v _build_vo/default//lib/coq/theories/Lists/ListSet.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/ListDec.v _build_vo/default//lib/coq/theories/Lists/ListDec.v >cp -a theories/Lists/List.v _build_vo/default//lib/coq/theories/Lists/List.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Wf.v _build_vo/default//lib/coq/theories/Init/Wf.v >mkdir -p _build_vo/default//lib/coq/theories/Init >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Tauto.v _build_vo/default//lib/coq/theories/Init/Tauto.v >cp -a theories/Init/Tactics.v _build_vo/default//lib/coq/theories/Init/Tactics.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Specif.v _build_vo/default//lib/coq/theories/Init/Specif.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Prelude.v _build_vo/default//lib/coq/theories/Init/Prelude.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Peano.v _build_vo/default//lib/coq/theories/Init/Peano.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Number.v _build_vo/default//lib/coq/theories/Init/Number.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Notations.v _build_vo/default//lib/coq/theories/Init/Notations.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Nat.v _build_vo/default//lib/coq/theories/Init/Nat.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Ltac.v _build_vo/default//lib/coq/theories/Init/Ltac.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Logic_Type.v _build_vo/default//lib/coq/theories/Init/Logic_Type.v >mkdir -p _build_vo/default//lib/coq/theories/Init >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Logic.v _build_vo/default//lib/coq/theories/Init/Logic.v >cp -a theories/Init/Hexadecimal.v _build_vo/default//lib/coq/theories/Init/Hexadecimal.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Decimal.v _build_vo/default//lib/coq/theories/Init/Decimal.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Datatypes.v _build_vo/default//lib/coq/theories/Init/Datatypes.v >mkdir -p _build_vo/default//lib/coq/theories/Init >cp -a theories/Init/Byte.v _build_vo/default//lib/coq/theories/Init/Byte.v >mkdir -p _build_vo/default//lib/coq/theories/Floats >mkdir -p _build_vo/default//lib/coq/theories/Floats >cp -a theories/Floats/SpecFloat.v _build_vo/default//lib/coq/theories/Floats/SpecFloat.v >cp -a theories/Floats/PrimFloat.v _build_vo/default//lib/coq/theories/Floats/PrimFloat.v >mkdir -p _build_vo/default//lib/coq/theories/Floats >cp -a theories/Floats/Floats.v _build_vo/default//lib/coq/theories/Floats/Floats.v >mkdir -p _build_vo/default//lib/coq/theories/Floats >cp -a theories/Floats/FloatOps.v _build_vo/default//lib/coq/theories/Floats/FloatOps.v >mkdir -p _build_vo/default//lib/coq/theories/Floats >cp -a theories/Floats/FloatLemmas.v _build_vo/default//lib/coq/theories/Floats/FloatLemmas.v >mkdir -p _build_vo/default//lib/coq/theories/Floats >cp -a theories/Floats/FloatClass.v _build_vo/default//lib/coq/theories/Floats/FloatClass.v >mkdir -p _build_vo/default//lib/coq/theories/Floats >cp -a theories/Floats/FloatAxioms.v _build_vo/default//lib/coq/theories/Floats/FloatAxioms.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSets.v _build_vo/default//lib/coq/theories/FSets/FSets.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetWeakList.v _build_vo/default//lib/coq/theories/FSets/FSetWeakList.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetToFiniteSet.v _build_vo/default//lib/coq/theories/FSets/FSetToFiniteSet.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetProperties.v _build_vo/default//lib/coq/theories/FSets/FSetProperties.v >cp -a theories/FSets/FSetPositive.v _build_vo/default//lib/coq/theories/FSets/FSetPositive.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetList.v _build_vo/default//lib/coq/theories/FSets/FSetList.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetInterface.v _build_vo/default//lib/coq/theories/FSets/FSetInterface.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetFacts.v _build_vo/default//lib/coq/theories/FSets/FSetFacts.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetEqProperties.v _build_vo/default//lib/coq/theories/FSets/FSetEqProperties.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetDecide.v _build_vo/default//lib/coq/theories/FSets/FSetDecide.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetCompat.v _build_vo/default//lib/coq/theories/FSets/FSetCompat.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetBridge.v _build_vo/default//lib/coq/theories/FSets/FSetBridge.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FSetAVL.v _build_vo/default//lib/coq/theories/FSets/FSetAVL.v >cp -a theories/FSets/FMaps.v _build_vo/default//lib/coq/theories/FSets/FMaps.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FMapWeakList.v _build_vo/default//lib/coq/theories/FSets/FMapWeakList.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FMapPositive.v _build_vo/default//lib/coq/theories/FSets/FMapPositive.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FMapList.v _build_vo/default//lib/coq/theories/FSets/FMapList.v >cp -a theories/FSets/FMapInterface.v _build_vo/default//lib/coq/theories/FSets/FMapInterface.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FMapFullAVL.v _build_vo/default//lib/coq/theories/FSets/FMapFullAVL.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FMapFacts.v _build_vo/default//lib/coq/theories/FSets/FMapFacts.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >cp -a theories/FSets/FMapAVL.v _build_vo/default//lib/coq/theories/FSets/FMapAVL.v >mkdir -p _build_vo/default//lib/coq/theories/Compat >mkdir -p _build_vo/default//lib/coq/theories/Compat >cp -a theories/Compat/Coq815.v _build_vo/default//lib/coq/theories/Compat/Coq815.v >cp -a theories/Compat/Coq814.v _build_vo/default//lib/coq/theories/Compat/Coq814.v >mkdir -p _build_vo/default//lib/coq/theories/Compat >cp -a theories/Compat/Coq813.v _build_vo/default//lib/coq/theories/Compat/Coq813.v >mkdir -p _build_vo/default//lib/coq/theories/Compat >cp -a theories/Compat/AdmitAxiom.v _build_vo/default//lib/coq/theories/Compat/AdmitAxiom.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/SetoidTactics.v _build_vo/default//lib/coq/theories/Classes/SetoidTactics.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/SetoidDec.v _build_vo/default//lib/coq/theories/Classes/SetoidDec.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/SetoidClass.v _build_vo/default//lib/coq/theories/Classes/SetoidClass.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/RelationPairs.v _build_vo/default//lib/coq/theories/Classes/RelationPairs.v >cp -a theories/Classes/RelationClasses.v _build_vo/default//lib/coq/theories/Classes/RelationClasses.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/Morphisms_Relations.v _build_vo/default//lib/coq/theories/Classes/Morphisms_Relations.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/Morphisms_Prop.v _build_vo/default//lib/coq/theories/Classes/Morphisms_Prop.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/Morphisms.v _build_vo/default//lib/coq/theories/Classes/Morphisms.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/Init.v _build_vo/default//lib/coq/theories/Classes/Init.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/Equivalence.v _build_vo/default//lib/coq/theories/Classes/Equivalence.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/EquivDec.v _build_vo/default//lib/coq/theories/Classes/EquivDec.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/DecidableClass.v _build_vo/default//lib/coq/theories/Classes/DecidableClass.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/CRelationClasses.v _build_vo/default//lib/coq/theories/Classes/CRelationClasses.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/CMorphisms.v _build_vo/default//lib/coq/theories/Classes/CMorphisms.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/CEquivalence.v _build_vo/default//lib/coq/theories/Classes/CEquivalence.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >cp -a theories/Bool/Zerob.v _build_vo/default//lib/coq/theories/Bool/Zerob.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >cp -a theories/Bool/Sumbool.v _build_vo/default//lib/coq/theories/Bool/Sumbool.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >mkdir -p _build_vo/default//lib/coq/theories/Bool >cp -a theories/Bool/IfProp.v _build_vo/default//lib/coq/theories/Bool/IfProp.v >cp -a theories/Bool/DecBool.v _build_vo/default//lib/coq/theories/Bool/DecBool.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >cp -a theories/Bool/Bvector.v _build_vo/default//lib/coq/theories/Bool/Bvector.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >cp -a theories/Bool/BoolOrder.v _build_vo/default//lib/coq/theories/Bool/BoolOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >cp -a theories/Bool/BoolEq.v _build_vo/default//lib/coq/theories/Bool/BoolEq.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >cp -a theories/Bool/Bool.v _build_vo/default//lib/coq/theories/Bool/Bool.v >mkdir -p _build_vo/default//lib/coq/theories/Array >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Array/PArray.v _build_vo/default//lib/coq/theories/Array/PArray.v >cp -a theories/Arith/Wf_nat.v _build_vo/default//lib/coq/theories/Arith/Wf_nat.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Plus.v _build_vo/default//lib/coq/theories/Arith/Plus.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Peano_dec.v _build_vo/default//lib/coq/theories/Arith/Peano_dec.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/PeanoNat.v _build_vo/default//lib/coq/theories/Arith/PeanoNat.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Mult.v _build_vo/default//lib/coq/theories/Arith/Mult.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Minus.v _build_vo/default//lib/coq/theories/Arith/Minus.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Min.v _build_vo/default//lib/coq/theories/Arith/Min.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Max.v _build_vo/default//lib/coq/theories/Arith/Max.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Lt.v _build_vo/default//lib/coq/theories/Arith/Lt.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Le.v _build_vo/default//lib/coq/theories/Arith/Le.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Gt.v _build_vo/default//lib/coq/theories/Arith/Gt.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Factorial.v _build_vo/default//lib/coq/theories/Arith/Factorial.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Even.v _build_vo/default//lib/coq/theories/Arith/Even.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Euclid.v _build_vo/default//lib/coq/theories/Arith/Euclid.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/EqNat.v _build_vo/default//lib/coq/theories/Arith/EqNat.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Div2.v _build_vo/default//lib/coq/theories/Arith/Div2.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Compare_dec.v _build_vo/default//lib/coq/theories/Arith/Compare_dec.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Compare.v _build_vo/default//lib/coq/theories/Arith/Compare.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Cantor.v _build_vo/default//lib/coq/theories/Arith/Cantor.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Bool_nat.v _build_vo/default//lib/coq/theories/Arith/Bool_nat.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Between.v _build_vo/default//lib/coq/theories/Arith/Between.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Arith_base.v _build_vo/default//lib/coq/theories/Arith/Arith_base.v >cp -a theories/Arith/Arith.v _build_vo/default//lib/coq/theories/Arith/Arith.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/String.v _build_vo/default//lib/coq/user-contrib/Ltac2/String.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Std.v _build_vo/default//lib/coq/user-contrib/Ltac2/Std.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Printf.v _build_vo/default//lib/coq/user-contrib/Ltac2/Printf.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Pattern.v _build_vo/default//lib/coq/user-contrib/Ltac2/Pattern.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Option.v _build_vo/default//lib/coq/user-contrib/Ltac2/Option.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Notations.v _build_vo/default//lib/coq/user-contrib/Ltac2/Notations.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Message.v _build_vo/default//lib/coq/user-contrib/Ltac2/Message.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Ltac2.v _build_vo/default//lib/coq/user-contrib/Ltac2/Ltac2.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Ltac1.v _build_vo/default//lib/coq/user-contrib/Ltac2/Ltac1.v >cp -a user-contrib/Ltac2/List.v _build_vo/default//lib/coq/user-contrib/Ltac2/List.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Int.v _build_vo/default//lib/coq/user-contrib/Ltac2/Int.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Init.v _build_vo/default//lib/coq/user-contrib/Ltac2/Init.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Ind.v _build_vo/default//lib/coq/user-contrib/Ltac2/Ind.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Ident.v _build_vo/default//lib/coq/user-contrib/Ltac2/Ident.v >cp -a user-contrib/Ltac2/Fresh.v _build_vo/default//lib/coq/user-contrib/Ltac2/Fresh.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Env.v _build_vo/default//lib/coq/user-contrib/Ltac2/Env.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Control.v _build_vo/default//lib/coq/user-contrib/Ltac2/Control.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Constr.v _build_vo/default//lib/coq/user-contrib/Ltac2/Constr.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Char.v _build_vo/default//lib/coq/user-contrib/Ltac2/Char.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Bool.v _build_vo/default//lib/coq/user-contrib/Ltac2/Bool.v >mkdir -p _build_vo/default//lib/coq/user-contrib/Ltac2 >cp -a user-contrib/Ltac2/Array.v _build_vo/default//lib/coq/user-contrib/Ltac2/Array.v > ocamlc lib/.lib.objs/byte/util.{cmi,cmti} >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. > ocamlc lib/.lib.objs/byte/coqProject_file.{cmo,cmt} >File "lib/coqProject_file.ml", line 82, characters 35-46: >82 | let rec parse_string buf s = match Stream.next s with > ^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 90, characters 12-26: >90 | | exception Stream.Failure -> buffer buf > ^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 92, characters 32-43: >92 | and parse_string2 buf s = match Stream.next s with > ^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 97, characters 12-26: >97 | | exception Stream.Failure -> raise (Parsing_error "unterminated string") > ^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 99, characters 33-44: >99 | and parse_skip_comment s = match Stream.next s with > ^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 102, characters 12-26: >102 | | exception Stream.Failure -> () > ^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 104, characters 34-45: >104 | and parse_args buf accu s = match Stream.next s with > ^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 116, characters 12-26: >116 | | exception Stream.Failure -> accu > ^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "lib/coqProject_file.ml", line 123, characters 31-48: >123 | let res = parse_args buf [] (Stream.of_channel c) in > ^^^^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc lib/.lib.objs/byte/util.{cmo,cmt} >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. > ocamlc lib/.lib.objs/byte/lStream.{cmo,cmt} >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. >touch _build/install/default/bin/coqdep >find theories user-contrib/Ltac2 -type f -name '*.v' | \ >sed 's|^|_build_vo/default//lib/coq/|' | \ >xargs _build/install/default/bin/coqdep -boot -dyndep byte -R _build_vo/default//lib/coq/theories Coq -Q _build_vo/default//lib/coq/user-contrib "" -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax > ".vfiles.d" >flock .dune.lock dune build --display=quiet --release @all-src >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqc.byte >flock .dune.lock dune build --display=quiet --release _build/install/default/lib/stublibs/dllcoqrun_stubs.so >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ltac/ltac_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/syntax/number_string_notation_plugin.cma > ocamlc gramlib/.gramlib.objs/byte/gramlib__Plexing.{cmi,cmti} >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. > ocamlc gramlib/.gramlib.objs/byte/gramlib__Plexing.{cmo,cmt} >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. > ocamlc gramlib/.gramlib.objs/byte/gramlib__Grammar.{cmi,cmti} >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. >x86_64-pc-linux-gnu-gcc kernel/byterun/coq_fix_code.o >coq_fix_code.c: In function âcoq_stat_allocâ: >coq_fix_code.c:36:13: warning: "raise_out_of_memory" is deprecated: use "caml_raise_out_of_memory" instead > 36 | if (result == NULL) raise_out_of_memory (); > | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ >x86_64-pc-linux-gnu-gcc kernel/byterun/coq_memory.o >coq_memory.c: In function âinit_coq_vmâ: >coq_memory.c:114:13: warning: "scan_roots_hook" is deprecated: use "caml_scan_roots_hook" instead > 114 | coq_prev_scan_roots_hook = scan_roots_hook; > | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ >coq_memory.c:115:13: warning: "scan_roots_hook" is deprecated: use "caml_scan_roots_hook" instead > 115 | scan_roots_hook = coq_scan_roots; > | ^~~~~~~~~~~~~~~~~~~~~~~~~ > ocamlc gramlib/.gramlib.objs/byte/gramlib__Grammar.{cmo,cmt} >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. >x86_64-pc-linux-gnu-gcc kernel/byterun/coq_interp.o >coq_interp.c: In function âcoq_interpreteâ: >coq_interp.c:287:20: warning: storing the address of local variable âcoq_lbl_ACC0â in âcoq_instr_baseâ [-Wdangling-pointer=] > 287 | coq_instr_base = coq_Jumptbl_base; > | ^ >coq_interp.c:74:26: note: âcoq_lbl_ACC0â declared here > 74 | # define Instruct(name) coq_lbl_##name: > | ^~~~~~~~ >coq_interp.c:311:7: note: in expansion of macro âInstructâ > 311 | Instruct(ACC0){ > | ^~~~~~~~ >In file included from coq_interp.c:28: >coq_fix_code.h:20:15: note: âcoq_instr_baseâ declared here > 20 | extern char * coq_instr_base; > | ^~~~~~~~~~~~~~ > ocamlc engine/.engine.objs/byte/evarutil.{cmo,cmt} >File "engine/evarutil.ml", line 124, characters 10-18: >124 | let m = E.create () in > ^^^^^^^^ >Alert old_ephemeron_api: E.create >This function won't be available in 5.0 >File "engine/evarutil.ml", line 125, characters 19-29: >125 | fun x y -> match E.get_key1 m, E.get_key2 m with > ^^^^^^^^^^ >Alert old_ephemeron_api: E.get_key1 >This function won't be available in 5.0 >File "engine/evarutil.ml", line 125, characters 33-43: >125 | fun x y -> match E.get_key1 m, E.get_key2 m with > ^^^^^^^^^^ >Alert old_ephemeron_api: E.get_key2 >This function won't be available in 5.0 >File "engine/evarutil.ml", line 126, characters 60-70: >126 | | Some x', Some y' when x == x' && y == y' -> Option.get (E.get_data m) > ^^^^^^^^^^ >Alert old_ephemeron_api: E.get_data >This function won't be available in 5.0 >File "engine/evarutil.ml", line 127, characters 26-36: >127 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r > ^^^^^^^^^^ >Alert old_ephemeron_api: E.set_key1 >This function won't be available in 5.0 >File "engine/evarutil.ml", line 127, characters 42-52: >127 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r > ^^^^^^^^^^ >Alert old_ephemeron_api: E.set_key2 >This function won't be available in 5.0 >File "engine/evarutil.ml", line 127, characters 58-68: >127 | | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r > ^^^^^^^^^^ >Alert old_ephemeron_api: E.set_data >This function won't be available in 5.0 > ocamlc interp/.interp.objs/byte/numTok.{cmi,cmti} >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. > ocamlc interp/.interp.objs/byte/numTok.{cmo,cmt} >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. > ocamlc interp/.interp.objs/byte/constrexpr_ops.{cmo,cmt} >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. > ocamlc parsing/.parsing.objs/byte/tok.{cmo,cmt} >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. > ocamlc parsing/.parsing.objs/byte/pcoq.{cmo,cmt} >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. > ocamlc parsing/.parsing.objs/byte/cLexer.{cmo,cmt} >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. > ocamlc parsing/.parsing.objs/byte/g_constr.{cmi,cmo,cmt} >File "parsing/g_constr.mlg", line 46, characters 19-33: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc interp/.interp.objs/byte/constrintern.{cmo,cmt} >File "interp/constrintern.ml", line 585, characters 22-34: >585 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") > ^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc printing/.printing.objs/byte/proof_diffs.{cmo,cmt} >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. > ocamlc vernac/.vernac.objs/byte/himsg.{cmo,cmt} >File "vernac/himsg.ml", line 1428, characters 4-16: >1428 | | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") > ^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc vernac/.vernac.objs/byte/comInductive.{cmo,cmt} >File "vernac/comInductive.ml", line 365, characters 20-32: >365 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") > ^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc vernac/.vernac.objs/byte/proof_using.{cmo,cmt} >File "vernac/proof_using.ml", line 210, characters 94-110: >210 | let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) > ^^^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc vernac/.vernac.objs/byte/vernacinterp.{cmo,cmt} >File "vernac/vernacinterp.ml", line 177, characters 9-26: >177 | (Stream.of_channel in_chan) in > ^^^^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc vernac/.vernac.objs/byte/record.{cmo,cmt} >File "vernac/record.ml", line 113, characters 20-32: >113 | Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters") > ^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc toplevel/.toplevel.objs/byte/g_toplevel.{cmi,cmo,cmt} >File "toplevel/g_toplevel.mlg", line 34, characters 19-33: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. > ocamlc toplevel/.toplevel.objs/byte/vernac.{cmo,cmt} >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. > ocamlc toplevel/.toplevel.objs/byte/coqloop.{cmo,cmt} >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. >touch _build/install/default/bin/coqc.byte >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ltac/tauto_plugin.cma >touch _build/install/default/lib/stublibs/dllcoqrun_stubs.so >flock .dune.lock dune build --display=quiet --release _build/default/plugins/cc/cc_plugin.cma > ocamlc plugins/ltac/.ltac_plugin.objs/byte/ltac_plugin__G_tactic.{cmi,cmo,cmt} >File "plugins/ltac/g_tactic.mlg", line 33, characters 19-33: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >touch _build/default/plugins/ltac/ltac_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/firstorder/firstorder_plugin.cma >touch _build/default/plugins/syntax/number_string_notation_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ssrmatching/ssrmatching_plugin.cma >touch _build/default/plugins/ltac/tauto_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ssr/ssreflect_plugin.cma >touch _build/default/plugins/cc/cc_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ring/ring_plugin.cma >touch _build/default/plugins/firstorder/firstorder_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/micromega/zify_plugin.cma >touch _build/default/plugins/ssrmatching/ssrmatching_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/micromega/micromega_plugin.cma > ocamlc plugins/ssr/.ssreflect_plugin.objs/byte/ssreflect_plugin__Ssrparser.{cmo,cmt} >File "plugins/ssr/ssrparser.mlg", line 263, characters 28-42: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 265, characters 22-36: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 272, characters 24-38: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 274, characters 22-36: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 276, characters 19-33: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 283, characters 24-38: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 285, characters 22-36: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 286, characters 15-29: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 294, characters 31-45: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 297, characters 20-34: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 843, characters 33-47: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 852, characters 9-23: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 857, characters 12-26: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 858, characters 55-69: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 859, characters 45-59: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 2409, characters 37-51: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "plugins/ssr/ssrparser.mlg", line 2413, characters 17-31: >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >touch _build/default/plugins/ssr/ssreflect_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/rtauto/rtauto_plugin.cma >touch _build/default/plugins/ring/ring_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/nsatz/nsatz_plugin.cma >touch _build/default/plugins/micromega/zify_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/extraction/extraction_plugin.cma >touch _build/default/plugins/micromega/micromega_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/funind/funind_plugin.cma >touch _build/default/plugins/rtauto/rtauto_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/derive/derive_plugin.cma >touch _build/default/plugins/nsatz/nsatz_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/btauto/btauto_plugin.cma >touch _build/default/plugins/extraction/extraction_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ltac2/ltac2_plugin.cma >touch _build/default/plugins/funind/funind_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqproofworker.opt >touch _build/default/plugins/derive/derive_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqtacticworker.opt >touch _build/default/plugins/btauto/btauto_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqqueryworker.opt >touch _build/default/plugins/ltac2/ltac2_plugin.cma >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqtop >touch _build/install/default/bin/coqproofworker.opt >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqchk >touch _build/install/default/bin/coqtacticworker.opt >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/csdpcert >touch _build/install/default/bin/coqqueryworker.opt >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqnative >touch _build/install/default/bin/coqtop >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/votour > ocamlc checker/.coq_checklib.objs/byte/coq_checklib__Checker.{cmo,cmt} >File "checker/checker.ml", line 220, characters 4-18: >220 | | Stream.Failure -> > ^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "checker/checker.ml", line 222, characters 4-16: >222 | | Stream.Error txt -> > ^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >touch _build/install/default/bin/coqchk >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqdoc >touch _build/install/default/bin/csdpcert >flock .dune.lock dune build --display=quiet --release _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty >touch _build/install/default/bin/coqnative >flock .dune.lock dune build --display=quiet --release _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css >touch _build/install/default/bin/votour >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coqwc >touch _build/install/default/bin/coqdoc >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/coq_makefile >touch _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty >flock .dune.lock dune build --display=quiet --release _build/default/tools/CoqMakefile.in >touch _build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css >flock .dune.lock dune build --display=quiet --release _build/install/default/bin/ocamllibdep >touch _build/install/default/bin/coqwc >flock .dune.lock dune build --display=quiet --release _build/default/doc/tools/docgram/doc_grammar.exe >touch _build/install/default/bin/coq_makefile >flock .dune.lock dune build --display=quiet --release _build/default/coq-core.install >touch _build/default/tools/CoqMakefile.in >flock .dune.lock dune build --display=quiet --release _build/default/coqide-server.install >touch _build/install/default/bin/ocamllibdep >flock .dune.lock dune build --display=quiet --release revision >touch _build/default/doc/tools/docgram/doc_grammar.exe >rm -f _build_vo/default//lib/coq/theories/Init/Notations.glob >mkdir -p _build_vo/default//lib/coq/theories/Init >_build/install/default/bin/coqc.byte -coqlib _build_vo/default//lib/coq/ -q -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax _build_vo/default//lib/coq/theories/Init/Notations.v -o _build_vo/default//lib/coq/theories/Init/Notations.vo -noinit -R _build_vo/default//lib/coq/theories Coq >Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins >[cannot-open-dir,filesystem] >rm -f _build_vo/default//lib/coq/theories/Init/Ltac.glob >mkdir -p _build_vo/default//lib/coq/theories/Init >_build/install/default/bin/coqc.byte -coqlib _build_vo/default//lib/coq/ -q -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax _build_vo/default//lib/coq/theories/Init/Ltac.v -o _build_vo/default//lib/coq/theories/Init/Ltac.vo -noinit -R _build_vo/default//lib/coq/theories Coq >Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins >[cannot-open-dir,filesystem] >rm -f _build_vo/default//lib/coq/theories/Init/Logic.glob >mkdir -p _build_vo/default//lib/coq/theories/Init >_build/install/default/bin/coqc.byte -coqlib _build_vo/default//lib/coq/ -q -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax _build_vo/default//lib/coq/theories/Init/Logic.v -o _build_vo/default//lib/coq/theories/Init/Logic.vo -noinit -R _build_vo/default//lib/coq/theories Coq >Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins >[cannot-open-dir,filesystem] >rm -f _build_vo/default//lib/coq/theories/Init/Datatypes.glob >mkdir -p _build_vo/default//lib/coq/theories/Init >_build/install/default/bin/coqc.byte -coqlib _build_vo/default//lib/coq/ -q -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax _build_vo/default//lib/coq/theories/Init/Datatypes.v -o _build_vo/default//lib/coq/theories/Init/Datatypes.vo -noinit -R _build_vo/default//lib/coq/theories Coq >rm -f _build_vo/default//lib/coq/theories/Init/Logic_Type.glob >mkdir -p _build_vo/default//lib/coq/theories/Init >_build/install/default/bin/coqc.byte -coqlib _build_vo/default//lib/coq/ -q -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax _build_vo/default//lib/coq/theories/Init/Logic_Type.v -o _build_vo/default//lib/coq/theories/Init/Logic_Type.vo -noinit -R _build_vo/default//lib/coq/theories Coq >rm -f _build_vo/default//lib/coq/theories/Init/Specif.glob >mkdir -p _build_vo/default//lib/coq/theories/Init >_build/install/default/bin/coqc.byte -coqlib _build_vo/default//lib/coq/ -q -I _build/default/plugins/btauto -I _build/default/plugins/cc -I _build/default/plugins/derive -I _build/default/plugins/extraction -I _build/default/plugins/firstorder -I _build/default/plugins/funind -I _build/default/plugins/ltac -I _build/default/plugins/ltac2 -I _build/default/plugins/micromega -I _build/default/plugins/nsatz -I _build/default/plugins/ring -I _build/default/plugins/rtauto -I _build/default/plugins/ssr -I _build/default/plugins/ssrmatching -I _build/default/plugins/syntax _build_vo/default//lib/coq/theories/Init/Specif.v -o _build_vo/default//lib/coq/theories/Init/Specif.vo -noinit -R _build_vo/default//lib/coq/theories Coq >File "topbin/dune", line 24, characters 7-15: >24 | (name coqc_bin) > ^^^^^^^^ >Error: No rule found for topbin/coqc_bin.exe >make[1]: *** [Makefile.common:184: _build/default/coq-core.install] Error 1 >make[1]: *** Waiting for unfinished jobs.... > ocamlc ide/coqide/.idetop.eobjs/byte/dune__exe__Idetop.{cmi,cmo,cmt} >File "ide/coqide/idetop.ml", line 85, characters 36-52: >85 | let pa = Pcoq.Parsable.make ~loc (Stream.of_string s) in > ^^^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "ide/coqide/idetop.ml", line 112, characters 31-47: >112 | let pa = Pcoq.Parsable.make (Stream.of_string s) in > ^^^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "ide/coqide/idetop.ml", line 118, characters 31-47: >118 | let pa = Pcoq.Parsable.make (Stream.of_string phrase) in > ^^^^^^^^^^^^^^^^ >Alert deprecated: module Stdlib.Stream >Use the camlp-streams library instead. >File "ide/coqide/dune", line 12, characters 7-13: >12 | (name idetop) > ^^^^^^ >Error: No rule found for ide/coqide/idetop.exe >make[1]: *** [Makefile.common:184: _build/default/coqide-server.install] Error 1 >touch revision >rm _build/install/default/lib/stublibs/dllcoqrun_stubs.so >make[1]: Leaving directory '/var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2' >make: *** [Makefile.make:122: submake] Error 2 > * ERROR: sci-mathematics/coq-8.15.2::gentoo failed (compile phase): > * emake failed > * > * If you need support, post the output of `emerge --info '=sci-mathematics/coq-8.15.2::gentoo'`, > * the complete build log and the output of `emerge -pqv '=sci-mathematics/coq-8.15.2::gentoo'`. > * The complete build log is located at '/var/log/portage/sci-mathematics:coq-8.15.2:20220604-011345.log'. > * For convenience, a symlink to the build log is located at '/var/tmp/portage/sci-mathematics/coq-8.15.2/temp/build.log'. > * The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/coq-8.15.2/temp/environment'. > * Working directory: '/var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2' > * S: '/var/tmp/portage/sci-mathematics/coq-8.15.2/work/coq-8.15.2' >
<b>You cannot view the attachment while viewing its details because your browser does not support IFRAMEs. <a href="attachment.cgi?id=782702">View the attachment on a separate page</a>.</b>
View Attachment As Raw
Actions:
View
Attachments on
bug 849638
:
782690
|
782693
|
782696
|
782699
| 782702 |
782705
