starting phase `set-SOURCE-DATE-EPOCH' phase `set-SOURCE-DATE-EPOCH' succeeded after 0.0 seconds starting phase `set-paths' environment variable `PATH' set to `/gnu/store/b3ijxswrcsl3l4406aawbmby4nc0lc0b-autoconf-2.69/bin:/gnu/store/pwnl32gbma9xw5sjyhfv5n25c75bsl1d-automake-1.16.2/bin:/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/bin:/gnu/store/n3gp6sh4fb3ar05mmkwp2avn55sn9mj1-which-2.21/bin:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/bin:/gnu/store/am3imbjafa1wdvw9j6qabrxc09w169lz-tar-1.32/bin:/gnu/store/chqjscapsg928dy8pg6yrdhw3ypk8c9x-gzip-1.10/bin:/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/bin:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/bin:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/bin:/gnu/store/m8fnsfqs18c3srjiaw4frqadb9rqsq16-diffutils-3.7/bin:/gnu/store/2cfnrxy8icrz3sxfn86k0klmvsnj1n82-patch-2.7.6/bin:/gnu/store/0bmzacdzdhi41kkjbsq7iakwjzxkv6fm-findutils-4.7.0/bin:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/bin:/gnu/store/qy7gpiba7s7ylpfxaay6i76rk892j52n-sed-4.8/bin:/gnu/store/74d5jq5sj2fhy5j0j07jqdclf8nyxgqn-grep-3.4/bin:/gnu/store/wy177cwa387g9kaf3ss716d4fhzb21wx-coreutils-8.32/bin:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/bin:/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin:/gnu/store/y4iy1jvfq07gxynkb9jl1f69jmy349vi-ld-wrapper-0/bin:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/bin:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/bin:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/bin:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/sbin' environment variable `ACLOCAL_PATH' set to `/gnu/store/pwnl32gbma9xw5sjyhfv5n25c75bsl1d-automake-1.16.2/share/aclocal' environment variable `OCAMLPATH' set to `/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/lib/ocaml:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml/site-lib' environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/stublibs:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml/site-lib/stublibs' environment variable `COQPATH' set to `/gnu/store/zzd8f8dzlid6ry0sln843f3rih6mps9w-coq-flocq-3.3.1/lib/coq/user-contrib:/gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib:/gnu/store/v43cj96i26kw914sw8xqpp4wxlccpgc3-coq-coquelicot-3.1.0/lib/coq/user-contrib:/gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq/user-contrib' environment variable `COQLIB' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/coq' environment variable `BASH_LOADABLES_PATH' unset environment variable `C_INCLUDE_PATH' set to `/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/include:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/include:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/include:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/include:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/include:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/include:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/include:/gnu/store/72z9rxrrmfw1xx9gf27jm2s8h5h0fkh0-linux-libre-headers-5.4.20/include' environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/include:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/include:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/include:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/include:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/include:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/include:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include/c++:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/include:/gnu/store/72z9rxrrmfw1xx9gf27jm2s8h5h0fkh0-linux-libre-headers-5.4.20/include' environment variable `LIBRARY_PATH' set to `/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/lib:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib:/gnu/store/zzd8f8dzlid6ry0sln843f3rih6mps9w-coq-flocq-3.3.1/lib:/gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib:/gnu/store/v43cj96i26kw914sw8xqpp4wxlccpgc3-coq-coquelicot-3.1.0/lib:/gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib:/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/lib:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/lib:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/lib:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/lib:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/lib:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/lib:/gnu/store/m4l52mw8m0amgy4j129z5j0syryb7pkg-glibc-2.31-static/lib:/gnu/store/vispxhcwmvasm225pm373jhfn21q1sa1-glibc-utf8-locales-2.31/lib' environment variable `GUIX_LOCPATH' set to `/gnu/store/vispxhcwmvasm225pm373jhfn21q1sa1-glibc-utf8-locales-2.31/lib/locale' phase `set-paths' succeeded after 0.2 seconds starting phase `install-locale' using 'en_US.utf8' locale for category "LC_ALL" phase `install-locale' succeeded after 0.0 seconds starting phase `unpack' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/.gitignore' -> `./.gitignore' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/.gitlab-ci.yml' -> `./.gitlab-ci.yml' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/INSTALL.md' -> `./INSTALL.md' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/NEWS.md' -> `./NEWS.md' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/README.md' -> `./README.md' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/Remakefile.in' -> `./Remakefile.in' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/_CoqProject' -> `./_CoqProject' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/configure.in' -> `./configure.in' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/opam' -> `./opam' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/.gitattributes' -> `./.gitattributes' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/.mailmap' -> `./.mailmap' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/AUTHORS' -> `./AUTHORS' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/COPYING' -> `./COPYING' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/remake.cpp' -> `./remake.cpp' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20201020.v' -> `./testsuite/bug-20201020.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20201223.v' -> `./testsuite/bug-20201223.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20210113.v' -> `./testsuite/bug-20210113.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20071016.v' -> `./testsuite/example-20071016.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20140610.v' -> `./testsuite/example-20140610.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20150105.v' -> `./testsuite/example-20150105.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20210218.v' -> `./testsuite/example-20210218.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20120927.v' -> `./testsuite/bug-20120927.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20140723.v' -> `./testsuite/bug-20140723.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20140728.v' -> `./testsuite/bug-20140728.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20150924.v' -> `./testsuite/bug-20150924.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20150925.v' -> `./testsuite/bug-20150925.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20160218.v' -> `./testsuite/bug-20160218.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/bug-20200616.v' -> `./testsuite/bug-20200616.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20120205.v' -> `./testsuite/example-20120205.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20140221.v' -> `./testsuite/example-20140221.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20160218.v' -> `./testsuite/example-20160218.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20171018.v' -> `./testsuite/example-20171018.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20200428.v' -> `./testsuite/example-20200428.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/example-20200430.v' -> `./testsuite/example-20200430.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/testsuite/test-failures.v' -> `./testsuite/test-failures.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Plot.v' -> `./src/Plot.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Tactic.v' -> `./src/Tactic.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Tactic_bignum.v' -> `./src/Tactic_bignum.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Tactic_primfloat.v' -> `./src/Tactic_primfloat.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Tactics/Integral_helper.v' -> `./src/Tactics/Integral_helper.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Tactics/Interval_helper.v' -> `./src/Tactics/Interval_helper.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Tactics/Plot_helper.v' -> `./src/Tactics/Plot_helper.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Real/Taylor.v' -> `./src/Real/Taylor.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Real/Xreal.v' -> `./src/Real/Xreal.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Real/Xreal_derive.v' -> `./src/Real/Xreal_derive.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Poly/Basic_rec.v' -> `./src/Poly/Basic_rec.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Poly/Bound_quad.v' -> `./src/Poly/Bound_quad.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Poly/Datatypes.v' -> `./src/Poly/Datatypes.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Poly/Taylor_model.v' -> `./src/Poly/Taylor_model.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Poly/Taylor_model_sharp.v' -> `./src/Poly/Taylor_model_sharp.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Poly/Taylor_poly.v' -> `./src/Poly/Taylor_poly.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Poly/Bound.v' -> `./src/Poly/Bound.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Plot/plot.c' -> `./src/Plot/plot.c' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Plot/plot.py' -> `./src/Plot/plot.py' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Missing/Stdlib.v' -> `./src/Missing/Stdlib.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Missing/Coquelicot.v' -> `./src/Missing/Coquelicot.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Missing/MathComp.v' -> `./src/Missing/MathComp.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Interval/Float.v' -> `./src/Interval/Float.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Interval/Float_full.v' -> `./src/Interval/Float_full.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Interval/Interval.v' -> `./src/Interval/Interval.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Interval/Transcend.v' -> `./src/Interval/Transcend.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Interval/Interval_compl.v' -> `./src/Interval/Interval_compl.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Interval/Univariate_sig.v' -> `./src/Interval/Univariate_sig.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Integral/Integral.v' -> `./src/Integral/Integral.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Integral/Refine.v' -> `./src/Integral/Refine.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Integral/Bertrand.v' -> `./src/Integral/Bertrand.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Integral/Priority.v' -> `./src/Integral/Priority.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Generic.v' -> `./src/Float/Generic.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Generic_ops.v' -> `./src/Float/Generic_ops.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Generic_proof.v' -> `./src/Float/Generic_proof.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Primitive_ops.v' -> `./src/Float/Primitive_ops.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Sig.v' -> `./src/Float/Sig.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Specific_bigint.v' -> `./src/Float/Specific_bigint.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Specific_ops.v' -> `./src/Float/Specific_ops.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Specific_sig.v' -> `./src/Float/Specific_sig.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Specific_stdz.v' -> `./src/Float/Specific_stdz.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Float/Basic.v' -> `./src/Float/Basic.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Eval/Eval.v' -> `./src/Eval/Eval.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Eval/Reify.v' -> `./src/Eval/Reify.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Eval/Tree.v' -> `./src/Eval/Tree.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/src/Eval/Prog.v' -> `./src/Eval/Prog.v' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/misc/Dockerfile' -> `./misc/Dockerfile' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/misc/ci.md' -> `./misc/ci.md' `/gnu/store/yr9l6npk52645gvygv20xb9hi8l1iba6-coq-interval-4.3.0-checkout/misc/template.html' -> `./misc/template.html' phase `unpack' succeeded after 0.0 seconds starting phase `bootstrap' autoreconf: Entering directory `.' autoreconf: configure.in: not using Gettext autoreconf: running: aclocal --force aclocal: warning: autoconf input should be named 'configure.ac', not 'configure.in' configure.in:5: warning: prefer named diversions autoreconf: configure.in: tracing configure.in:5: warning: prefer named diversions autoreconf: configure.in: not using Libtool autoreconf: running: /gnu/store/b3ijxswrcsl3l4406aawbmby4nc0lc0b-autoconf-2.69/bin/autoconf --force configure.in:5: warning: prefer named diversions autoreconf: configure.in: not using Autoheader autoreconf: configure.in: not using Automake autoreconf: Leaving directory `.' phase `bootstrap' succeeded after 3.3 seconds starting phase `patch-usr-bin-file' phase `patch-usr-bin-file' succeeded after 0.0 seconds starting phase `patch-source-shebangs' patch-shebang: ./configure: changing `/bin/sh' to `/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin/sh' phase `patch-source-shebangs' succeeded after 0.0 seconds starting phase `fix-remake' phase `fix-remake' succeeded after 0.0 seconds starting phase `configure' source directory: "/tmp/guix-build-coq-interval-4.3.0.drv-0/source" (relative from build: ".") build directory: "/tmp/guix-build-coq-interval-4.3.0.drv-0/source" configure flags: ("CONFIG_SHELL=/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin/bash" "SHELL=/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin/bash" "--prefix=/gnu/store/n9abs0c9sa7hb45bg2qyqhn7xj0l52sp-coq-interval-4.3.0" "--enable-fast-install" "--build=arm-unknown-linux-gnueabihf" "COQUSERCONTRIB=/gnu/store/n9abs0c9sa7hb45bg2qyqhn7xj0l52sp-coq-interval-4.3.0/lib/coq/user-contrib") configure: WARNING: unrecognized options: --enable-fast-install checking for gcc... gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C compiler... yes checking whether gcc accepts -g... yes checking for gcc option to accept ISO C89... none needed checking how to run the C preprocessor... gcc -E checking for coqc... /gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin/coqc checking Coq version... 81302 checking for coqdep... /gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin/coqdep checking for coqdoc... /gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin/coqdoc checking for ocamlfind... /gnu/store/bw2a27zxsrbcagmzhqk0dcrflk1wxba3-ocaml-findlib-1.8.1/bin/ocamlfind checking for Flocq... yes checking for primitive floats... yes checking for Ssreflect... yes checking for Coquelicot... yes checking for Bignums... yes checking for native development files... yes checking for bytecode development files... yes checking for g++... g++ checking whether we are using the GNU C++ compiler... yes checking whether g++ accepts -g... yes configure: building remake... ld: /tmp/guix-build-coq-interval-4.3.0.drv-0/ccL3IiaA.o: in function `main': remake.cpp:(.text.startup+0x5c0): warning: the use of `tempnam' is dangerous, better use `mkstemp' === Summary === Installation directory /gnu/store/n9abs0c9sa7hb45bg2qyqhn7xj0l52sp-coq-interval-4.3.0/lib/coq/user-contrib Plot tactic native bytecode configure: creating ./config.status config.status: creating Remakefile configure: WARNING: unrecognized options: --enable-fast-install phase `configure' succeeded after 14.3 seconds starting phase `patch-generated-file-shebangs' phase `patch-generated-file-shebangs' succeeded after 0.0 seconds starting phase `build' Building src/Tactic_float.v Finished src/Tactic_float.v Building src/Tactic.vo Building src/Float/Sig.vo Building src/Float/Basic.vo Building src/Real/Xreal.vo Building src/Missing/Stdlib.vo File "./src/Missing/Stdlib.v", line 1085, characters 0-37: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Missing/Stdlib.vo File "./src/Real/Xreal.v", line 186, characters 0-31: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope XR_scope.". [undeclared-scope,deprecated] Finished src/Real/Xreal.vo Finished src/Float/Basic.vo Finished src/Float/Sig.vo Building src/Float/Specific_bigint.vo Building src/Float/Generic.vo Finished src/Float/Generic.vo Building src/Float/Generic_proof.vo File "./src/Float/Generic_proof.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Generic_proof.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Generic_proof.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Generic_proof.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Generic_proof.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Generic_proof.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] Finished src/Float/Generic_proof.vo Building src/Float/Specific_sig.vo Finished src/Float/Specific_sig.vo Finished src/Float/Specific_bigint.vo Building src/Float/Specific_ops.vo File "./src/Float/Specific_ops.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Specific_ops.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Specific_ops.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Specific_ops.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Specific_ops.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Float/Specific_ops.v", line 22, characters 0-47: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] Finished src/Float/Specific_ops.vo Building src/Interval/Float_full.vo Building src/Interval/Float.vo Building src/Interval/Interval.vo File "./src/Interval/Interval.v", line 21, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Interval/Interval.vo Finished src/Interval/Float.vo Building src/Interval/Transcend.vo File "./src/Interval/Transcend.v", line 52, characters 0-88: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] Finished src/Interval/Transcend.vo Finished src/Interval/Float_full.vo Building src/Tactic_float.vo Building src/Float/Primitive_ops.vo File "./src/Float/Primitive_ops.v", line 137, characters 31-48: Warning: Notation "_ == _" is deprecated since 8.13. use infix =? instead [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 139, characters 31-44: Warning: Notation "_ == _" is deprecated since 8.13. use infix =? instead [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 206, characters 14-21: Warning: Notation "_ < _" is deprecated since 8.13. use infix = _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Missing/MathComp.vo Building src/Real/Taylor.vo File "./src/Real/Taylor.v", line 24, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Real/Taylor.vo File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 25, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Interval/Interval_compl.vo Building src/Missing/Coquelicot.vo File "./src/Missing/Coquelicot.v", line 22, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 494, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 497, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 515, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 529, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 532, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 551, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] Finished src/Missing/Coquelicot.vo Building src/Poly/Taylor_model.vo Building src/Interval/Univariate_sig.vo Finished src/Interval/Univariate_sig.vo Building src/Poly/Bound.vo Building src/Poly/Datatypes.vo Building src/Poly/Basic_rec.vo File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Basic_rec.vo File "./src/Poly/Datatypes.v", line 24, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 26, characters 0-31: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 852, characters 0-70: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope ipoly_scope.". [undeclared-scope,deprecated] File "./src/Poly/Datatypes.v", line 989, characters 0-34: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope ipoly_scope.". [undeclared-scope,deprecated] Finished src/Poly/Datatypes.vo File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Bound.vo Building src/Poly/Bound_quad.vo File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Bound_quad.vo Building src/Poly/Taylor_model_sharp.vo Building src/Poly/Taylor_poly.vo File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Taylor_poly.vo Building src/Real/Xreal_derive.vo Finished src/Real/Xreal_derive.vo File "./src/Poly/Taylor_model_sharp.v", line 25, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 1348, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1357, characters 2-76: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1580, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1682, characters 6-32: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1720, characters 4-48: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1742, characters 4-53: Warning: Duplicate clear of X [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1751, characters 2-28: Warning: Duplicate clear of E0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1853, characters 4-48: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1961, characters 4-48: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2053, characters 2-51: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2168, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2310, characters 4-37: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2421, characters 2-189: Warning: Duplicate clear of X [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2424, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] Finished src/Poly/Taylor_model_sharp.vo File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Taylor_model.vo File "./src/Eval/Eval.v", line 23, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Eval/Eval.v", line 522, characters 0-25: Warning: Duplicate clear of H [duplicate-clear,ssr] Finished src/Eval/Eval.vo Building src/Eval/Reify.vo Finished src/Eval/Reify.vo Building src/Integral/Bertrand.vo File "./src/Integral/Bertrand.v", line 3, characters 0-53: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Integral/Bertrand.vo Building src/Integral/Integral.vo File "./src/Integral/Integral.v", line 21, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Integral/Integral.v", line 22, characters 0-64: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Integral.v", line 22, characters 0-64: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Integral.v", line 22, characters 0-64: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Integral.v", line 22, characters 0-64: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Integral.v", line 22, characters 0-64: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Integral.v", line 22, characters 0-64: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Integral.v", line 583, characters 2-57: Warning: Duplicate clear of HPint [duplicate-clear,ssr] File "./src/Integral/Integral.v", line 742, characters 2-57: Warning: Duplicate clear of HPint [duplicate-clear,ssr] Finished src/Integral/Integral.vo Building src/Integral/Refine.vo Building src/Integral/Priority.vo File "./src/Integral/Priority.v", line 21, characters 0-62: Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Priority.v", line 21, characters 0-62: Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Priority.v", line 21, characters 0-62: Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Priority.v", line 21, characters 0-62: Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Priority.v", line 21, characters 0-62: Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Priority.v", line 21, characters 0-62: Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing] File "./src/Integral/Priority.v", line 527, characters 0-118: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] Finished src/Integral/Priority.vo File "./src/Integral/Refine.v", line 21, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Integral/Refine.vo Building src/Tactics/Interval_helper.vo Finished src/Tactics/Interval_helper.vo File "./src/Tactics/Integral_helper.v", line 22, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Tactics/Integral_helper.vo Building src/Tactics/Plot_helper.vo Finished src/Tactics/Plot_helper.vo File "./src/Tactic.v", line 22, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Tactic.vo Building src/Float/Generic_ops.vo Finished src/Float/Generic_ops.vo Building src/Float/Specific_stdz.vo Finished src/Float/Specific_stdz.vo Building src/Plot/interval_plot.ml Finished src/Plot/interval_plot.ml Building src/Plot/interval_plot.cmxs File "src/Plot/plot.c", line 16, characters 65-96: Alert deprecated: Coqlib.gen_reference_in_modules Please use Coqlib.lib_ref Finished src/Plot/interval_plot.cmxs Building src/Plot/interval_plot.cmo File "src/Plot/plot.c", line 16, characters 65-96: Alert deprecated: Coqlib.gen_reference_in_modules Please use Coqlib.lib_ref Finished src/Plot/interval_plot.cmo Building src/Plot.vo Finished src/Plot.vo Building all Finished all phase `build' succeeded after 351.4 seconds starting phase `check' Building check Finished check phase `check' succeeded after 85.1 seconds starting phase `install' Building install Finished install phase `install' succeeded after 0.3 seconds starting phase `patch-shebangs' phase `patch-shebangs' succeeded after 0.0 seconds starting phase `strip' stripping binaries in "/gnu/store/n9abs0c9sa7hb45bg2qyqhn7xj0l52sp-coq-interval-4.3.0/lib" with "strip" and flags ("--strip-debug" "--enable-deterministic-archives") phase `strip' succeeded after 0.0 seconds starting phase `validate-runpath' validating RUNPATH of 1 binaries in "/gnu/store/n9abs0c9sa7hb45bg2qyqhn7xj0l52sp-coq-interval-4.3.0/lib"... phase `validate-runpath' succeeded after 0.0 seconds starting phase `validate-documentation-location' phase `validate-documentation-location' succeeded after 0.0 seconds starting phase `delete-info-dir-file' phase `delete-info-dir-file' succeeded after 0.0 seconds starting phase `patch-dot-desktop-files' phase `patch-dot-desktop-files' succeeded after 0.0 seconds starting phase `install-license-files' installing 1 license files from '.' phase `install-license-files' succeeded after 0.0 seconds starting phase `reset-gzip-timestamps' phase `reset-gzip-timestamps' succeeded after 0.0 seconds starting phase `compress-documentation' phase `compress-documentation' succeeded after 0.0 seconds