D: [iurt_root_command] chroot
Installing /home/pterjan/rpmbuild/SRPMS/coq-flocq-4.1.0-1.mga9.src.rpm
Building target platforms: x86_64
Building for target x86_64
Executing(%prep): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.cjkIyf
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ cd /home/pterjan/rpmbuild/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 .
+ /usr/lib/rpm/rpmuncompress /home/pterjan/rpmbuild/SOURCES/flocq-4.1.0-mga-coqdoc-url.patch
+ /usr/bin/patch -p1 -s --fuzz=0 --no-backup-if-mismatch -f
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.vw8H99
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD
+ 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 for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
configure: building remake...
/usr/bin/ld: /tmp/cc5QfqX1.o: in function `main':
remake.cpp:(.text.startup+0xb13): 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
warning: use --coqlib_url to specify stdlib's URL starting with Coq 8.14
coqdoc: cannot find coqdoc style file: http://coq.inria.fr/distrib/current/stdlib/../coq-core/tools/coqdoc/coqdoc.css
Failed to build html/index.html
Failed to build doc
error: Bad exit status from /home/pterjan/rpmbuild/tmp/rpm-tmp.vw8H99 (%build)

RPM build errors:
    Bad exit status from /home/pterjan/rpmbuild/tmp/rpm-tmp.vw8H99 (%build)
I: [iurt_root_command] ERROR: chroot