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/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'
environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/stublibs'
environment variable `COQPATH' set to `/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/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/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/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/.mailmap' -> `./.mailmap'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/INSTALL.md' -> `./INSTALL.md'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/NEWS.md' -> `./NEWS.md'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/README.md' -> `./README.md'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/Remakefile.in' -> `./Remakefile.in'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/configure.in' -> `./configure.in'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/COPYING' -> `./COPYING'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/remake.cpp' -> `./remake.cpp'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/AutoDerive.v' -> `./theories/AutoDerive.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Compactness.v' -> `./theories/Compactness.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Complex.v' -> `./theories/Complex.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Continuity.v' -> `./theories/Continuity.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Coquelicot.v' -> `./theories/Coquelicot.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Derive.v' -> `./theories/Derive.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Derive_2d.v' -> `./theories/Derive_2d.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/ElemFct.v' -> `./theories/ElemFct.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Equiv.v' -> `./theories/Equiv.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Hierarchy.v' -> `./theories/Hierarchy.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Iter.v' -> `./theories/Iter.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/KHInt.v' -> `./theories/KHInt.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Lim_seq.v' -> `./theories/Lim_seq.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Lub.v' -> `./theories/Lub.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Markov.v' -> `./theories/Markov.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/PSeries.v' -> `./theories/PSeries.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/RInt.v' -> `./theories/RInt.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/RInt_analysis.v' -> `./theories/RInt_analysis.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/RInt_gen.v' -> `./theories/RInt_gen.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Rbar.v' -> `./theories/Rbar.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Rcomplements.v' -> `./theories/Rcomplements.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/SF_seq.v' -> `./theories/SF_seq.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Seq_fct.v' -> `./theories/Seq_fct.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/theories/Series.v' -> `./theories/Series.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/examples/BacS2013.v' -> `./examples/BacS2013.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/examples/BacS2013_bonus.v' -> `./examples/BacS2013_bonus.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/examples/Bessel.v' -> `./examples/Bessel.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/examples/DAlembert.v' -> `./examples/DAlembert.v'
`/gnu/store/jh2m5wyp835rh090g312hmxkvh2sbvq7-coq-coquelicot-3.1.0-checkout/examples/Wasow.v' -> `./examples/Wasow.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/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.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/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-coquelicot-3.1.0.drv-0/source" (relative from build: ".")
build directory: "/tmp/guix-build-coq-coquelicot-3.1.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/v43cj96i26kw914sw8xqpp4wxlccpgc3-coq-coquelicot-3.1.0" "--enable-fast-install" "--build=arm-unknown-linux-gnueabihf" "--libdir=/gnu/store/v43cj96i26kw914sw8xqpp4wxlccpgc3-coq-coquelicot-3.1.0/lib/coq/user-contrib/Coquelicot")
configure: WARNING: unrecognized options: --enable-fast-install
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
checking for coqc... /gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin/coqc
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 SSReflect... yes
configure: building remake...
ld: /tmp/guix-build-coq-coquelicot-3.1.0.drv-0/ccbUa9T4.o: in function `main':
remake.cpp:(.text.startup+0x5c0): 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 9.8 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 660, characters 2-37:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Rcomplements.v", line 676, characters 2-20:
Warning: Duplicate clear of n [duplicate-clear,ssr]
File "./theories/Rcomplements.v", line 1383, characters 2-54:
Warning: Duplicate clear of n [duplicate-clear,ssr]
File "./theories/Rcomplements.v", line 1413, characters 2-54:
Warning: Duplicate clear of n [duplicate-clear,ssr]
File "./theories/Rcomplements.v", line 1434, characters 2-49:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Rcomplements.v", line 1439, characters 2-26:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1637, characters 19-28:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1638, characters 24-34:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1637, characters 19-28:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1638, characters 24-34:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1637, characters 19-28:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1630, characters 2-460:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1638, characters 24-34:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1656, characters 35-48:
Warning: Notation RList.Rlength is deprecated since 8.12.
use List.length instead [deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1657, characters 19-29:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1657, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1658, characters 21-31:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1658, characters 36-46:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1666, characters 35-45:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1666, characters 49-59:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
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
Finished theories/Markov.vo
Building theories/Rbar.vo
File "./theories/Rbar.v", line 49, characters 0-27:
Warning:
New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function.
[ambiguous-paths,typechecker]
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 1832, characters 0-47:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 1855, characters 0-77:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2040, characters 0-20:
Warning: Duplicate clear of x [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2054, characters 0-25:
Warning: Duplicate clear of x [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2059, characters 0-25:
Warning: Duplicate clear of x [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2269, characters 2-37:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2400, characters 2-54:
Warning: Duplicate clear of HFc [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2405, characters 2-40:
Warning: Duplicate clear of H0 [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2406, characters 2-47:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2407, characters 2-61:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2461, characters 2-23:
Warning: Duplicate clear of Hfg [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2469, characters 2-23:
Warning: Duplicate clear of Hhl [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2508, characters 2-23:
Warning: Duplicate clear of Hfg [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2512, characters 2-115:
Warning: Duplicate clear of Hfh [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 2521, characters 2-64:
Warning: Duplicate clear of Hfh [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 4220, characters 2-36:
Warning: Duplicate clear of A [duplicate-clear,ssr]
File "./theories/Hierarchy.v", line 4255, characters 2-36:
Warning: Duplicate clear of A [duplicate-clear,ssr]
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 268, characters 2-211:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 268, characters 2-211:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 268, characters 2-211:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 268, characters 2-211:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 280, characters 2-121:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 284, characters 2-119:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 286, characters 2-88:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 290, characters 2-91:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 303, characters 2-211:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 303, characters 2-211:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 303, characters 2-211:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 303, characters 2-211:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 317, characters 2-121:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 321, characters 2-91:
Warning: Duplicate clear of Hl0 [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 323, characters 2-119:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 325, characters 2-88:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 482, characters 2-235:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 508, characters 2-166:
Warning: Duplicate clear of Hiu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 508, characters 2-166:
Warning: Duplicate clear of Hsu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 517, characters 2-133:
Warning: Duplicate clear of Hiu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 520, characters 2-133:
Warning: Duplicate clear of Hsu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 536, characters 2-60:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 726, characters 2-38:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 744, characters 2-28:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 1512, characters 2-103:
Warning: Duplicate clear of Hcv [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 1517, characters 2-103:
Warning: Duplicate clear of Hcv [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 2113, characters 2-31:
Warning: Duplicate clear of n [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 2130, characters 2-31:
Warning: Duplicate clear of n [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 2139, characters 2-31:
Warning: Duplicate clear of n [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 2178, characters 2-38:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 2185, characters 2-38:
Warning: Duplicate clear of Hu [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 2465, characters 4-58:
Warning: Duplicate clear of Hl [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 2857, characters 2-43:
Warning: Duplicate clear of Ha [duplicate-clear,ssr]
File "./theories/Lim_seq.v", line 3155, characters 2-76:
Warning: Duplicate clear of H2 [duplicate-clear,ssr]
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]
File "./theories/Continuity.v", line 863, characters 4-75:
Warning: Duplicate clear of Cf [duplicate-clear,ssr]
File "./theories/Continuity.v", line 885, characters 2-68:
Warning: Duplicate clear of He [duplicate-clear,ssr]
File "./theories/Continuity.v", line 1000, characters 2-46:
Warning: Duplicate clear of Hab [duplicate-clear,ssr]
File "./theories/Continuity.v", line 1808, characters 2-66:
Warning: Duplicate clear of Cf [duplicate-clear,ssr]
File "./theories/Continuity.v", line 1820, characters 4-41:
Warning: Duplicate clear of eps [duplicate-clear,ssr]
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]
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]
File "./theories/Derive.v", line 345, characters 2-21:
Warning: Duplicate clear of Df [duplicate-clear,ssr]
File "./theories/Derive.v", line 2208, characters 2-63:
Warning: Duplicate clear of Cf [duplicate-clear,ssr]
File "./theories/Derive.v", line 2209, characters 2-63:
Warning: Duplicate clear of Cg [duplicate-clear,ssr]
File "./theories/Derive.v", line 2233, characters 2-33:
Warning: Duplicate clear of Cf [duplicate-clear,ssr]
File "./theories/Derive.v", line 2234, characters 2-33:
Warning: Duplicate clear of Cg [duplicate-clear,ssr]
File "./theories/Derive.v", line 2235, characters 2-62:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/Derive.v", line 2325, characters 2-29:
Warning: Duplicate clear of Hbx [duplicate-clear,ssr]
File "./theories/Derive.v", line 2343, characters 2-29:
Warning: Duplicate clear of Hax [duplicate-clear,ssr]
File "./theories/Derive.v", line 2479, characters 2-29:
Warning: Duplicate clear of Hbx [duplicate-clear,ssr]
File "./theories/Derive.v", line 2510, characters 2-29:
Warning: Duplicate clear of Hax [duplicate-clear,ssr]
File "./theories/Derive.v", line 3327, characters 6-22:
Warning: Duplicate clear of Hy [duplicate-clear,ssr]
File "./theories/Derive.v", line 3406, characters 2-37:
Warning: Duplicate clear of f [duplicate-clear,ssr]
File "./theories/Derive.v", line 3422, characters 2-38:
Warning: Duplicate clear of f [duplicate-clear,ssr]
File "./theories/Derive.v", line 3439, characters 2-38:
Warning: Duplicate clear of f [duplicate-clear,ssr]
Finished theories/Derive.vo
Building theories/Derive_2d.vo
File "./theories/Derive_2d.v", line 1196, characters 2-43:
Warning: Duplicate clear of z [duplicate-clear,ssr]
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]
File "./theories/Series.v", line 974, characters 4-28:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Series.v", line 1033, characters 4-34:
Warning: Duplicate clear of Hda [duplicate-clear,ssr]
File "./theories/Series.v", line 1054, characters 2-16:
Warning: Duplicate clear of H [duplicate-clear,ssr]
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]
File "./theories/Seq_fct.v", line 159, characters 2-59:
Warning: Duplicate clear of H0 [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 180, characters 2-59:
Warning: Duplicate clear of H0 [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 243, characters 4-35:
Warning: Duplicate clear of Hy [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 279, characters 4-64:
Warning: Duplicate clear of Hfn [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 280, characters 4-41:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 281, characters 4-36:
Warning: Duplicate clear of Hex [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 316, characters 2-97:
Warning: Duplicate clear of x [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 392, characters 4-36:
Warning: Duplicate clear of Edn [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 702, characters 4-82:
Warning: Duplicate clear of Hcvs [duplicate-clear,ssr]
File "./theories/Seq_fct.v", line 714, characters 4-82:
Warning: Duplicate clear of Hcvs [duplicate-clear,ssr]
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 537, characters 2-59:
Warning: Duplicate clear of Hnot_ex [duplicate-clear,ssr]
File "./theories/PSeries.v", line 660, characters 4-44:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/PSeries.v", line 1268, characters 2-53:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/PSeries.v", line 1306, characters 2-53:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/PSeries.v", line 1474, characters 2-33:
Warning: Duplicate clear of H0 [duplicate-clear,ssr]
File "./theories/PSeries.v", line 1481, characters 2-26:
Warning: Duplicate clear of H0 [duplicate-clear,ssr]
File "./theories/PSeries.v", line 2045, characters 4-64:
Warning: Duplicate clear of Hn [duplicate-clear,ssr]
File "./theories/PSeries.v", line 2045, characters 4-64:
Warning: Duplicate clear of Hn [duplicate-clear,ssr]
File "./theories/PSeries.v", line 2441, characters 4-46:
Warning: Duplicate clear of r [duplicate-clear,ssr]
File "./theories/PSeries.v", line 2457, characters 3-82:
Warning: Duplicate clear of Hw [duplicate-clear,ssr]
Finished theories/PSeries.vo
Building theories/RInt.vo
Building theories/SF_seq.vo
File "./theories/SF_seq.v", line 25, 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 38, characters 14-23:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 39, characters 14-24:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 41, characters 24-35:
Warning: Notation RList.Rlist is deprecated since 8.12. use (list R) instead
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 41, characters 0-134:
Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 41, characters 0-134:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 47, characters 25-36:
Warning: Notation RList.Rlist is deprecated since 8.12. use (list R) instead
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 59, characters 2-15:
Warning: Notation RList.Rlength is deprecated since 8.12.
use List.length instead [deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 116, characters 2-78:
Warning: Duplicate clear of IHs [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 337, characters 2-18:
Warning: Duplicate clear of IH [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 403, characters 2-38:
Warning: Duplicate clear of IHst [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 845, characters 2-30:
Warning: Duplicate clear of IH [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 918, characters 2-31:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 1032, characters 2-74:
Warning: Duplicate clear of Hx' [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 1108, characters 2-30:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 1302, characters 2-149:
Warning: Duplicate clear of Hdec [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 2104, characters 2-28:
Warning: Duplicate clear of IH [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 2659, characters 4-242:
Warning: Duplicate clear of Hw [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 2659, characters 4-242:
Warning: Duplicate clear of Hw [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 2774, characters 4-242:
Warning: Duplicate clear of Hw [duplicate-clear,ssr]
File "./theories/SF_seq.v", line 2774, characters 4-242:
Warning: Duplicate clear of Hw [duplicate-clear,ssr]
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 177, characters 2-23:
Warning: Duplicate clear of Hex [duplicate-clear,ssr]
File "./theories/RInt.v", line 191, characters 2-37:
Warning: Duplicate clear of Hex [duplicate-clear,ssr]
File "./theories/RInt.v", line 287, characters 2-23:
Warning: Duplicate clear of Hex [duplicate-clear,ssr]
File "./theories/RInt.v", line 357, characters 4-35:
Warning: Duplicate clear of Hg [duplicate-clear,ssr]
File "./theories/RInt.v", line 399, characters 2-22:
Warning: Duplicate clear of Hex [duplicate-clear,ssr]
File "./theories/RInt.v", line 464, characters 2-74:
Warning: Duplicate clear of Hstep [duplicate-clear,ssr]
File "./theories/RInt.v", line 552, characters 2-71:
Warning: Duplicate clear of Heq [duplicate-clear,ssr]
File "./theories/RInt.v", line 557, characters 2-60:
Warning: Duplicate clear of Hstep [duplicate-clear,ssr]
File "./theories/RInt.v", line 888, characters 2-22:
Warning: Duplicate clear of If [duplicate-clear,ssr]
File "./theories/RInt.v", line 912, characters 2-212:
Warning: Duplicate clear of Hs [duplicate-clear,ssr]
File "./theories/RInt.v", line 986, characters 2-97:
Warning: Duplicate clear of H1 [duplicate-clear,ssr]
File "./theories/RInt.v", line 987, characters 2-97:
Warning: Duplicate clear of H2 [duplicate-clear,ssr]
File "./theories/RInt.v", line 1813, characters 6-22:
Warning: Duplicate clear of H0 [duplicate-clear,ssr]
File "./theories/RInt.v", line 2936, characters 37-47:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2936, characters 53-63:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2936, characters 37-47:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2936, characters 53-63:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2937, characters 33-43:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2937, characters 49-59:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2937, characters 33-43:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2937, characters 49-59:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2985, characters 18-28:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2985, characters 18-28:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2997, characters 2-27:
Warning: Duplicate clear of H [duplicate-clear,ssr]
File "./theories/RInt.v", line 3037, characters 2-44:
Warning: Duplicate clear of IH [duplicate-clear,ssr]
File "./theories/RInt.v", line 3323, characters 2-30:
Warning: Duplicate clear of IH [duplicate-clear,ssr]
File "./theories/RInt.v", line 3325, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3325, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3587, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3587, characters 50-60:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3587, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3587, characters 50-60:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3590, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3590, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3590, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3593, characters 33-43:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3593, characters 49-59:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3593, characters 33-43:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3593, characters 49-59:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3597, characters 33-43:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3597, characters 49-59:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3597, characters 33-43:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3597, characters 49-59:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3618, characters 2-51:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/RInt.v", line 3618, characters 2-51:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/RInt.v", line 3620, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3620, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3624, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3624, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3624, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3664, characters 2-55:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/RInt.v", line 3664, characters 2-55:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/RInt.v", line 3666, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3666, characters 34-44:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3670, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3670, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3670, characters 27-37:
Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3749, characters 2-107:
Warning: Duplicate clear of IH [duplicate-clear,ssr]
File "./theories/RInt.v", line 3805, characters 2-148:
Warning: Duplicate clear of Hptd [duplicate-clear,ssr]
File "./theories/RInt.v", line 3814, characters 2-159:
Warning: Duplicate clear of IH [duplicate-clear,ssr]
File "./theories/RInt.v", line 3904, characters 4-50:
Warning: Duplicate clear of Hab [duplicate-clear,ssr]
File "./theories/RInt.v", line 3904, characters 4-50:
Warning: Duplicate clear of Hab [duplicate-clear,ssr]
File "./theories/RInt.v", line 4023, characters 4-79:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/RInt.v", line 4294, characters 2-23:
Warning: Duplicate clear of HIf [duplicate-clear,ssr]
File "./theories/RInt.v", line 4309, characters 2-23:
Warning: Duplicate clear of HIf [duplicate-clear,ssr]
File "./theories/RInt.v", line 4332, characters 2-22:
Warning: Duplicate clear of HIf [duplicate-clear,ssr]
File "./theories/RInt.v", line 4394, characters 2-23:
Warning: Duplicate clear of HIf [duplicate-clear,ssr]
File "./theories/RInt.v", line 4454, characters 6-34:
Warning: Duplicate clear of H1 [duplicate-clear,ssr]
File "./theories/RInt.v", line 4454, characters 6-34:
Warning: Duplicate clear of H1 [duplicate-clear,ssr]
File "./theories/RInt.v", line 4489, characters 6-34:
Warning: Duplicate clear of Ht [duplicate-clear,ssr]
File "./theories/RInt.v", line 4489, characters 6-34:
Warning: Duplicate clear of Ht [duplicate-clear,ssr]
File "./theories/RInt.v", line 4503, characters 6-34:
Warning: Duplicate clear of H1 [duplicate-clear,ssr]
File "./theories/RInt.v", line 4503, characters 6-34:
Warning: Duplicate clear of H1 [duplicate-clear,ssr]
File "./theories/RInt.v", line 4592, characters 2-23:
Warning: Duplicate clear of HIf [duplicate-clear,ssr]
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]
File "./theories/RInt_analysis.v", line 48, characters 4-104:
Warning: Duplicate clear of CIf [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 113, characters 2-114:
Warning: Duplicate clear of CIf [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 338, characters 2-59:
Warning: Duplicate clear of Hf [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 470, characters 2-95:
Warning: Duplicate clear of Ha [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 474, characters 2-95:
Warning: Duplicate clear of Hb [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 692, characters 2-60:
Warning: Duplicate clear of Hf [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 773, characters 0-57:
Warning: Duplicate clear of Ca [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 793, characters 0-57:
Warning: Duplicate clear of Ca [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 794, characters 0-57:
Warning: Duplicate clear of Cb [duplicate-clear,ssr]
File "./theories/RInt_analysis.v", line 1283, characters 0-58:
Warning: Duplicate clear of Hy [duplicate-clear,ssr]
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 556, characters 2-30:
Warning: Duplicate clear of Hy [duplicate-clear,ssr]
File "./theories/ElemFct.v", line 570, characters 2-36:
Warning: Duplicate clear of n [duplicate-clear,ssr]
File "./theories/ElemFct.v", line 666, characters 2-56:
Warning: Duplicate clear of Hx [duplicate-clear,ssr]
File "./theories/ElemFct.v", line 674, characters 2-53:
Warning: Duplicate clear of n [duplicate-clear,ssr]
Finished theories/ElemFct.vo
File "./theories/AutoDerive.v", line 763, characters 0-65:
Warning: Duplicate clear of Dle [duplicate-clear,ssr]
File "./theories/AutoDerive.v", line 961, characters 0-45:
Warning: Duplicate clear of IHe1 [duplicate-clear,ssr]
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 507, 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 510, 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 513, 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 590, 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 272, 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 161.5 seconds
starting phase `check'
Building examples/BacS2013.vo
File "./examples/BacS2013.v", line 24, characters 0-96:
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-46:
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-84:
Warning:
New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function.
[ambiguous-paths,typechecker]
File "./examples/Bessel.v", line 316, characters 2-76:
Warning: Duplicate clear of Haux [duplicate-clear,ssr]
File "./examples/Bessel.v", line 316, characters 2-76:
Warning: Duplicate clear of Haux [duplicate-clear,ssr]
File "./examples/Bessel.v", line 330, characters 2-76:
Warning: Duplicate clear of Haux [duplicate-clear,ssr]
File "./examples/Bessel.v", line 330, characters 2-76:
Warning: Duplicate clear of Haux [duplicate-clear,ssr]
File "./examples/Bessel.v", line 356, characters 2-55:
Warning: Duplicate clear of Haux [duplicate-clear,ssr]
Finished examples/Bessel.vo
Building examples/DAlembert.vo
Finished examples/DAlembert.vo
Building check
Finished check
phase `check' succeeded after 25.3 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/v43cj96i26kw914sw8xqpp4wxlccpgc3-coq-coquelicot-3.1.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 0 binaries in "/gnu/store/v43cj96i26kw914sw8xqpp4wxlccpgc3-coq-coquelicot-3.1.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