D: [iurt_root_command] chroot
Building target platforms: x86_64
Building for target x86_64
Installing /home/pterjan/rpmbuild/SRPMS/coq-flocq-4.2.1-1.mga10.src.rpm
Executing(%mkbuilddir): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.VBCmkQ
Executing(%prep): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.XSZhmc
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ rm -rf flocq-4.2.1
+ /usr/lib/rpm/rpmuncompress -x /home/pterjan/rpmbuild/SOURCES/flocq-4.2.1.tar.gz
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd flocq-4.2.1
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ sed -i 's,\(--coqlib \)[^[:blank:]]*,\1/usr/lib64/ocaml/coq,' Remakefile.in
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.C8gA9o
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ CFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CFLAGS
+ CXXFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CXXFLAGS
+ FFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FFLAGS
+ FCFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none --cap-lints=warn'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,--as-needed -Wl,--no-undefined -Wl,-z,relro -Wl,-z,now -Wl,-O1 -Wl,--build-id=sha1 -Wl,--enable-new-dtags -specs=/usr/lib/rpm/redhat/redhat-hardened-ld'
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd flocq-4.2.1
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ ./configure
checking for coqc... /usr/bin/coqc
checking Coq version... 8.20.1
checking for coqdep... /usr/bin/coqdep
checking for coqdoc... /usr/bin/coqdoc
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C++... yes
checking whether g++ accepts -g... yes
checking for g++ option to enable C++11 features... none needed
configure: building remake...
/usr/bin/ld: /tmp/cc1nWmIM.o: in function `main':
remake.cpp:(.text.startup+0xec3): warning: the use of `tempnam' is dangerous, better use `mkstemp'
configure: creating ./config.status
config.status: creating Remakefile
config.status: creating src/Version.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 327, characters 2-6:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 327, characters 8-12:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 327, characters 28-32:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 361, characters 10-14:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 361, characters 31-35:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 367, characters 25-29:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 367, characters 25-29:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 367, characters 25-29:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 367, characters 25-29:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 855, characters 31-35:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Zaux.v", line 858, characters 14-18:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
Finished src/Core/Zaux.vo
File "./src/Core/Raux.v", line 189, characters 6-14:
Warning: Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 189, characters 6-14:
Warning: Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 571, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 571, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 583, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 583, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1312, characters 35-43:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1312, characters 35-43:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1312, characters 35-43:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1325, characters 36-44:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1325, characters 36-44:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1325, characters 36-44:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1884, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1884, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1994, characters 12-22:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Raux.v", line 1994, characters 12-22:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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
File "./src/Core/Float_prop.v", line 461, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Float_prop.v", line 461, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Float_prop.v", line 471, characters 16-23:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Float_prop.v", line 471, characters 16-23:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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
File "./src/Core/Ulp.v", line 1424, characters 10-20:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Ulp.v", line 1424, characters 10-20:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Ulp.v", line 1451, characters 24-34:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Core/Ulp.v", line 1451, characters 24-34:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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 183, characters 13-23:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Bracket.v", line 183, characters 13-23:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Bracket.v", line 629, characters 85-89:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Bracket.v", line 660, characters 63-67:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
Finished src/Calc/Bracket.vo
Building src/Calc/Div.vo
File "./src/Calc/Div.v", line 89, characters 14-21:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Div.v", line 89, characters 14-21:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Div.v", line 98, characters 14-21:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Div.v", line 98, characters 14-21:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Div.v", line 115, characters 12-19:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Div.v", line 115, characters 12-19:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Div.v", line 117, characters 12-19:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Div.v", line 117, characters 12-19:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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
File "./src/Calc/Round.v", line 612, characters 41-45:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/Calc/Round.v", line 1146, characters 43-47:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Div_sqrt_error.v", line 204, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Div_sqrt_error.v", line 204, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Div_sqrt_error.v", line 211, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Div_sqrt_error.v", line 211, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Div_sqrt_error.v", line 218, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Div_sqrt_error.v", line 218, characters 10-17:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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 1456, characters 14-20:
Warning: Notation double is deprecated since 8.19. Use Rplus_diag.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 1456, characters 14-20:
Warning: Notation double is deprecated since 8.19. Use Rplus_diag.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 1456, characters 14-20:
Warning: Notation double is deprecated since 8.19. Use Rplus_diag.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 2637, characters 8-18:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 2637, characters 8-18:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 3057, characters 8-18:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 3057, characters 8-18:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 3493, characters 25-32:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 3493, characters 25-32:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 3497, characters 31-38:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 3497, characters 31-38:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 4322, characters 12-20:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 4322, characters 12-20:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 4322, characters 12-20:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 4337, characters 12-20:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 4337, characters 12-20:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Prop/Double_rounding.v", line 4337, characters 12-20:
Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
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-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
Finished src/Prop/Double_rounding.vo
Building src/IEEE754/BinarySingleNaN.vo
File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2473, characters 16-18:
Warning: Unused variable sx might be a misspelled constructor. Use _ or _sx
to silence this warning. [unused-pattern-matching-variable,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2987, characters 29-36:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 2987, characters 29-36:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 3026, characters 29-36:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/BinarySingleNaN.v", line 3026, characters 29-36:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
Finished src/IEEE754/BinarySingleNaN.vo
Building src/IEEE754/Binary.vo
Finished src/IEEE754/Binary.vo
Building src/IEEE754/Bits.vo
File "./src/IEEE754/Bits.v", line 80, characters 25-29:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./src/IEEE754/Bits.v", line 80, characters 36-40:
Warning: Notation Zmod is deprecated since 8.17.
Use Coq.ZArith.BinIntDef.Z.modulo instead
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
Finished src/IEEE754/Bits.vo
Building src/IEEE754/PrimFloat.vo
Finished src/IEEE754/PrimFloat.vo
Building src/Pff/Pff.vo
File "./src/Pff/Pff.v", line 68, characters 30-45:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Pff/Pff.v", line 69, characters 24-33:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Pff/Pff.v", line 70, characters 23-31:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Pff/Pff.v", line 71, characters 30-45:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Pff/Pff.v", line 72, characters 25-35:
Warning: Notation Rlt_Rminus is deprecated since 8.19.
Use the bidirectional version Rlt_0_minus instead.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
File "./src/Pff/Pff.v", line 73, characters 26-37:
Warning: Notation powerRZ_inv is deprecated since 8.16. Use powerRZ_inv'.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Pff/Pff.v", line 74, characters 26-37:
Warning: Notation powerRZ_neg is deprecated since 8.16.
Use powerRZ_neg' and powerRZ_inv'.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
File "./src/Pff/Pff.v", line 80, characters 22-29:
Warning: Notation IZR_neq is deprecated since 8.19.
Use eq_IZR_contrapositive.
[deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default]
Finished src/Pff/Pff.vo
Building src/Pff/Pff2FlocqAux.vo
Finished src/Pff/Pff2FlocqAux.vo
Building src/Pff/Pff2Flocq.vo
Finished src/Pff/Pff2Flocq.vo
Building all
Finished all
Building html/index.html
Finished html/index.html
Building doc
Finished doc
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%install): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.qVEePC
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ '[' 1 -eq 1 ']'
+ '[' /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT '!=' / ']'
+ rm -rf /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT
++ dirname /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT
+ mkdir -p /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ mkdir /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT
+ CFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CFLAGS
+ CXXFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full'
+ export CXXFLAGS
+ FFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FFLAGS
+ FCFLAGS='-O2 -g -pipe -Wformat -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -m64 -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection=full '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none --cap-lints=warn'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,--as-needed -Wl,--no-undefined -Wl,-z,relro -Wl,-z,now -Wl,-O1 -Wl,--build-id=sha1 -Wl,--enable-new-dtags -specs=/usr/lib/rpm/redhat/redhat-hardened-ld'
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd flocq-4.2.1
+ '[' 1 -eq 1 ']'
+ DESTDIR=/home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT
+ ./remake install
Building install
Finished install
+ find /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq -name .coq-native -prune -exec rm -r '{}' +
+ /usr/lib/rpm/check-buildroot
+ '[' -n '' ']'
+ /usr/share/spec-helper/clean_files
+ '[' -n '' ']'
+ /usr/share/spec-helper/compress_files .xz
+ '[' -n '' ']'
+ /usr/share/spec-helper/relink_symlinks
+ '[' -n '' ']'
+ /usr/share/spec-helper/clean_perl
+ '[' -n '' ']'
+ /usr/share/spec-helper/lib_symlinks
+ '[' -n '' ']'
+ /usr/share/spec-helper/gprintify
+ '[' -n '' ']'
+ /usr/share/spec-helper/fix_mo
+ '[' -n '' ']'
+ /usr/share/spec-helper/fix_pamd
+ '[' -n '' ']'
+ /usr/share/spec-helper/remove_info_dir
+ '[' -n '' ']'
+ /usr/share/spec-helper/fix_eol
+ '[' -n '' ']'
+ /usr/share/spec-helper/check_desktop_files
+ '[' -n '' ']'
+ /usr/share/spec-helper/check_elf_files
+ /usr/lib/rpm/brp-strip /usr/bin/strip
+ /usr/lib/rpm/brp-strip-comment-note /usr/bin/strip /usr/bin/objdump
+ /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip
+ /usr/lib/rpm/check-rpaths
+ /usr/lib/rpm/brp-remove-la-files
+ /usr/lib/rpm/redhat/brp-mangle-shebangs
+ env -u SOURCE_DATE_EPOCH /usr/lib/rpm/redhat/brp-python-bytecompile '' 1 0 -j16
+ /usr/lib/rpm/redhat/brp-python-hardlink
Reading /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/SPECPARTS/rpm-debuginfo.specpart
Processing files: coq-flocq-4.2.1-1.mga10.x86_64
Executing(%doc): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.H5I3Hz
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ cd flocq-4.2.1
+ DOCDIR=/home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/share/doc/coq-flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export DOCDIR
+ /usr/bin/mkdir -p /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/flocq-4.2.1/AUTHORS /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/flocq-4.2.1/COPYING /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/flocq-4.2.1/NEWS.md /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/flocq-4.2.1/README.md /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/share/doc/coq-flocq
+ cp -pr /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/flocq-4.2.1/html /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT/usr/share/doc/coq-flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: coq-flocq = 4.2.1-1.mga10 coq-flocq(x86-64) = 4.2.1-1.mga10
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Checking for unpackaged file(s): /usr/lib/rpm/check-files /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build/BUILDROOT
Wrote: /home/pterjan/rpmbuild/RPMS/x86_64/coq-flocq-4.2.1-1.mga10.x86_64.rpm
Executing(rmbuild): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.ZSX8sT
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ test -d /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ rm -rf /home/pterjan/rpmbuild/BUILD/coq-flocq-4.2.1-build
+ RPM_EC=0
++ jobs -p
+ exit 0
D: [iurt_root_command] Success!