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/3ddp6zriaxnqxb7qig1y2n0gqfmx7qid-autoconf-2.69/bin:/gnu/store/g8mv598r970cn82frwsz5qrm0b2vdy4a-automake-1.16.5/bin:/gnu/store/m8hs4qbkzs49qwh3q0r7a6az0d8332wp-ocaml-4.14.1/bin:/gnu/store/6h9mxys5lbbh9k6av74xq88i2d8h946z-which-2.21/bin:/gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/bin:/gnu/store/54cg8d0xnnbd6n40hg2smaqfafz2km79-tar-1.34/bin:/gnu/store/jjazmdlhvqh0yxzk2qwbl13hflnv9jj6-gzip-1.12/bin:/gnu/store/nbalv23p48cdwf9m651s4yagcacsay2l-bzip2-1.0.8/bin:/gnu/store/q68rwxvi47zkw29r7ycg6a4jg2lpky1d-file-5.44/bin:/gnu/store/8315h8gqhd9l5a593g2j09rby3zs6nds-diffutils-3.8/bin:/gnu/store/10dp5a06lqg5kcbl77wdl2sfhrjchagk-patch-2.7.6/bin:/gnu/store/kj4h8gvidm64l0p8k4q9knhprvmajcrp-findutils-4.9.0/bin:/gnu/store/vjw939r5cjccbmdcjxg34lbpqrcjpnwb-gawk-5.2.1/bin:/gnu/store/9a4hc78kh956srjzr00cwpql1pavfk7d-sed-4.8/bin:/gnu/store/acf2bj4w033i0b1v5bcws46gc85x4dm4-grep-3.8/bin:/gnu/store/qbhy2zzqzzfqbr7s59y513bxd1w22wzb-xz-5.2.8/bin:/gnu/store/n1jykk68ml8y9zm4ybygyfdjs3rw6bjs-coreutils-9.1/bin:/gnu/store/0mfya6ws3bk273wrwdgwlyv8j8cikkkg-make-4.3/bin:/gnu/store/id0knspwhrd51wrg2nbx2pw3ajz36ngg-bash-minimal-5.1.16/bin:/gnu/store/czfalsz0yhfl1m64k2s5ag9h2w4wxz95-ld-wrapper-0/bin:/gnu/store/1b5sk5dgk5y3hzczd8bq1micm5c7d1vj-binutils-2.38/bin:/gnu/store/9c54kwmmb31zzjxbcfi2z6070mqk73fy-gcc-11.3.0/bin:/gnu/store/a19xbynxc3sg25xpkwmx7g0mdl7g31hx-glibc-2.35/bin:/gnu/store/a19xbynxc3sg25xpkwmx7g0mdl7g31hx-glibc-2.35/sbin' environment variable `ACLOCAL_PATH' set to `/gnu/store/g8mv598r970cn82frwsz5qrm0b2vdy4a-automake-1.16.5/share/aclocal' environment variable `OCAMLPATH' set to `/gnu/store/m8hs4qbkzs49qwh3q0r7a6az0d8332wp-ocaml-4.14.1/lib/ocaml:/gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/lib/ocaml:/gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/lib/ocaml/site-lib' environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/lib/ocaml/site-lib/stublibs' environment variable `COQPATH' set to `/gnu/store/qmaxk1qrrmnb20i63dfd2cllcs8p9jm6-coq-mathcomp-1.19.0/lib/coq/user-contrib' environment variable `BASH_LOADABLES_PATH' unset environment variable `C_INCLUDE_PATH' set to `/gnu/store/nbalv23p48cdwf9m651s4yagcacsay2l-bzip2-1.0.8/include:/gnu/store/q68rwxvi47zkw29r7ycg6a4jg2lpky1d-file-5.44/include:/gnu/store/vjw939r5cjccbmdcjxg34lbpqrcjpnwb-gawk-5.2.1/include:/gnu/store/qbhy2zzqzzfqbr7s59y513bxd1w22wzb-xz-5.2.8/include:/gnu/store/0mfya6ws3bk273wrwdgwlyv8j8cikkkg-make-4.3/include:/gnu/store/1b5sk5dgk5y3hzczd8bq1micm5c7d1vj-binutils-2.38/include:/gnu/store/9c54kwmmb31zzjxbcfi2z6070mqk73fy-gcc-11.3.0/include:/gnu/store/a19xbynxc3sg25xpkwmx7g0mdl7g31hx-glibc-2.35/include:/gnu/store/64svgy8g04741kvr5sq60mp568ygsqfi-linux-libre-headers-5.15.49/include' environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/nbalv23p48cdwf9m651s4yagcacsay2l-bzip2-1.0.8/include:/gnu/store/q68rwxvi47zkw29r7ycg6a4jg2lpky1d-file-5.44/include:/gnu/store/vjw939r5cjccbmdcjxg34lbpqrcjpnwb-gawk-5.2.1/include:/gnu/store/qbhy2zzqzzfqbr7s59y513bxd1w22wzb-xz-5.2.8/include:/gnu/store/0mfya6ws3bk273wrwdgwlyv8j8cikkkg-make-4.3/include:/gnu/store/1b5sk5dgk5y3hzczd8bq1micm5c7d1vj-binutils-2.38/include:/gnu/store/9c54kwmmb31zzjxbcfi2z6070mqk73fy-gcc-11.3.0/include/c++:/gnu/store/9c54kwmmb31zzjxbcfi2z6070mqk73fy-gcc-11.3.0/include:/gnu/store/a19xbynxc3sg25xpkwmx7g0mdl7g31hx-glibc-2.35/include:/gnu/store/64svgy8g04741kvr5sq60mp568ygsqfi-linux-libre-headers-5.15.49/include' environment variable `LIBRARY_PATH' set to `/gnu/store/m8hs4qbkzs49qwh3q0r7a6az0d8332wp-ocaml-4.14.1/lib:/gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/lib:/gnu/store/qmaxk1qrrmnb20i63dfd2cllcs8p9jm6-coq-mathcomp-1.19.0/lib:/gnu/store/nbalv23p48cdwf9m651s4yagcacsay2l-bzip2-1.0.8/lib:/gnu/store/q68rwxvi47zkw29r7ycg6a4jg2lpky1d-file-5.44/lib:/gnu/store/vjw939r5cjccbmdcjxg34lbpqrcjpnwb-gawk-5.2.1/lib:/gnu/store/qbhy2zzqzzfqbr7s59y513bxd1w22wzb-xz-5.2.8/lib:/gnu/store/1b5sk5dgk5y3hzczd8bq1micm5c7d1vj-binutils-2.38/lib:/gnu/store/a19xbynxc3sg25xpkwmx7g0mdl7g31hx-glibc-2.35/lib:/gnu/store/s2sl8i4m58xyl9d34lspx8d82nlxlz79-glibc-2.35-static/lib:/gnu/store/4yq91i7db97yvn7yw3gghlraacllzvrw-glibc-utf8-locales-2.35/lib' environment variable `GUIX_LOCPATH' set to `/gnu/store/4yq91i7db97yvn7yw3gghlraacllzvrw-glibc-utf8-locales-2.35/lib/locale' phase `set-paths' succeeded after 0.0 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/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.mailmap' -> `./.mailmap' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/configure.in' -> `./configure.in' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/README.md' -> `./README.md' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/INSTALL.md' -> `./INSTALL.md' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/opam' -> `./opam' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.gitlab-ci.yml' -> `./.gitlab-ci.yml' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/remake.cpp' -> `./remake.cpp' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.gitattributes' -> `./.gitattributes' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.gitignore' -> `./.gitignore' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/_CoqProject' -> `./_CoqProject' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/Remakefile.in' -> `./Remakefile.in' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/NEWS.md' -> `./NEWS.md' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/COPYING' -> `./COPYING' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/misc/ci.md' -> `./misc/ci.md' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/misc/Dockerfile' -> `./misc/Dockerfile' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/examples/BacS2013_bonus.v' -> `./examples/BacS2013_bonus.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/examples/DAlembert.v' -> `./examples/DAlembert.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/examples/BacS2013.v' -> `./examples/BacS2013.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/examples/Bessel.v' -> `./examples/Bessel.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/examples/Wasow.v' -> `./examples/Wasow.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Derive_2d.v' -> `./theories/Derive_2d.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Lim_seq.v' -> `./theories/Lim_seq.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Series.v' -> `./theories/Series.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/RInt_analysis.v' -> `./theories/RInt_analysis.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Coquelicot.v' -> `./theories/Coquelicot.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Hierarchy.v' -> `./theories/Hierarchy.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/AutoDerive.v' -> `./theories/AutoDerive.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Complex.v' -> `./theories/Complex.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/RInt_gen.v' -> `./theories/RInt_gen.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Continuity.v' -> `./theories/Continuity.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Iter.v' -> `./theories/Iter.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Compactness.v' -> `./theories/Compactness.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Lub.v' -> `./theories/Lub.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/ElemFct.v' -> `./theories/ElemFct.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/SF_seq.v' -> `./theories/SF_seq.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Equiv.v' -> `./theories/Equiv.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Markov.v' -> `./theories/Markov.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/KHInt.v' -> `./theories/KHInt.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Derive.v' -> `./theories/Derive.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Rbar.v' -> `./theories/Rbar.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/PSeries.v' -> `./theories/PSeries.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Seq_fct.v' -> `./theories/Seq_fct.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/Rcomplements.v' -> `./theories/Rcomplements.v' `/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/RInt.v' -> `./theories/RInt.v' 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/3ddp6zriaxnqxb7qig1y2n0gqfmx7qid-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 2.8 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/id0knspwhrd51wrg2nbx2pw3ajz36ngg-bash-minimal-5.1.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-coquelicot-3.4.1.drv-0/source" (relative from build: ".") build directory: "/tmp/guix-build-coq-coquelicot-3.4.1.drv-0/source" configure flags: ("CONFIG_SHELL=/gnu/store/id0knspwhrd51wrg2nbx2pw3ajz36ngg-bash-minimal-5.1.16/bin/bash" "SHELL=/gnu/store/id0knspwhrd51wrg2nbx2pw3ajz36ngg-bash-minimal-5.1.16/bin/bash" "--prefix=/gnu/store/6m1gjr9czmjgvx87fp10wm7y0axndll7-coq-coquelicot-3.4.1" "--enable-fast-install" "--build=aarch64-unknown-linux-gnu" "COQUSERCONTRIB=/gnu/store/6m1gjr9czmjgvx87fp10wm7y0axndll7-coq-coquelicot-3.4.1/lib/coq/user-contrib") configure: WARNING: unrecognized options: --enable-fast-install checking for coqc... /gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/bin/coqc checking for coqdep... /gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/bin/coqdep checking for coqdoc... /gnu/store/nfc8k0l56ch0s3g7xc04a31p9jj4bsvb-coq-8.17.1/bin/coqdoc checking for SSReflect... yes checking for g++... g++ 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 g++ accepts -g... yes configure: building remake... ld: /tmp/guix-build-coq-coquelicot-3.4.1.drv-0/ccTyMw1V.o: in function `main': remake.cpp:(.text.startup+0x724): warning: the use of `tempnam' is dangerous, better use `mkstemp' configure: creating ./config.status config.status: creating Remakefile configure: WARNING: unrecognized options: --enable-fast-install phase `configure' succeeded after 11.6 seconds starting phase `patch-generated-file-shebangs' phase `patch-generated-file-shebangs' succeeded after 0.0 seconds starting phase `build' Building theories/AutoDerive.vo Building theories/Continuity.vo Building theories/Compactness.vo Building theories/Rcomplements.vo File "./theories/Rcomplements.v", line 997, characters 10-19: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 997, characters 10-19: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 997, characters 10-19: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./theories/Rcomplements.v", line 1346, characters 0-21: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished theories/Rcomplements.vo Finished theories/Compactness.vo Building theories/Hierarchy.vo Building theories/Iter.vo Finished theories/Iter.vo Building theories/Lub.vo Building theories/Markov.vo File "./theories/Markov.v", line 106, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Markov.v", line 106, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Markov.v", line 106, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Markov.v", line 139, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Markov.v", line 139, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Markov.v", line 139, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] Finished theories/Markov.vo Building theories/Rbar.vo File "./theories/Rbar.v", line 51, characters 0-27: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Rbar.v", line 570, characters 10-26: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition,deprecated] File "./theories/Rbar.v", line 570, characters 10-26: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition,deprecated] File "./theories/Rbar.v", line 570, characters 10-26: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition,deprecated] Finished theories/Rbar.vo File "./theories/Lub.v", line 24, characters 0-40: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Lub.vo File "./theories/Hierarchy.v", line 24, characters 0-49: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Hierarchy.v", line 49, characters 0-141: Warning: A coercion will be introduced instead of an instance in future versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq < 8.17). Beware that the default locality for '::' is #[export], as opposed to #[global] for ':>' currently. Add an explicit #[global] attribute to the field if you need to keep the current behavior. For example: "Class foo := { #[global] field :: bar }." [future-coercion-class-field,records] File "./theories/Hierarchy.v", line 54, characters 0-138: Warning: A coercion will be introduced instead of an instance in future versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq < 8.17). Beware that the default locality for '::' is #[export], as opposed to #[global] for ':>' currently. Add an explicit #[global] attribute to the field if you need to keep the current behavior. For example: "Class foo := { #[global] field :: bar }." [future-coercion-class-field,records] File "./theories/Hierarchy.v", line 5574, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Hierarchy.v", line 5574, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Hierarchy.v", line 5574, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] Finished theories/Hierarchy.vo Building theories/Lim_seq.vo File "./theories/Lim_seq.v", line 24, characters 0-54: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Lim_seq.v", line 2542, characters 27-36: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Lim_seq.v", line 2542, characters 27-36: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Lim_seq.v", line 2542, characters 27-36: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Lim_seq.v", line 2543, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Lim_seq.v", line 2543, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Lim_seq.v", line 2543, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] Finished theories/Lim_seq.vo File "./theories/Continuity.v", line 24, characters 0-63: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Continuity.vo Building theories/Derive.vo Building theories/Equiv.vo File "./theories/Equiv.v", line 24, characters 0-43: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Equiv.v", line 454, characters 28-37: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 454, characters 28-37: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 454, characters 28-37: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 454, characters 28-37: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 454, characters 28-37: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 454, characters 28-37: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 454, characters 28-37: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 507, characters 20-29: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 507, characters 20-29: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 507, characters 20-29: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 507, characters 20-29: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 507, characters 20-29: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 507, characters 20-29: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/Equiv.v", line 507, characters 20-29: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] Finished theories/Equiv.vo File "./theories/Derive.v", line 26, characters 0-73: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Derive.vo Building theories/Derive_2d.vo Finished theories/Derive_2d.vo Building theories/ElemFct.vo Building theories/PSeries.vo Building theories/Seq_fct.vo Building theories/Series.vo File "./theories/Series.v", line 24, characters 0-51: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Series.vo File "./theories/Seq_fct.v", line 23, characters 0-80: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Seq_fct.vo File "./theories/PSeries.v", line 24, characters 0-88: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/PSeries.v", line 1237, characters 21-29: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] File "./theories/PSeries.v", line 1237, characters 21-29: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] File "./theories/PSeries.v", line 1237, characters 21-29: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] Finished theories/PSeries.vo Building theories/RInt.vo Building theories/SF_seq.vo File "./theories/SF_seq.v", line 24, characters 0-47: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/SF_seq.v", line 141, characters 11-18: Warning: Notation le_pred is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.pred_le_mono instead. [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 141, characters 11-18: Warning: Notation le_pred is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.pred_le_mono instead. [deprecated-syntactic-definition,deprecated] Finished theories/SF_seq.vo File "./theories/RInt.v", line 25, characters 0-80: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/RInt.v", line 311, characters 18-27: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 311, characters 18-27: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 311, characters 18-27: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2858, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2858, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2858, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] Finished theories/RInt.vo Building theories/RInt_analysis.vo File "./theories/RInt_analysis.v", line 27, characters 0-66: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/RInt_analysis.vo File "./theories/ElemFct.v", line 24, characters 0-96: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/ElemFct.v", line 230, characters 11-27: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition,deprecated] File "./theories/ElemFct.v", line 230, characters 11-27: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition,deprecated] File "./theories/ElemFct.v", line 230, characters 11-27: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition,deprecated] File "./theories/ElemFct.v", line 615, characters 39-54: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] File "./theories/ElemFct.v", line 615, characters 39-54: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition,deprecated] Finished theories/ElemFct.vo Finished theories/AutoDerive.vo Building theories/Complex.vo File "./theories/Complex.v", line 24, characters 0-61: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Complex.v", line 71, characters 0-29: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope C_scope.". [undeclared-scope,deprecated] File "./theories/Complex.v", line 828, characters 0-135: Warning: Ignoring canonical projection to C by ModuleSpace.sort in C_R_ModuleSpace: redundant with C_ModuleSpace [redundant-canonical-projection,typechecker] File "./theories/Complex.v", line 831, characters 0-167: Warning: Ignoring canonical projection to C by NormedModuleAux.sort in C_R_NormedModuleAux: redundant with C_NormedModuleAux [redundant-canonical-projection,typechecker] File "./theories/Complex.v", line 834, characters 0-113: Warning: Ignoring canonical projection to C by NormedModule.sort in C_R_NormedModule: redundant with C_NormedModule [redundant-canonical-projection,typechecker] File "./theories/Complex.v", line 911, characters 0-175: Warning: Ignoring canonical projection to C by CompleteNormedModule.sort in C_R_CompleteNormedModule: redundant with C_CompleteNormedModule [redundant-canonical-projection,typechecker] Finished theories/Complex.vo Building theories/Coquelicot.vo Building theories/RInt_gen.vo File "./theories/RInt_gen.v", line 24, characters 0-88: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/RInt_gen.vo File "./theories/Coquelicot.v", line 274, characters 0-52: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Coquelicot.vo Building theories/KHInt.vo Finished theories/KHInt.vo Building all Finished all phase `build' succeeded after 151.7 seconds starting phase `check' Building examples/BacS2013.vo File "./examples/BacS2013.v", line 24, characters 0-112: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished examples/BacS2013.vo Building examples/BacS2013_bonus.vo File "./examples/BacS2013_bonus.v", line 24, characters 0-62: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished examples/BacS2013_bonus.vo Building examples/Bessel.vo File "./examples/Bessel.v", line 24, characters 0-100: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./examples/Bessel.v", line 324, characters 2-15: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 339, characters 2-15: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 483, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 483, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 488, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 488, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 488, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 488, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 496, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 496, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 496, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 496, characters 2-31: Warning: "auto with *" was used through the default "intuition_solver" tactic. This will be replaced by just "auto" in the future. [intuition-auto-with-star,deprecated] File "./examples/Bessel.v", line 531, characters 27-35: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] File "./examples/Bessel.v", line 531, characters 27-35: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] File "./examples/Bessel.v", line 531, characters 27-35: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] File "./examples/Bessel.v", line 545, characters 27-35: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] File "./examples/Bessel.v", line 545, characters 27-35: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] File "./examples/Bessel.v", line 545, characters 27-35: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition,deprecated] Finished examples/Bessel.vo Building examples/DAlembert.vo Finished examples/DAlembert.vo Building check Finished check phase `check' succeeded after 19.0 seconds starting phase `install' Building install Finished install phase `install' succeeded after 0.0 seconds starting phase `patch-shebangs' phase `patch-shebangs' succeeded after 0.0 seconds starting phase `strip' stripping binaries in "/gnu/store/6m1gjr9czmjgvx87fp10wm7y0axndll7-coq-coquelicot-3.4.1/lib" with "strip" and flags ("--strip-unneeded" "--enable-deterministic-archives") phase `strip' succeeded after 0.0 seconds starting phase `validate-runpath' validating RUNPATH of 0 binaries in "/gnu/store/6m1gjr9czmjgvx87fp10wm7y0axndll7-coq-coquelicot-3.4.1/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 `make-dynamic-linker-cache' phase `make-dynamic-linker-cache' 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