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/5cqcyfz3941q5in3rj2ny9hngmaxhih3-autoconf-2.69/bin:/gnu/store/rxp211xl23pna06mdcffcic6fkkqkwa6-automake-1.16.5/bin:/gnu/store/cf97w7kzgn8digz7cl831pn1hlmyxhqa-ocaml-4.14.1/bin:/gnu/store/mxb4gi3xvghny9psxqi3xmziqnkbiyli-which-2.21/bin:/gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-coq-8.17.1/bin:/gnu/store/4vs95giv3b18mr7422adf7r7l917ad41-tar-1.34/bin:/gnu/store/cmp43qav05qdfx8l7am699nngvrcymmf-gzip-1.12/bin:/gnu/store/jyj45lhbdv3ck62qvblhv4rdygszjv3w-bzip2-1.0.8/bin:/gnu/store/54jpx6ymfslv25n1h92ls72z87r9ja2i-file-5.44/bin:/gnu/store/9raglzgr029gila3bl3832h2ry564ayi-diffutils-3.8/bin:/gnu/store/gpcv5f7wsw56kysrlnqpq4g4ij37j1aj-patch-2.7.6/bin:/gnu/store/fs50ippbz10zl55zwwxl04zfvlgjmr7s-findutils-4.9.0/bin:/gnu/store/cdwc7qmxhfmjhhhzrvbhmwal65sshm6z-gawk-5.2.1/bin:/gnu/store/ams1v0vks47c950hym908a4lismsdl6z-sed-4.8/bin:/gnu/store/amm36qk60pnyl3v0vbl72w6agi5xkh07-grep-3.8/bin:/gnu/store/la6c6k6h32bddrf1171n0dp8dm47k656-xz-5.2.8/bin:/gnu/store/g3pv7a535y9h5dsvzv5zr669zzd1hx73-coreutils-9.1/bin:/gnu/store/ly36q12ji4l2fr2kpqf2api2dvg0rmfa-make-4.3/bin:/gnu/store/vza0n6gb01lbc9cgwx2hygvq15qiczn6-bash-minimal-5.1.16/bin:/gnu/store/lymlgi1qapfyr9jxmps1x95qwfgrwmgd-ld-wrapper-0/bin:/gnu/store/b4x9dk21q93na0cg28xmnis3g943nc3p-binutils-2.38/bin:/gnu/store/7pnvpswg5khkrj7gdaq4b5cipr9z2j00-gcc-11.3.0/bin:/gnu/store/r6gm2il1kkyyb6k1881lwilcij2kmbcq-glibc-2.35/bin:/gnu/store/r6gm2il1kkyyb6k1881lwilcij2kmbcq-glibc-2.35/sbin'
environment variable `ACLOCAL_PATH' set to `/gnu/store/rxp211xl23pna06mdcffcic6fkkqkwa6-automake-1.16.5/share/aclocal'
environment variable `OCAMLPATH' set to `/gnu/store/cf97w7kzgn8digz7cl831pn1hlmyxhqa-ocaml-4.14.1/lib/ocaml:/gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-coq-8.17.1/lib/ocaml:/gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-coq-8.17.1/lib/ocaml/site-lib'
environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-coq-8.17.1/lib/ocaml/site-lib/stublibs'
environment variable `COQPATH' set to `/gnu/store/nlqvixvyv31wnwa3gwy618639kdndf2w-coq-mathcomp-1.19.0/lib/coq/user-contrib'
environment variable `BASH_LOADABLES_PATH' unset
environment variable `C_INCLUDE_PATH' set to `/gnu/store/jyj45lhbdv3ck62qvblhv4rdygszjv3w-bzip2-1.0.8/include:/gnu/store/54jpx6ymfslv25n1h92ls72z87r9ja2i-file-5.44/include:/gnu/store/cdwc7qmxhfmjhhhzrvbhmwal65sshm6z-gawk-5.2.1/include:/gnu/store/la6c6k6h32bddrf1171n0dp8dm47k656-xz-5.2.8/include:/gnu/store/ly36q12ji4l2fr2kpqf2api2dvg0rmfa-make-4.3/include:/gnu/store/b4x9dk21q93na0cg28xmnis3g943nc3p-binutils-2.38/include:/gnu/store/7pnvpswg5khkrj7gdaq4b5cipr9z2j00-gcc-11.3.0/include:/gnu/store/r6gm2il1kkyyb6k1881lwilcij2kmbcq-glibc-2.35/include:/gnu/store/4w2igc2gchw1xwh1gb1phgbfjy06ram8-linux-libre-headers-5.15.49/include'
environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/jyj45lhbdv3ck62qvblhv4rdygszjv3w-bzip2-1.0.8/include:/gnu/store/54jpx6ymfslv25n1h92ls72z87r9ja2i-file-5.44/include:/gnu/store/cdwc7qmxhfmjhhhzrvbhmwal65sshm6z-gawk-5.2.1/include:/gnu/store/la6c6k6h32bddrf1171n0dp8dm47k656-xz-5.2.8/include:/gnu/store/ly36q12ji4l2fr2kpqf2api2dvg0rmfa-make-4.3/include:/gnu/store/b4x9dk21q93na0cg28xmnis3g943nc3p-binutils-2.38/include:/gnu/store/7pnvpswg5khkrj7gdaq4b5cipr9z2j00-gcc-11.3.0/include/c++:/gnu/store/7pnvpswg5khkrj7gdaq4b5cipr9z2j00-gcc-11.3.0/include:/gnu/store/r6gm2il1kkyyb6k1881lwilcij2kmbcq-glibc-2.35/include:/gnu/store/4w2igc2gchw1xwh1gb1phgbfjy06ram8-linux-libre-headers-5.15.49/include'
environment variable `LIBRARY_PATH' set to `/gnu/store/cf97w7kzgn8digz7cl831pn1hlmyxhqa-ocaml-4.14.1/lib:/gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-coq-8.17.1/lib:/gnu/store/nlqvixvyv31wnwa3gwy618639kdndf2w-coq-mathcomp-1.19.0/lib:/gnu/store/jyj45lhbdv3ck62qvblhv4rdygszjv3w-bzip2-1.0.8/lib:/gnu/store/54jpx6ymfslv25n1h92ls72z87r9ja2i-file-5.44/lib:/gnu/store/cdwc7qmxhfmjhhhzrvbhmwal65sshm6z-gawk-5.2.1/lib:/gnu/store/la6c6k6h32bddrf1171n0dp8dm47k656-xz-5.2.8/lib:/gnu/store/b4x9dk21q93na0cg28xmnis3g943nc3p-binutils-2.38/lib:/gnu/store/r6gm2il1kkyyb6k1881lwilcij2kmbcq-glibc-2.35/lib:/gnu/store/s0cscf8lbg5ipm7gwz41jxcfwv43jzsp-glibc-2.35-static/lib:/gnu/store/zjm02y5r97anpgngbvfvn7mfd2sh9d78-glibc-utf8-locales-2.35/lib'
environment variable `GUIX_LOCPATH' set to `/gnu/store/zjm02y5r97anpgngbvfvn7mfd2sh9d78-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/_CoqProject' -> `./_CoqProject'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/INSTALL.md' -> `./INSTALL.md'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/NEWS.md' -> `./NEWS.md'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.gitlab-ci.yml' -> `./.gitlab-ci.yml'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/COPYING' -> `./COPYING'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.gitattributes' -> `./.gitattributes'
`/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/Remakefile.in' -> `./Remakefile.in'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/remake.cpp' -> `./remake.cpp'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/opam' -> `./opam'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/.mailmap' -> `./.mailmap'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/misc/Dockerfile' -> `./misc/Dockerfile'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/misc/ci.md' -> `./misc/ci.md'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/examples/Wasow.v' -> `./examples/Wasow.v'
`/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/BacS2013.v' -> `./examples/BacS2013.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/Bessel.v' -> `./examples/Bessel.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/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/Hierarchy.v' -> `./theories/Hierarchy.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/Markov.v' -> `./theories/Markov.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/PSeries.v' -> `./theories/PSeries.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/Continuity.v' -> `./theories/Continuity.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/Lub.v' -> `./theories/Lub.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/ElemFct.v' -> `./theories/ElemFct.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/Compactness.v' -> `./theories/Compactness.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/Seq_fct.v' -> `./theories/Seq_fct.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/RInt_gen.v' -> `./theories/RInt_gen.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/Rcomplements.v' -> `./theories/Rcomplements.v'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/RInt.v' -> `./theories/RInt.v'
`/gnu/store/kcqnwqj7wafy6xb4bmprm8q861pqh0j4-coq-coquelicot-3.4.1-checkout/theories/AutoDerive.v' -> `./theories/AutoDerive.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/5cqcyfz3941q5in3rj2ny9hngmaxhih3-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.1 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/vza0n6gb01lbc9cgwx2hygvq15qiczn6-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/vza0n6gb01lbc9cgwx2hygvq15qiczn6-bash-minimal-5.1.16/bin/bash" "SHELL=/gnu/store/vza0n6gb01lbc9cgwx2hygvq15qiczn6-bash-minimal-5.1.16/bin/bash" "--prefix=/gnu/store/xwh9xijphmc45nqd5v11xvkkzm3gh0sq-coq-coquelicot-3.4.1" "--enable-fast-install" "--build=powerpc64le-unknown-linux-gnu" "COQUSERCONTRIB=/gnu/store/xwh9xijphmc45nqd5v11xvkkzm3gh0sq-coq-coquelicot-3.4.1/lib/coq/user-contrib")
configure: WARNING: unrecognized options: --enable-fast-install
checking for coqc... /gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-coq-8.17.1/bin/coqc
checking for coqdep... /gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-coq-8.17.1/bin/coqdep
checking for coqdoc... /gnu/store/hfz9ym77anr0cq2vqzji3l9h8803n6c3-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/ccbAkMBc.o: in function `main':
remake.cpp:(.text.startup+0xba4): 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 4.7 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 95.4 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 12.4 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/xwh9xijphmc45nqd5v11xvkkzm3gh0sq-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/xwh9xijphmc45nqd5v11xvkkzm3gh0sq-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