Go to:
Gentoo Home
Documentation
Forums
Lists
Bugs
Planet
Store
Wiki
Get Gentoo!
Gentoo's Bugzilla – Attachment 767340 Details for
Bug 835583
sci-mathematics/coq-8.15.0-r2 - Fatal error: exception Stack overflow
Home
|
New
–
[Ex]
|
Browse
|
Search
|
Privacy Policy
|
[?]
|
Reports
|
Requests
|
Help
|
New Account
|
Log In
[x]
|
Forgot Password
Login:
[x]
sci-mathematics:coq-8.15.0-r2:20220318-113342.log
sci-mathematics:coq-8.15.0-r2:20220318-113342.log (text/plain), 95.98 KB, created by
Toralf Förster
on 2022-03-18 14:50:52 UTC
(
hide
)
Description:
sci-mathematics:coq-8.15.0-r2:20220318-113342.log
Filename:
MIME Type:
Creator:
Toralf Förster
Created:
2022-03-18 14:50:52 UTC
Size:
95.98 KB
patch
obsolete
> * Package: sci-mathematics/coq-8.15.0-r2 > * Repository: gentoo > * Maintainer: sci-mathematics@gentoo.org > * Upstream: https://github.com/coq/coq/issues/ > * USE: abi_x86_64 amd64 elibc_glibc kernel_linux ocamlopt userland_GNU > * FEATURES: network-sandbox preserve-libs sandbox userpriv usersandbox > >>>> Unpacking source... >>>> Unpacking coq-8.15.0.tar.gz to /var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work >>>> Source unpacked in /var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work >>>> Preparing source in /var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0 ... >>>> Source prepared. >>>> Configuring source in /var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0 ... >Configure options: -prefix /usr -libdir /usr/lib64/coq -mandir /usr/share/man -docdir /usr/share/doc/coq-8.15.0-r2 -datadir /usr/share/coq -configdir /etc/xdg/coq -with-doc no -coqide no >You have OCaml 4.09.0. Good! >You have OCamlfind 1.9.3. Good! >You have native-code compilation. 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.09.0 > OCaml binaries in : /usr/bin/ > OCaml library in : /usr/lib64/ocaml > Native dynamic link support : true > CoqIDE : no > Documentation : None > Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & > Coq web site : http://coq.inria.fr/ > Bytecode VM enabled : true > Native Compiler enabled : 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.0-r2 > >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.0-r2/work/coq-8.15.0 ... >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.0-r2/work/coq-8.15.0' >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.0-r2/work/coq-8.15.0/_build/install/default/bin/ bin >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0/_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.0-r2/work/coq-8.15.0/_build/install/default/lib/coq-core/ _build_vo/default//lib/coq-core >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0/_build/install/default/lib/coqide-server/ _build_vo/default//lib/coqide-server >ln -s /var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0/_build/install/default/lib/stublibs/ _build_vo/default//lib/stublibs >mkdir -p _build_vo/default//lib/coq/theories/ssrmatching >cp -a theories/ssrmatching/ssrmatching.v _build_vo/default//lib/coq/theories/ssrmatching/ssrmatching.v >mkdir -p _build_vo/default//lib/coq/theories/ssr >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 >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 >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_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 >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 >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 >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 >cp -a theories/setoid_ring/Ring.v _build_vo/default//lib/coq/theories/setoid_ring/Ring.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/RealField.v _build_vo/default//lib/coq/theories/setoid_ring/RealField.v >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 >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 >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 >cp -a theories/setoid_ring/ArithRing.v _build_vo/default//lib/coq/theories/setoid_ring/ArithRing.v >mkdir -p _build_vo/default//lib/coq/theories/setoid_ring >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 >cp -a theories/micromega/Psatz.v _build_vo/default//lib/coq/theories/micromega/Psatz.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/OrderedRing.v _build_vo/default//lib/coq/theories/micromega/OrderedRing.v >mkdir -p _build_vo/default//lib/coq/theories/micromega >mkdir -p _build_vo/default//lib/coq/theories/micromega >cp -a theories/micromega/MExtraction.v _build_vo/default//lib/coq/theories/micromega/MExtraction.v >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 >cp -a theories/funind/Recdef.v _build_vo/default//lib/coq/theories/funind/Recdef.v >mkdir -p _build_vo/default//lib/coq/theories/funind >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/funind/FunInd.v _build_vo/default//lib/coq/theories/funind/FunInd.v >cp -a theories/extraction/Extraction.v _build_vo/default//lib/coq/theories/extraction/Extraction.v >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 >mkdir -p _build_vo/default//lib/coq/theories/extraction >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 >mkdir -p _build_vo/default//lib/coq/theories/extraction >cp -a theories/extraction/ExtrHaskellNatInteger.v _build_vo/default//lib/coq/theories/extraction/ExtrHaskellNatInteger.v >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 >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/btauto/Algebra.v _build_vo/default//lib/coq/theories/btauto/Algebra.v >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 >cp -a theories/ZArith/Zpow_def.v _build_vo/default//lib/coq/theories/ZArith/Zpow_def.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >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 >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Znumtheory.v _build_vo/default//lib/coq/theories/ZArith/Znumtheory.v >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 >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zeuclid.v _build_vo/default//lib/coq/theories/ZArith/Zeuclid.v >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 >cp -a theories/ZArith/Zcomplements.v _build_vo/default//lib/coq/theories/ZArith/Zcomplements.v >mkdir -p _build_vo/default//lib/coq/theories/ZArith >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 >mkdir -p _build_vo/default//lib/coq/theories/ZArith >cp -a theories/ZArith/Zabs.v _build_vo/default//lib/coq/theories/ZArith/Zabs.v >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 >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 >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 >cp -a theories/ZArith/BinInt.v _build_vo/default//lib/coq/theories/ZArith/BinInt.v >mkdir -p _build_vo/default//lib/coq/theories/Wellfounded >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 >cp -a theories/Vectors/VectorDef.v _build_vo/default//lib/coq/theories/Vectors/VectorDef.v >mkdir -p _build_vo/default//lib/coq/theories/Vectors >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 >cp -a theories/Structures/OrdersLists.v _build_vo/default//lib/coq/theories/Structures/OrdersLists.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >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 >cp -a theories/Structures/OrderedType.v _build_vo/default//lib/coq/theories/Structures/OrderedType.v >mkdir -p _build_vo/default//lib/coq/theories/Structures >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 >mkdir -p _build_vo/default//lib/coq/theories/Structures >cp -a theories/Structures/Equalities.v _build_vo/default//lib/coq/theories/Structures/Equalities.v >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 >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/Sorting.v _build_vo/default//lib/coq/theories/Sorting/Sorting.v >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 >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/PermutSetoid.v _build_vo/default//lib/coq/theories/Sorting/PermutSetoid.v >cp -a theories/Sorting/PermutEq.v _build_vo/default//lib/coq/theories/Sorting/PermutEq.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/Mergesort.v _build_vo/default//lib/coq/theories/Sorting/Mergesort.v >mkdir -p _build_vo/default//lib/coq/theories/Sorting >mkdir -p _build_vo/default//lib/coq/theories/Sorting >cp -a theories/Sorting/Heap.v _build_vo/default//lib/coq/theories/Sorting/Heap.v >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 >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 >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 >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 >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 >mkdir -p _build_vo/default//lib/coq/theories/Sets >cp -a theories/Sets/Image.v _build_vo/default//lib/coq/theories/Sets/Image.v >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 >mkdir -p _build_vo/default//lib/coq/theories/Relations >cp -a theories/Relations/Relations.v _build_vo/default//lib/coq/theories/Relations/Relations.v >cp -a theories/Relations/Relation_Operators.v _build_vo/default//lib/coq/theories/Relations/Relation_Operators.v >mkdir -p _build_vo/default//lib/coq/theories/Relations >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 >cp -a theories/Reals/Rtrigo.v _build_vo/default//lib/coq/theories/Reals/Rtrigo.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >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 >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rprod.v _build_vo/default//lib/coq/theories/Reals/Rprod.v >cp -a theories/Reals/Rpower.v _build_vo/default//lib/coq/theories/Reals/Rpower.v >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 >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rminmax.v _build_vo/default//lib/coq/theories/Reals/Rminmax.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rlogic.v _build_vo/default//lib/coq/theories/Reals/Rlogic.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rlimit.v _build_vo/default//lib/coq/theories/Reals/Rlimit.v >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 >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Reals.v _build_vo/default//lib/coq/theories/Reals/Reals.v >cp -a theories/Reals/Rderiv.v _build_vo/default//lib/coq/theories/Reals/Rderiv.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Rdefinitions.v _build_vo/default//lib/coq/theories/Reals/Rdefinitions.v >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 >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Ranalysis5.v _build_vo/default//lib/coq/theories/Reals/Ranalysis5.v >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 >cp -a theories/Reals/Ranalysis2.v _build_vo/default//lib/coq/theories/Reals/Ranalysis2.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >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 >cp -a theories/Reals/R_sqr.v _build_vo/default//lib/coq/theories/Reals/R_sqr.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >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 >cp -a theories/Reals/PartSum.v _build_vo/default//lib/coq/theories/Reals/PartSum.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >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 >cp -a theories/Reals/MVT.v _build_vo/default//lib/coq/theories/Reals/MVT.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Integration.v _build_vo/default//lib/coq/theories/Reals/Integration.v >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 >cp -a theories/Reals/DiscrR.v _build_vo/default//lib/coq/theories/Reals/DiscrR.v >mkdir -p _build_vo/default//lib/coq/theories/Reals >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 >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/ClassicalDedekindReals.v _build_vo/default//lib/coq/theories/Reals/ClassicalDedekindReals.v >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 >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 >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 >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/Cauchy/ConstructiveCauchyAbs.v _build_vo/default//lib/coq/theories/Reals/Cauchy/ConstructiveCauchyAbs.v >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 >mkdir -p _build_vo/default//lib/coq/theories/Reals >cp -a theories/Reals/AltSeries.v _build_vo/default//lib/coq/theories/Reals/AltSeries.v >cp -a theories/Reals/Alembert.v _build_vo/default//lib/coq/theories/Reals/Alembert.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >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 >cp -a theories/Reals/Abstract/ConstructiveMinMax.v _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveMinMax.v >mkdir -p _build_vo/default//lib/coq/theories/Reals/Abstract >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 >cp -a theories/QArith/Qpower.v _build_vo/default//lib/coq/theories/QArith/Qpower.v >mkdir -p _build_vo/default//lib/coq/theories/QArith >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 >mkdir -p _build_vo/default//lib/coq/theories/QArith >cp -a theories/QArith/Qabs.v _build_vo/default//lib/coq/theories/QArith/Qabs.v >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 >cp -a theories/Program/Program.v _build_vo/default//lib/coq/theories/Program/Program.v >mkdir -p _build_vo/default//lib/coq/theories/Program >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 >cp -a theories/PArith/Pnat.v _build_vo/default//lib/coq/theories/PArith/Pnat.v >mkdir -p _build_vo/default//lib/coq/theories/PArith >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 >cp -a theories/Numbers/Natural/Peano/NPeano.v _build_vo/default//lib/coq/theories/Numbers/Natural/Peano/NPeano.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Binary >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 >cp -a theories/Numbers/Natural/Abstract/NStrongRec.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NStrongRec.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >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 >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 >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 >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 >cp -a theories/Numbers/Natural/Abstract/NGcd.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NGcd.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >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 >cp -a theories/Numbers/Natural/Abstract/NBase.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NBase.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >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 >cp -a theories/Numbers/Natural/Abstract/NAddOrder.v _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract/NAddOrder.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Natural/Abstract >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 >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 >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 >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 >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 >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 >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 >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 >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 >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 >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 >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/NatInt/NZAdd.v _build_vo/default//lib/coq/theories/Numbers/NatInt/NZAdd.v >cp -a theories/Numbers/NaryFunctions.v _build_vo/default//lib/coq/theories/Numbers/NaryFunctions.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/NatPairs >mkdir -p _build_vo/default//lib/coq/theories/Numbers/Integer/Binary >cp -a theories/Numbers/Integer/NatPairs/ZNatPairs.v _build_vo/default//lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.v >cp -a theories/Numbers/Integer/Binary/ZBinary.v _build_vo/default//lib/coq/theories/Numbers/Integer/Binary/ZBinary.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/ZSgnAbs.v _build_vo/default//lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.v >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 >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 >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 >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 >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 >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 >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 >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 >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 >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 >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 >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 >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 >cp -a theories/Numbers/Cyclic/Abstract/CarryType.v _build_vo/default//lib/coq/theories/Numbers/Cyclic/Abstract/CarryType.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/BinNums.v _build_vo/default//lib/coq/theories/Numbers/BinNums.v >mkdir -p _build_vo/default//lib/coq/theories/Numbers >cp -a theories/Numbers/AltBinNotations.v _build_vo/default//lib/coq/theories/Numbers/AltBinNotations.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >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 >cp -a theories/NArith/Ndist.v _build_vo/default//lib/coq/theories/NArith/Ndist.v >mkdir -p _build_vo/default//lib/coq/theories/NArith >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 >cp -a theories/MSets/MSetProperties.v _build_vo/default//lib/coq/theories/MSets/MSetProperties.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >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 >cp -a theories/MSets/MSetEqProperties.v _build_vo/default//lib/coq/theories/MSets/MSetEqProperties.v >mkdir -p _build_vo/default//lib/coq/theories/MSets >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 >cp -a theories/Logic/WeakFan.v _build_vo/default//lib/coq/theories/Logic/WeakFan.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >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 >cp -a theories/Logic/ProofIrrelevanceFacts.v _build_vo/default//lib/coq/theories/Logic/ProofIrrelevanceFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >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 >cp -a theories/Logic/FinFun.v _build_vo/default//lib/coq/theories/Logic/FinFun.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >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 >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 >cp -a theories/Logic/EqdepFacts.v _build_vo/default//lib/coq/theories/Logic/EqdepFacts.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >mkdir -p _build_vo/default//lib/coq/theories/Logic >cp -a theories/Logic/Eqdep.v _build_vo/default//lib/coq/theories/Logic/Eqdep.v >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 >cp -a theories/Logic/ClassicalDescription.v _build_vo/default//lib/coq/theories/Logic/ClassicalDescription.v >mkdir -p _build_vo/default//lib/coq/theories/Logic >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 >cp -a theories/Lists/SetoidPermutation.v _build_vo/default//lib/coq/theories/Lists/SetoidPermutation.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/SetoidList.v _build_vo/default//lib/coq/theories/Lists/SetoidList.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/ListTactics.v _build_vo/default//lib/coq/theories/Lists/ListTactics.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/ListSet.v _build_vo/default//lib/coq/theories/Lists/ListSet.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >cp -a theories/Lists/ListDec.v _build_vo/default//lib/coq/theories/Lists/ListDec.v >mkdir -p _build_vo/default//lib/coq/theories/Lists >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 >cp -a theories/Init/Tauto.v _build_vo/default//lib/coq/theories/Init/Tauto.v >mkdir -p _build_vo/default//lib/coq/theories/Init >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 >cp -a theories/Init/Logic.v _build_vo/default//lib/coq/theories/Init/Logic.v >mkdir -p _build_vo/default//lib/coq/theories/Init >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 >cp -a theories/Floats/SpecFloat.v _build_vo/default//lib/coq/theories/Floats/SpecFloat.v >mkdir -p _build_vo/default//lib/coq/theories/Floats >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 >cp -a theories/FSets/FSetProperties.v _build_vo/default//lib/coq/theories/FSets/FSetProperties.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >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 >cp -a theories/FSets/FSetAVL.v _build_vo/default//lib/coq/theories/FSets/FSetAVL.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >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 >cp -a theories/FSets/FMapList.v _build_vo/default//lib/coq/theories/FSets/FMapList.v >mkdir -p _build_vo/default//lib/coq/theories/FSets >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 >cp -a theories/Compat/Coq815.v _build_vo/default//lib/coq/theories/Compat/Coq815.v >mkdir -p _build_vo/default//lib/coq/theories/Compat >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 >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/SetoidDec.v _build_vo/default//lib/coq/theories/Classes/SetoidDec.v >cp -a theories/Classes/SetoidClass.v _build_vo/default//lib/coq/theories/Classes/SetoidClass.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >cp -a theories/Classes/RelationPairs.v _build_vo/default//lib/coq/theories/Classes/RelationPairs.v >mkdir -p _build_vo/default//lib/coq/theories/Classes >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 >cp -a theories/Bool/IfProp.v _build_vo/default//lib/coq/theories/Bool/IfProp.v >mkdir -p _build_vo/default//lib/coq/theories/Bool >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 >cp -a theories/Array/PArray.v _build_vo/default//lib/coq/theories/Array/PArray.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >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 >mkdir -p _build_vo/default//lib/coq/theories/Arith >cp -a theories/Arith/Euclid.v _build_vo/default//lib/coq/theories/Arith/Euclid.v >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 >cp -a theories/Arith/Arith_base.v _build_vo/default//lib/coq/theories/Arith/Arith_base.v >mkdir -p _build_vo/default//lib/coq/theories/Arith >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 >cp -a user-contrib/Ltac2/Ltac1.v _build_vo/default//lib/coq/user-contrib/Ltac2/Ltac1.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/List.v _build_vo/default//lib/coq/user-contrib/Ltac2/List.v >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 >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 >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 >cp -a user-contrib/Ltac2/Ident.v _build_vo/default//lib/coq/user-contrib/Ltac2/Ident.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/Fresh.v _build_vo/default//lib/coq/user-contrib/Ltac2/Fresh.v >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 >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 >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 >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 opt -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 >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ltac/ltac_plugin.cmxs >flock .dune.lock dune build --display=quiet --release _build/default/plugins/syntax/number_string_notation_plugin.cmxs >flock .dune.lock dune build --display=quiet --release _build/default/plugins/ltac/tauto_plugin.cmxs > ocamlopt vernac/.vernac.objs/native/g_vernac.{cmx,o} (exit 2) >(cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib64/ocaml/threads -I /usr/lib64/ocaml/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/g_vernac.cmx -c -impl vernac/g_vernac.ml) >Fatal error: exception Stack overflow >make[1]: *** [Makefile.common:131: _build/install/default/bin/coqc] Error 1 >make[1]: *** Waiting for unfinished jobs.... > ocamlopt vernac/.vernac.objs/native/g_vernac.{cmx,o} (exit 2) >(cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib64/ocaml/threads -I /usr/lib64/ocaml/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/g_vernac.cmx -c -impl vernac/g_vernac.ml) >Fatal error: exception Stack overflow >make[1]: *** [Makefile.common:143: _build/default/plugins/ltac/ltac_plugin.cmxs] Error 1 > ocamlopt vernac/.vernac.objs/native/g_vernac.{cmx,o} (exit 2) >(cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib64/ocaml/threads -I /usr/lib64/ocaml/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/g_vernac.cmx -c -impl vernac/g_vernac.ml) >Fatal error: exception Stack overflow >make[1]: *** [Makefile.common:143: _build/default/plugins/syntax/number_string_notation_plugin.cmxs] Error 1 > ocamlopt vernac/.vernac.objs/native/g_vernac.{cmx,o} (exit 2) >(cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I vernac/.vernac.objs/byte -I vernac/.vernac.objs/native -I /usr/lib64/ocaml/threads -I /usr/lib64/ocaml/zarith -I boot/.boot.objs/byte -I boot/.boot.objs/native -I clib/.clib.objs/byte -I clib/.clib.objs/native -I config/.config.objs/byte -I config/.config.objs/native -I engine/.engine.objs/byte -I engine/.engine.objs/native -I gramlib/.gramlib.objs/byte -I gramlib/.gramlib.objs/native -I interp/.interp.objs/byte -I interp/.interp.objs/native -I kernel/.kernel.objs/byte -I kernel/.kernel.objs/native -I kernel/byterun/.coqrun.objs/byte -I kernel/byterun/.coqrun.objs/native -I lib/.lib.objs/byte -I lib/.lib.objs/native -I library/.library.objs/byte -I library/.library.objs/native -I parsing/.parsing.objs/byte -I parsing/.parsing.objs/native -I pretyping/.pretyping.objs/byte -I pretyping/.pretyping.objs/native -I printing/.printing.objs/byte -I printing/.printing.objs/native -I proofs/.proofs.objs/byte -I proofs/.proofs.objs/native -I tactics/.tactics.objs/byte -I tactics/.tactics.objs/native -intf-suffix .ml -no-alias-deps -o vernac/.vernac.objs/native/g_vernac.cmx -c -impl vernac/g_vernac.ml) >Fatal error: exception Stack overflow >make[1]: *** [Makefile.common:143: _build/default/plugins/ltac/tauto_plugin.cmxs] Error 1 >make[1]: Leaving directory '/var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0' >make: *** [Makefile.make:122: submake] Error 2 > * ERROR: sci-mathematics/coq-8.15.0-r2::gentoo failed (compile phase): > * emake failed > * > * If you need support, post the output of `emerge --info '=sci-mathematics/coq-8.15.0-r2::gentoo'`, > * the complete build log and the output of `emerge -pqv '=sci-mathematics/coq-8.15.0-r2::gentoo'`. > * The complete build log is located at '/var/log/portage/sci-mathematics:coq-8.15.0-r2:20220318-113342.log'. > * For convenience, a symlink to the build log is located at '/var/tmp/portage/sci-mathematics/coq-8.15.0-r2/temp/build.log'. > * The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/coq-8.15.0-r2/temp/environment'. > * Working directory: '/var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0' > * S: '/var/tmp/portage/sci-mathematics/coq-8.15.0-r2/work/coq-8.15.0' >
<b>You cannot view the attachment while viewing its details because your browser does not support IFRAMEs. <a href="attachment.cgi?id=767340">View the attachment on a separate page</a>.</b>
View Attachment As Raw
Actions:
View
Attachments on
bug 835583
:
767336
|
767337
|
767338
|
767339
| 767340 |
767341
