D: [iurt_root_command] chroot
Building target platforms: x86_64
Building for target x86_64
Installing /home/pterjan/rpmbuild/SRPMS/coq-flocq-4.1.0-2.mga10.src.rpm
Executing(%mkbuilddir): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.df2y9q
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ test -d /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ /usr/bin/rm -rf /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ /usr/bin/mkdir -p /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ /usr/bin/mkdir -p /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/SPECPARTS
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%prep): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.Uisxce
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ rm -rf flocq-4.1.0
+ /usr/lib/rpm/rpmuncompress -x /home/pterjan/rpmbuild/SOURCES/flocq-4.1.0.tar.gz
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd flocq-4.1.0
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ sed -i 's,\(--coqlib \)[^[:blank:]]*,\1/usr/lib64/ocaml/coq,' Remakefile.in
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.uoedwd
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ CFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CFLAGS
+ CXXFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CXXFLAGS
+ FFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FFLAGS
+ FCFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none --cap-lints=warn'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,--as-needed -Wl,--no-undefined -Wl,-z,relro -Wl,-z,now -Wl,-O1 -Wl,--build-id=sha1 -Wl,--enable-new-dtags -specs=/usr/lib/rpm/redhat/redhat-hardened-ld'
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd flocq-4.1.0
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ ./configure
checking for coqc... /usr/bin/coqc
checking Coq version... 8.16.1
checking for coqdep... /usr/bin/coqdep
checking for coqdoc... /usr/bin/coqdoc
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...
/usr/bin/ld: /tmp/ccJt0TzG.o: in function `main':
remake.cpp:(.text.startup+0xe4a): warning: the use of `tempnam' is dangerous, better use `mkstemp'
configure: creating ./config.status
config.status: creating Remakefile
config.status: creating src/Version.v
config.status: creating src/IEEE754/Int63Compat.v
+ ./remake all doc
Building src/Version.vo
Finished src/Version.vo
Building src/Core/Raux.vo
Building src/Core/Zaux.vo
File "./src/Core/Zaux.v", line 991, characters 12-20:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 991, characters 12-20:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 991, characters 12-20:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1015, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1015, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1015, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1021, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1021, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1021, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/Zaux.vo
File "./src/Core/Raux.v", line 1284, characters 8-24:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1284, characters 8-24:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1284, characters 8-24:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2279, characters 8-15:
Warning: Notation lt_0_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2279, characters 8-15:
Warning: Notation lt_0_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2293, characters 28-34:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2293, characters 28-34:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2348, characters 8-14:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2348, characters 8-14:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/Raux.vo
Building src/Core/Defs.vo
Finished src/Core/Defs.vo
Building src/Core/Digits.vo
Finished src/Core/Digits.vo
Building src/Core/Float_prop.vo
Finished src/Core/Float_prop.vo
Building src/Core/FIX.vo
Building src/Core/Generic_fmt.vo
Building src/Core/Round_pred.vo
Finished src/Core/Round_pred.vo
Finished src/Core/Generic_fmt.vo
Building src/Core/Round_NE.vo
Building src/Core/Ulp.vo
Finished src/Core/Ulp.vo
Finished src/Core/Round_NE.vo
Finished src/Core/FIX.vo
Building src/Core/FLT.vo
Building src/Core/FLX.vo
Finished src/Core/FLX.vo
Finished src/Core/FLT.vo
Building src/Core/FTZ.vo
Finished src/Core/FTZ.vo
Building src/Core/Core.vo
Finished src/Core/Core.vo
Building src/Calc/Bracket.vo
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
Finished src/Calc/Bracket.vo
Building src/Calc/Div.vo
Finished src/Calc/Div.vo
Building src/Calc/Operations.vo
Finished src/Calc/Operations.vo
Building src/Calc/Plus.vo
Building src/Calc/Round.vo
Finished src/Calc/Round.vo
Finished src/Calc/Plus.vo
Building src/Calc/Sqrt.vo
Finished src/Calc/Sqrt.vo
Building src/Prop/Div_sqrt_error.vo
Building src/Prop/Mult_error.vo
Building src/Prop/Plus_error.vo
Building src/Prop/Relative.vo
File "./src/Prop/Relative.v", line 568, characters 17-26:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 568, characters 17-26:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 568, characters 17-26:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 572, characters 43-52:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 572, characters 43-52:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 572, characters 43-52:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Relative.vo
Finished src/Prop/Plus_error.vo
Finished src/Prop/Mult_error.vo
Building src/Prop/Sterbenz.vo
Finished src/Prop/Sterbenz.vo
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Div_sqrt_error.vo
Building src/Prop/Round_odd.vo
Finished src/Prop/Round_odd.vo
Building src/Prop/Double_rounding.vo
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Double_rounding.vo
Building src/IEEE754/BinarySingleNaN.vo
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/IEEE754/BinarySingleNaN.vo
Building src/IEEE754/Binary.vo
Finished src/IEEE754/Binary.vo
Building src/IEEE754/Bits.vo
Finished src/IEEE754/Bits.vo
Building src/IEEE754/Int63Compat.vo
Building src/IEEE754/Int63Copy.vo
Finished src/IEEE754/Int63Copy.vo
Finished src/IEEE754/Int63Compat.vo
Building src/IEEE754/PrimFloat.vo
File "./src/IEEE754/PrimFloat.v", line 271, characters 10-15:
Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 305, characters 16-21:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 309, characters 12-22:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 309, characters 12-22:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 310, characters 9-14:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 332, characters 0-13:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 332, characters 0-13:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 364, characters 5-10:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 364, characters 5-10:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 381, characters 14-24:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 381, characters 14-24:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 383, characters 7-12:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 383, characters 7-12:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
Finished src/IEEE754/PrimFloat.vo
Building src/Pff/Pff.vo
File "./src/Pff/Pff.v", line 107, characters 6-14:
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 "./src/Pff/Pff.v", line 107, characters 6-14:
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 "./src/Pff/Pff.v", line 241, characters 21-29:
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 "./src/Pff/Pff.v", line 241, characters 21-29:
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 "./src/Pff/Pff.v", line 243, 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 "./src/Pff/Pff.v", line 243, 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 "./src/Pff/Pff.v", line 456, characters 6-14:
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 "./src/Pff/Pff.v", line 456, characters 6-14:
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 "./src/Pff/Pff.v", line 464, characters 21-32:
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 "./src/Pff/Pff.v", line 464, characters 21-32:
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 "./src/Pff/Pff.v", line 632, characters 25-33:
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 "./src/Pff/Pff.v", line 632, characters 25-33:
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 "./src/Pff/Pff.v", line 633, characters 18-29:
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 "./src/Pff/Pff.v", line 633, characters 18-29:
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 "./src/Pff/Pff.v", line 655, characters 20-28:
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 "./src/Pff/Pff.v", line 655, characters 20-28:
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 "./src/Pff/Pff.v", line 673, characters 6-17:
Warning: Notation lt_le_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 673, characters 6-17:
Warning: Notation lt_le_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 714, characters 6-15:
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 "./src/Pff/Pff.v", line 714, characters 6-15:
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 "./src/Pff/Pff.v", line 790, characters 6-19:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 790, characters 6-19:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 791, 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 "./src/Pff/Pff.v", line 791, 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 "./src/Pff/Pff.v", line 791, 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 "./src/Pff/Pff.v", line 791, 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 "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
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 "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
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 "./src/Pff/Pff.v", line 879, characters 27-42:
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 "./src/Pff/Pff.v", line 879, characters 27-42:
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 "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 882, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 882, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
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 "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
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 "./src/Pff/Pff.v", line 888, characters 27-42:
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 "./src/Pff/Pff.v", line 888, characters 27-42:
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 "./src/Pff/Pff.v", line 889, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 889, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
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 "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
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 "./src/Pff/Pff.v", line 898, characters 27-42:
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 "./src/Pff/Pff.v", line 898, characters 27-42:
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 "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 900, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 900, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 27-42:
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 "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 27-42:
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 "./src/Pff/Pff.v", line 906, characters 27-42:
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 "./src/Pff/Pff.v", line 906, characters 27-42:
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 "./src/Pff/Pff.v", line 907, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 907, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 912, characters 6-21:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 912, characters 6-21:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 922, characters 8-19:
Warning: Notation powerRZ_neg is deprecated since 8.16.
Use powerRZ_neg' and powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 922, characters 8-19:
Warning: Notation powerRZ_neg is deprecated since 8.16.
Use powerRZ_neg' and powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 922, characters 8-19:
Warning: Notation powerRZ_neg is deprecated since 8.16.
Use powerRZ_neg' and powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 923, characters 10-21:
Warning: Notation powerRZ_inv is deprecated since 8.16. Use powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 923, characters 10-21:
Warning: Notation powerRZ_inv is deprecated since 8.16. Use powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2323, characters 18-28:
Warning: Notation le_antisym is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_antisymm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2323, characters 18-28:
Warning: Notation le_antisym is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_antisymm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2337, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2337, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2337, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2490, characters 6-12:
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 "./src/Pff/Pff.v", line 2490, characters 20-30:
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 "./src/Pff/Pff.v", line 2490, characters 6-12:
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 "./src/Pff/Pff.v", line 2490, characters 20-30:
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 "./src/Pff/Pff.v", line 2498, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2498, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2498, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2591, characters 6-14:
Warning: Notation le_trans is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2591, characters 6-14:
Warning: Notation le_trans is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2593, characters 11-24:
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 "./src/Pff/Pff.v", line 2593, characters 11-24:
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 "./src/Pff/Pff.v", line 2593, characters 11-24:
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 "./src/Pff/Pff.v", line 2593, characters 11-24:
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 "./src/Pff/Pff.v", line 2637, characters 6-19:
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 "./src/Pff/Pff.v", line 2637, characters 6-19:
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 "./src/Pff/Pff.v", line 3809, characters 52-59:
Warning: Notation lt_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_lt_pred instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 3809, characters 52-59:
Warning: Notation lt_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_lt_pred instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5413, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5417, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5413, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5417, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5429, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5433, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5429, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5433, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5489, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5494, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5489, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5494, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5504, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5508, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5504, characters 7-20:
Warning: Notation plus_lt_reg_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 "./src/Pff/Pff.v", line 5508, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 6081, characters 24-32:
Warning: Notation lt_O_neq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 6081, characters 24-32:
Warning: Notation lt_O_neq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12940, characters 12-18:
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 "./src/Pff/Pff.v", line 12940, characters 12-18:
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 "./src/Pff/Pff.v", line 12940, characters 12-18:
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 "./src/Pff/Pff.v", line 12940, characters 12-18:
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 "./src/Pff/Pff.v", line 16078, characters 11-17:
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 "./src/Pff/Pff.v", line 16078, characters 11-17:
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 "./src/Pff/Pff.v", line 16078, characters 11-17:
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 "./src/Pff/Pff.v", line 16078, characters 11-17:
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 "./src/Pff/Pff.v", line 16134, characters 11-17:
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 "./src/Pff/Pff.v", line 16134, characters 11-17:
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 "./src/Pff/Pff.v", line 16134, characters 11-17:
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 "./src/Pff/Pff.v", line 16134, characters 11-17:
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 "./src/Pff/Pff.v", line 16161, characters 11-17:
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 "./src/Pff/Pff.v", line 16161, characters 11-17:
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 "./src/Pff/Pff.v", line 16161, characters 11-17:
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 "./src/Pff/Pff.v", line 16161, characters 11-17:
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 "./src/Pff/Pff.v", line 17313, characters 12-18:
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 "./src/Pff/Pff.v", line 17313, characters 12-18:
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 "./src/Pff/Pff.v", line 17313, characters 12-18:
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 "./src/Pff/Pff.v", line 17313, characters 12-18:
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 "./src/Pff/Pff.v", line 17436, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17464, characters 14-18:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17464, characters 14-18:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17466, characters 12-16:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17466, 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 "./src/Pff/Pff.v", line 17466, characters 12-16:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17466, 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 "./src/Pff/Pff.v", line 17467, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17468, characters 6-17:
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 "./src/Pff/Pff.v", line 17468, characters 6-17:
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 "./src/Pff/Pff.v", line 17469, characters 11-22:
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 "./src/Pff/Pff.v", line 17469, characters 11-22:
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 "./src/Pff/Pff.v", line 17469, characters 11-22:
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 "./src/Pff/Pff.v", line 17470, characters 34-45:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17470, characters 47-51:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17470, characters 34-45:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17470, characters 47-51:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17471, characters 11-21:
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 "./src/Pff/Pff.v", line 17471, characters 11-21:
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 "./src/Pff/Pff.v", line 17471, characters 11-21:
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 "./src/Pff/Pff.v", line 17472, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17472, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17478, 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 "./src/Pff/Pff.v", line 17478, 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 "./src/Pff/Pff.v", line 17480, 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 "./src/Pff/Pff.v", line 17480, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, 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 "./src/Pff/Pff.v", line 17480, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17481, characters 6-17:
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 "./src/Pff/Pff.v", line 17481, characters 6-17:
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 "./src/Pff/Pff.v", line 17482, characters 11-22:
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 "./src/Pff/Pff.v", line 17482, characters 11-22:
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 "./src/Pff/Pff.v", line 17482, characters 11-22:
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 "./src/Pff/Pff.v", line 17483, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17483, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17483, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17483, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17484, characters 11-21:
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 "./src/Pff/Pff.v", line 17484, characters 11-21:
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 "./src/Pff/Pff.v", line 17484, characters 11-21:
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 "./src/Pff/Pff.v", line 17484, characters 11-21:
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 "./src/Pff/Pff.v", line 17486, characters 19-22:
Warning: Notation odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17486, characters 19-22:
Warning: Notation odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17487, characters 17-33:
Warning: Notation not_even_and_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_Odd_False (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17487, characters 17-33:
Warning: Notation not_even_and_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_Odd_False (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 6-12:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 20-25:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 33-39:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 47-52:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 60-66:
Warning: Notation even_O is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_O instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 6-12:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 20-25:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 33-39:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 47-52:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 60-66:
Warning: Notation even_O is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_O instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17490, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17490, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17495, characters 8-12:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17495, characters 8-12:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17496, characters 6-17:
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 "./src/Pff/Pff.v", line 17496, characters 6-17:
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 "./src/Pff/Pff.v", line 17497, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17497, 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 "./src/Pff/Pff.v", line 17497, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17497, 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 "./src/Pff/Pff.v", line 17498, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17498, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17499, characters 11-22:
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 "./src/Pff/Pff.v", line 17499, characters 11-22:
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 "./src/Pff/Pff.v", line 17499, characters 11-22:
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 "./src/Pff/Pff.v", line 17499, characters 11-22:
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 "./src/Pff/Pff.v", line 17500, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17500, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17500, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17500, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17502, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17502, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17503, characters 11-21:
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 "./src/Pff/Pff.v", line 17503, characters 11-21:
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 "./src/Pff/Pff.v", line 17503, characters 11-21:
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 "./src/Pff/Pff.v", line 17510, characters 15-22:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17510, characters 15-22:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17511, characters 15-19:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17511, characters 15-19:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17512, characters 6-17:
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 "./src/Pff/Pff.v", line 17512, characters 6-17:
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 "./src/Pff/Pff.v", line 17513, characters 25-36:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17513, characters 38-42:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17513, characters 25-36:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17513, characters 38-42:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17514, characters 0-57:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17514, characters 0-57:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17515, characters 11-22:
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 "./src/Pff/Pff.v", line 17515, characters 11-22:
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 "./src/Pff/Pff.v", line 17515, characters 11-22:
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 "./src/Pff/Pff.v", line 17515, characters 11-22:
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 "./src/Pff/Pff.v", line 17516, characters 28-39:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17516, characters 41-45:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17516, characters 28-39:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17516, characters 41-45:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17518, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17518, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17519, characters 11-21:
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 "./src/Pff/Pff.v", line 17519, characters 11-21:
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 "./src/Pff/Pff.v", line 17519, characters 11-21:
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 "./src/Pff/Pff.v", line 17519, characters 11-21:
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 "./src/Pff/Pff.v", line 17643, characters 37-41:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17688, characters 12-18:
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 "./src/Pff/Pff.v", line 17688, characters 12-18:
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 "./src/Pff/Pff.v", line 17688, characters 12-18:
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 "./src/Pff/Pff.v", line 17688, characters 12-18:
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 "./src/Pff/Pff.v", line 17734, characters 35-42:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17734, characters 35-42:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17735, characters 16-20:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17735, characters 16-20:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17736, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17736, 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 "./src/Pff/Pff.v", line 17736, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17736, 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 "./src/Pff/Pff.v", line 17737, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17737, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17738, characters 11-22:
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 "./src/Pff/Pff.v", line 17738, characters 11-22:
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 "./src/Pff/Pff.v", line 17738, characters 11-22:
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 "./src/Pff/Pff.v", line 17738, characters 11-22:
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 "./src/Pff/Pff.v", line 17753, characters 33-37:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17787, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17814, characters 34-38:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17882, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17882, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17883, 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 "./src/Pff/Pff.v", line 17884, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17883, 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 "./src/Pff/Pff.v", line 17884, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17913, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17913, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17914, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17915, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17914, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17915, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18040, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18067, characters 34-38:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18134, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18134, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18135, 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 "./src/Pff/Pff.v", line 18136, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18135, 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 "./src/Pff/Pff.v", line 18136, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18165, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18165, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18166, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18167, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18166, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18167, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18293, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18320, characters 33-37:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18349, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18509, characters 18-22:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18645, characters 11-17:
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 "./src/Pff/Pff.v", line 18645, characters 11-17:
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 "./src/Pff/Pff.v", line 18645, characters 11-17:
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 "./src/Pff/Pff.v", line 18645, characters 11-17:
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 "./src/Pff/Pff.v", line 18758, characters 18-22:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18892, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18919, characters 32-36:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Pff/Pff.vo
Building src/Pff/Pff2FlocqAux.vo
Finished src/Pff/Pff2FlocqAux.vo
Building src/Pff/Pff2Flocq.vo
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 943, characters 6-16:
Warning: Notation even_equiv is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_alt_Even instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 943, characters 6-16:
Warning: Notation even_equiv is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_alt_Even instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Pff/Pff2Flocq.vo
Building all
Finished all
Building html/index.html
Finished html/index.html
Building doc
Finished doc
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%install): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.NctMJ3
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ '[' 1 -eq 1 ']'
+ '[' /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT '!=' / ']'
+ rm -rf /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT
++ dirname /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT
+ mkdir -p /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ mkdir /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT
+ CFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CFLAGS
+ CXXFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CXXFLAGS
+ FFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FFLAGS
+ FCFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none --cap-lints=warn'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,--as-needed -Wl,--no-undefined -Wl,-z,relro -Wl,-z,now -Wl,-O1 -Wl,--build-id=sha1 -Wl,--enable-new-dtags -specs=/usr/lib/rpm/redhat/redhat-hardened-ld'
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd flocq-4.1.0
+ '[' 1 -eq 1 ']'
+ DESTDIR=/home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT
+ ./remake install
Building install
Finished install
+ find /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq -name .coq-native -prune -exec rm -r '{}' +
+ /usr/lib/rpm/check-buildroot
+ '[' -n '' ']'
+ /usr/share/spec-helper/clean_files
+ '[' -n '' ']'
+ /usr/share/spec-helper/compress_files .xz
+ '[' -n '' ']'
+ /usr/share/spec-helper/relink_symlinks
+ '[' -n '' ']'
+ /usr/share/spec-helper/clean_perl
+ '[' -n '' ']'
+ /usr/share/spec-helper/lib_symlinks
+ '[' -n '' ']'
+ /usr/share/spec-helper/gprintify
+ '[' -n '' ']'
+ /usr/share/spec-helper/fix_mo
+ '[' -n '' ']'
+ /usr/share/spec-helper/fix_pamd
+ '[' -n '' ']'
+ /usr/share/spec-helper/remove_info_dir
+ '[' -n '' ']'
+ /usr/share/spec-helper/fix_eol
+ '[' -n '' ']'
+ /usr/share/spec-helper/check_desktop_files
+ '[' -n '' ']'
+ /usr/share/spec-helper/check_elf_files
+ /usr/lib/rpm/brp-strip /usr/bin/strip
+ /usr/lib/rpm/brp-strip-comment-note /usr/bin/strip /usr/bin/objdump
+ /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip
+ /usr/lib/rpm/check-rpaths
+ /usr/lib/rpm/brp-remove-la-files
+ /usr/lib/rpm/redhat/brp-mangle-shebangs
+ env -u SOURCE_DATE_EPOCH /usr/lib/rpm/redhat/brp-python-bytecompile '' 1 0 -j16
+ /usr/lib/rpm/redhat/brp-python-hardlink
Reading /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/SPECPARTS/rpm-debuginfo.specpart
Processing files: coq-flocq-4.1.0-2.mga10.x86_64
Executing(%doc): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.1ezHOg
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ cd flocq-4.1.0
+ DOCDIR=/home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/share/doc/coq-flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export DOCDIR
+ /usr/bin/mkdir -p /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/flocq-4.1.0/AUTHORS /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/flocq-4.1.0/COPYING /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/flocq-4.1.0/NEWS.md /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/flocq-4.1.0/README.md /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/flocq-4.1.0/html /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT/usr/share/doc/coq-flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: coq-flocq = 4.1.0-2.mga10 coq-flocq(x86-64) = 4.1.0-2.mga10
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Checking for unpackaged file(s): /usr/lib/rpm/check-files /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build/BUILDROOT
Wrote: /home/pterjan/rpmbuild/RPMS/x86_64/coq-flocq-4.1.0-2.mga10.x86_64.rpm
Executing(rmbuild): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.Dcu65L
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ test -d /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ rm -rf /home/pterjan/rpmbuild/BUILD/coq-flocq-4.1.0-build
+ RPM_EC=0
++ jobs -p
+ exit 0
D: [iurt_root_command] Success!