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/lwsi05xjf0hhihyxplyx6n51448cmr71-coq-mathcomp-1.17.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/lwsi05xjf0hhihyxplyx6n51448cmr71-coq-mathcomp-1.17.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/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/INSTALL.md' -> `./INSTALL.md'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/NEWS.md' -> `./NEWS.md'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/.gitlab-ci.yml' -> `./.gitlab-ci.yml'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/COPYING' -> `./COPYING'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/.gitattributes' -> `./.gitattributes'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/configure.in' -> `./configure.in'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/README.md' -> `./README.md'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/Remakefile.in' -> `./Remakefile.in'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/remake.cpp' -> `./remake.cpp'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/opam' -> `./opam'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/.mailmap' -> `./.mailmap'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/misc/Dockerfile' -> `./misc/Dockerfile'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/misc/ci.md' -> `./misc/ci.md'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/examples/Wasow.v' -> `./examples/Wasow.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/examples/BacS2013_bonus.v' -> `./examples/BacS2013_bonus.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/examples/BacS2013.v' -> `./examples/BacS2013.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/examples/DAlembert.v' -> `./examples/DAlembert.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/examples/Bessel.v' -> `./examples/Bessel.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/SF_seq.v' -> `./theories/SF_seq.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Derive_2d.v' -> `./theories/Derive_2d.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Lim_seq.v' -> `./theories/Lim_seq.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Hierarchy.v' -> `./theories/Hierarchy.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Coquelicot.v' -> `./theories/Coquelicot.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Markov.v' -> `./theories/Markov.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Complex.v' -> `./theories/Complex.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/PSeries.v' -> `./theories/PSeries.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/RInt_analysis.v' -> `./theories/RInt_analysis.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Continuity.v' -> `./theories/Continuity.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Derive.v' -> `./theories/Derive.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Lub.v' -> `./theories/Lub.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/KHInt.v' -> `./theories/KHInt.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/ElemFct.v' -> `./theories/ElemFct.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Series.v' -> `./theories/Series.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Compactness.v' -> `./theories/Compactness.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Iter.v' -> `./theories/Iter.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Seq_fct.v' -> `./theories/Seq_fct.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Equiv.v' -> `./theories/Equiv.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/RInt_gen.v' -> `./theories/RInt_gen.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Rbar.v' -> `./theories/Rbar.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/Rcomplements.v' -> `./theories/Rcomplements.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-checkout/theories/RInt.v' -> `./theories/RInt.v'
`/gnu/store/spdzi549k2rpp2pcz9k5z7mqixidw7wv-coq-coquelicot-3.4.0-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.0.drv-0/source" (relative from build: ".")
build directory: "/tmp/guix-build-coq-coquelicot-3.4.0.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/gyslaz6vs71gs81qjsgjv3vvr68gw6s7-coq-coquelicot-3.4.0" "--enable-fast-install" "--build=powerpc64le-unknown-linux-gnu" "COQUSERCONTRIB=/gnu/store/gyslaz6vs71gs81qjsgjv3vvr68gw6s7-coq-coquelicot-3.4.0/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.0.drv-0/ccTO1zvU.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 51, characters 30-40:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 51, characters 30-40:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 51, characters 30-40:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 63, characters 7-21:
Warning: Notation not_le_minus_0 is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_le (together with Nat.lt_nge and Nat.lt_le_incl) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 63, characters 7-21:
Warning: Notation not_le_minus_0 is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_le (together with Nat.lt_nge and Nat.lt_le_incl) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 73, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 73, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 73, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 80, characters 13-22:
Warning: Notation le_n_0_eq is deprecated since 8.16.
The Arith.Le file is obsolete. Use the bidirectional version Nat.le_0_r (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 81, characters 24-39:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 81, characters 24-39:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 81, characters 24-39:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 584, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 584, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 605, characters 18-28:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 605, characters 18-28:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 605, characters 18-28:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 622, characters 31-57:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 622, characters 31-57:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 622, characters 31-57:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 640, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 640, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 680, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 680, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 696, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 696, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 696, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 956, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 956, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 956, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ <= _ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ < _ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ <= _ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ < _ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1305, characters 0-21:
Warning: Notation "_ ^ _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./theories/Rcomplements.v", line 1344, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1344, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1348, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1348, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1355, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1355, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1360, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1360, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1370, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1370, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1466, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1466, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1675, characters 53-59:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1675, characters 53-59:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1678, characters 18-24:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Rcomplements.v", line 1678, characters 18-24:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
Finished theories/Rcomplements.vo
Finished theories/Compactness.vo
Building theories/Hierarchy.vo
Building theories/Iter.vo
File "./theories/Iter.v", line 131, characters 10-24:
Warning: Notation not_le_minus_0 is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_le (together with Nat.lt_nge and Nat.lt_le_incl) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 131, characters 10-24:
Warning: Notation not_le_minus_0 is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_le (together with Nat.lt_nge and Nat.lt_le_incl) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 131, characters 10-24:
Warning: Notation not_le_minus_0 is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_le (together with Nat.lt_nge and Nat.lt_le_incl) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 143, characters 13-26:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 143, characters 13-26:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 143, characters 13-26:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 175, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 175, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Iter.v", line 175, characters 11-21:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
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 812, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 812, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4211, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4211, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4222, characters 18-24:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4222, characters 18-24:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4228, characters 24-30:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4228, characters 24-30:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4240, characters 14-20:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4240, characters 14-20:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4243, characters 16-22:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4243, characters 16-22:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4243, characters 16-22:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4518, characters 13-23:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4518, characters 13-23:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4543, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4543, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4559, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4559, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4562, characters 14-24:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4562, characters 14-24:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4575, characters 25-35:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4575, characters 25-35:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4594, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4594, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4597, characters 14-24:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4597, characters 14-24:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4610, characters 37-47:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4610, characters 37-47:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4632, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4632, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4650, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4650, characters 11-21:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4939, characters 11-18:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Hierarchy.v", line 4939, characters 11-18:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[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]
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 721, characters 38-47:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 721, characters 38-47:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 723, characters 32-41:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 723, characters 32-41:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 761, characters 32-41:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 761, characters 32-41:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1016, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1016, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1025, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1025, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1033, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1033, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1041, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1041, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1290, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1290, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1297, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1297, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1309, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1309, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1317, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1317, characters 11-20:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1523, characters 47-56:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1523, characters 47-56:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1588, characters 6-19:
Warning: Notation plus_le_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1588, characters 6-19:
Warning: Notation plus_le_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1590, characters 28-37:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1590, characters 28-37:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1596, characters 6-13:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1596, characters 6-13:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1598, characters 6-22:
Warning: Notation plus_lt_compat_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1598, characters 6-22:
Warning: Notation plus_lt_compat_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1600, characters 6-15:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1600, characters 6-15:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1602, characters 39-48:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1602, characters 39-48:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1606, characters 34-55:
Warning: Notation Plus.plus_assoc is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1606, characters 34-55:
Warning: Notation Plus.plus_assoc is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1606, characters 34-55:
Warning: Notation Plus.plus_assoc is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1607, characters 6-22:
Warning: Notation plus_le_compat_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1607, characters 6-22:
Warning: Notation plus_le_compat_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1608, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1608, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1608, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1612, characters 18-33:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 1612, characters 18-33:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2058, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2058, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2058, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2079, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2079, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2079, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2543, 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 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 27-36:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2544, 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 2544, 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 2544, 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 2995, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2995, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 2995, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 3152, characters 35-44:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Lim_seq.v", line 3152, characters 35-44:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[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]
File "./theories/Continuity.v", line 945, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Continuity.v", line 945, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Continuity.v", line 946, characters 30-40:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Continuity.v", line 946, characters 30-40:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
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]
File "./theories/Derive.v", line 2990, characters 11-21:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive.v", line 2990, characters 11-21:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
Finished theories/Derive.vo
Building theories/Derive_2d.vo
File "./theories/Derive_2d.v", line 741, characters 10-19:
Warning: Notation le_n_0_eq is deprecated since 8.16.
The Arith.Le file is obsolete. Use the bidirectional version Nat.le_0_r (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 741, characters 10-19:
Warning: Notation le_n_0_eq is deprecated since 8.16.
The Arith.Le file is obsolete. Use the bidirectional version Nat.le_0_r (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 742, characters 6-17:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 742, characters 6-17:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 744, characters 10-17:
Warning: Notation gt_S_le is deprecated since 8.16.
The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 744, characters 10-17:
Warning: Notation gt_S_le is deprecated since 8.16.
The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 996, characters 6-13:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 996, characters 6-13:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1055, characters 6-15:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1055, characters 6-15:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1067, characters 6-19:
Warning: Notation le_plus_trans is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_r (together with Nat.le_trans) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1067, characters 27-34:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1067, characters 6-19:
Warning: Notation le_plus_trans is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_r (together with Nat.le_trans) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1067, characters 27-34:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1120, characters 54-69:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1120, characters 54-69:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1120, characters 54-69:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1122, characters 15-30:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1122, characters 15-30:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1122, characters 15-30:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1162, characters 10-21:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1162, characters 10-21:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1165, characters 10-17:
Warning: Notation gt_S_le is deprecated since 8.16.
The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1165, characters 10-17:
Warning: Notation gt_S_le is deprecated since 8.16.
The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1228, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1228, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1228, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1234, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1234, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1234, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1239, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1239, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1239, characters 14-27:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1318, characters 43-53:
Warning: Notation plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.add_sub_eq_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1318, characters 43-53:
Warning: Notation plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.add_sub_eq_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1324, characters 13-23:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1324, characters 13-23:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1324, characters 13-23:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1337, characters 10-20:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1337, characters 10-20:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1393, characters 9-22:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1393, characters 9-22:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Derive_2d.v", line 1393, characters 9-22:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
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 155, characters 10-18:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 155, characters 10-18:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 159, characters 10-18:
Warning: Notation le_Sn_le is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 159, characters 10-18:
Warning: Notation le_Sn_le is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 181, characters 10-18:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 181, characters 10-18:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 809, characters 37-63:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 809, characters 37-63:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 809, characters 37-63:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 821, characters 13-39:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 821, characters 13-39:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 821, characters 13-39:
Warning: Notation minus_plus_simpl_l_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 826, characters 10-16:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 826, characters 10-16:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 827, characters 36-45:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 827, characters 67-76:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 842, characters 59-68:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 842, characters 86-95:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 842, characters 59-68:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 842, characters 86-95:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 859, characters 11-26:
Warning: Notation Div2.ind_0_1_SS is deprecated since 8.16.
The Arith.Div2 file is obsolete. [deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 859, characters 50-59:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 859, characters 11-26:
Warning: Notation Div2.ind_0_1_SS is deprecated since 8.16.
The Arith.Div2 file is obsolete. [deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 859, characters 50-59:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 863, characters 13-22:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 863, characters 43-52:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 863, characters 13-22:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 863, characters 43-52:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 864, characters 20-29:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 864, characters 54-63:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 864, characters 20-29:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 864, characters 54-63:
Warning: Notation Div2.div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 1047, characters 16-25:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Series.v", line 1047, characters 16-25:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
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 161, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 161, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 161, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 182, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 182, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 182, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 282, characters 16-25:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 282, characters 16-25:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 282, characters 16-25:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 711, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 711, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 714, characters 25-31:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 714, characters 25-31:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 745, characters 13-19:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/Seq_fct.v", line 745, characters 13-19:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
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 337, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 337, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 399, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 399, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1003, characters 11-22:
Warning: Notation lt_pred_n_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_pred_l (together with Nat.neq_0_lt_0) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1003, characters 11-22:
Warning: Notation lt_pred_n_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_pred_l (together with Nat.neq_0_lt_0) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1041, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1041, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[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]
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 1241, characters 12-22:
Warning: Notation plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.add_sub_eq_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1241, characters 12-22:
Warning: Notation plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.add_sub_eq_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1369, characters 57-61:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1371, characters 70-74:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1369, characters 57-61:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1371, characters 70-74:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1374, characters 9-21:
Warning: Notation even_odd_dec is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_Odd_dec (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1374, characters 9-21:
Warning: Notation even_odd_dec is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_Odd_dec (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1374, characters 9-21:
Warning: Notation even_odd_dec is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_Odd_dec (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1377, characters 12-21:
Warning: Notation even_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_div2 (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1377, characters 32-43:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1377, characters 12-21:
Warning: Notation even_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_div2 (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1377, characters 12-21:
Warning: Notation even_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_div2 (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1377, characters 32-43:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1377, characters 32-43:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1378, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1379, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1378, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1378, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1378, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1378, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1379, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1379, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1379, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1379, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1379, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1380, characters 11-17:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1380, characters 11-17:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1380, characters 11-17:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1382, characters 36-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1383, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1383, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1382, characters 36-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1383, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1383, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1383, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1383, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1384, characters 17-23:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1384, characters 52-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1384, characters 17-23:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1384, characters 52-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1388, characters 12-20:
Warning: Notation odd_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_div2 (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1388, characters 31-41:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1388, characters 12-20:
Warning: Notation odd_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_div2 (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1388, characters 12-20:
Warning: Notation odd_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_div2 (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1388, characters 31-41:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1388, characters 31-41:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1389, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1390, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1389, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1389, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1389, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1389, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1390, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1390, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1390, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1390, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1390, characters 11-19:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1391, characters 11-17:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1391, characters 11-17:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1391, characters 11-17:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1393, characters 36-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1394, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1394, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1393, characters 36-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1394, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1394, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1394, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1394, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1395, characters 46-52:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1396, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1396, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1395, characters 46-52:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1396, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1396, characters 17-25:
Warning: Notation double_S is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double_S instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1396, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1396, characters 27-33:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1397, characters 17-23:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1397, characters 52-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1397, characters 17-23:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1397, characters 52-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1406, characters 8-21:
Warning: Notation plus_le_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1406, characters 8-21:
Warning: Notation plus_le_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1409, characters 29-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1409, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1409, characters 29-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1409, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1410, characters 8-19:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1410, characters 8-19:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1411, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1411, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1411, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1411, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1413, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1413, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1413, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1413, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1419, characters 7-11:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1419, characters 7-11:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1428, characters 8-21:
Warning: Notation plus_le_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1428, characters 8-21:
Warning: Notation plus_le_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1431, characters 32-38:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1431, characters 40-44:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1431, characters 32-38:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1431, characters 40-44:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1432, characters 8-19:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1432, characters 8-19:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1433, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1433, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1433, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1433, characters 13-24:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1437, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1437, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1437, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/PSeries.v", line 1437, characters 13-23:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
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 97, characters 26-32:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 97, characters 26-32:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 101, characters 59-65:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 101, characters 59-65:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 139, characters 11-21:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 139, characters 11-21:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r 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]
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 159, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 159, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 162, characters 10-20:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 162, characters 10-20:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 162, characters 10-20:
Warning: Notation minus_Sn_m is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_succ_l (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 171, characters 10-20:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 171, characters 10-20:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 178, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 178, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 240, characters 69-75:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 240, characters 69-75:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 244, characters 33-39:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 244, characters 33-39:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 307, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 307, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 312, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 312, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 316, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 316, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 702, characters 39-45:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 702, characters 39-45:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 702, characters 39-45:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 702, characters 39-45:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 722, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 722, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 818, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 818, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 830, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 830, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 833, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 833, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 994, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 994, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 994, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 994, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1003, characters 17-23:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1003, characters 17-23:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1003, characters 17-23:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1003, characters 17-23:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1003, characters 17-23:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1020, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1020, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1020, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1020, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1037, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1037, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1038, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1038, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1046, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1046, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1046, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1046, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1054, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1054, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1054, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1054, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1056, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1056, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1072, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1072, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1072, characters 29-35:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1072, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1072, characters 21-27:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1072, characters 29-35:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1074, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1074, characters 8-14:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1214, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1214, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1313, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1313, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1320, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1320, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1320, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1320, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1321, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1321, characters 11-17:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1322, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1322, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1419, characters 10-16:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1419, characters 10-16:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1424, characters 14-20:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1424, characters 14-20:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1440, characters 8-15:
Warning: Notation gt_S_le is deprecated since 8.16.
The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1440, characters 8-15:
Warning: Notation gt_S_le is deprecated since 8.16.
The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1977, characters 25-31:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 1977, characters 25-31:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2140, characters 34-40:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2140, characters 34-40:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2141, characters 34-40:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2141, characters 34-40:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2150, characters 43-49:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2150, characters 43-49:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2255, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2255, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2255, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2257, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2257, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2257, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2264, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2264, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2264, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2301, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2301, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2529, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2529, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2529, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2531, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2531, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2531, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2538, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2538, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2538, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2567, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2567, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2585, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2585, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2585, characters 20-26:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2587, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2587, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2587, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2594, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2594, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2594, characters 35-41:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2623, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2623, characters 32-38:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2702, characters 19-25:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2702, characters 19-25:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2817, characters 19-25:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/SF_seq.v", line 2817, characters 19-25:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
Finished theories/SF_seq.vo
File "./theories/RInt.v", line 23, characters 0-65:
Warning: Notation "[ predI _ & _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./theories/RInt.v", line 23, characters 0-65:
Warning: Notation "[ predU _ & _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./theories/RInt.v", line 23, characters 0-65:
Warning: Notation "[ predD _ & _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./theories/RInt.v", line 23, characters 0-65:
Warning: Notation "[ predC _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./theories/RInt.v", line 23, characters 0-65:
Warning: Notation "[ preim _ of _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
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 151, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 151, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 151, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 154, characters 41-47:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 154, characters 41-47:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 214, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 214, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 243, characters 32-38:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 243, characters 32-38:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 246, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 246, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[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 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 360, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 360, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 360, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 400, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 400, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 410, characters 16-22:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 410, characters 16-22:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 410, characters 16-22:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 412, characters 31-37:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 412, characters 31-37:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 412, characters 31-37:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 742, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 742, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 753, characters 8-15:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 753, characters 8-15:
Warning: Notation lt_le_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 767, characters 13-22:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 767, characters 13-22:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 775, characters 13-22:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 775, characters 13-22:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 930, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 930, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1179, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1179, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1905, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1905, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1917, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1917, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1928, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1928, characters 23-29:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1928, characters 15-21:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1928, characters 23-29:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1931, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1931, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1942, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1942, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1969, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1969, characters 12-18:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1975, characters 15-21:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 1975, characters 15-21:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2859, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2859, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2859, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2865, characters 18-27:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2865, characters 18-27:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2934, characters 16-22:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 2934, characters 16-22:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3027, characters 24-33:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3027, characters 24-33:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3060, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3060, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3063, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3063, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3065, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3065, characters 38-44:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3067, characters 24-30:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3067, characters 24-30:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3068, characters 24-30:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3068, characters 24-30:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3339, characters 16-22:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3339, characters 16-22:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3339, characters 16-22:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3589, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3589, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3593, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3593, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3596, characters 8-18:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3596, characters 8-18:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3621, characters 46-52:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3621, characters 46-52:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3630, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3630, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3630, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3650, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3650, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3650, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3666, characters 46-52:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3666, characters 46-52:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3675, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3675, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3675, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3691, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3691, characters 11-17:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3699, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3699, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3699, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3714, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3714, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 3714, characters 22-28:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4060, characters 17-23:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4060, characters 17-23:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4159, characters 33-39:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4159, characters 33-39:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4241, characters 34-40:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4241, characters 34-40:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4263, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4263, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4263, characters 19-25:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4270, characters 25-31:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4270, characters 25-31:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4357, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4357, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4369, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4369, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4450, characters 36-42:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4450, characters 36-42:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4451, characters 36-42:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4451, characters 36-42:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4485, characters 36-42:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4485, characters 36-42:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4579, characters 46-52:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4579, characters 58-65:
Warning: Notation lt_O_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4579, characters 46-52:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4579, characters 58-65:
Warning: Notation lt_O_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4579, characters 46-52:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4579, characters 58-65:
Warning: Notation lt_O_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4583, characters 68-74:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4583, characters 68-74:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4713, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4713, characters 25-31:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4745, characters 41-47:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4745, characters 41-47:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4745, characters 41-47:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4772, characters 17-23:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4772, characters 17-23:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4772, characters 17-23:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4836, characters 18-24:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4836, characters 18-24:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4837, characters 18-24:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4837, characters 18-24:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4865, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4865, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4868, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4868, characters 10-16:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4876, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4876, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4899, characters 24-30:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/RInt.v", line 4899, characters 24-30:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[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 460, characters 17-23:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 460, characters 17-23:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 460, characters 17-23:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 481, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 481, characters 8-18:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 557, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 557, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 557, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 617, characters 39-54:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 617, characters 39-54:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 667, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 667, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/ElemFct.v", line 667, characters 15-24:
Warning: Notation le_plus_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.
[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
File "./theories/KHInt.v", line 170, characters 6-16:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/KHInt.v", line 170, characters 6-16:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/KHInt.v", line 798, characters 33-39:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/KHInt.v", line 798, characters 33-39:
Warning: Notation lt_n_S is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
Finished theories/KHInt.vo
Building all
Finished all
phase `build' succeeded after 93.8 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 466, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./examples/Bessel.v", line 466, characters 13-19:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./examples/Bessel.v", line 469, characters 11-26:
Warning: Notation Div2.ind_0_1_SS is deprecated since 8.16.
The Arith.Div2 file is obsolete. [deprecated-syntactic-definition,deprecated]
File "./examples/Bessel.v", line 469, characters 11-26:
Warning: Notation Div2.ind_0_1_SS is deprecated since 8.16.
The Arith.Div2 file is obsolete. [deprecated-syntactic-definition,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/gyslaz6vs71gs81qjsgjv3vvr68gw6s7-coq-coquelicot-3.4.0/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/gyslaz6vs71gs81qjsgjv3vvr68gw6s7-coq-coquelicot-3.4.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 `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