Mock Version: 3.5 Mock Version: 3.5 Mock Version: 3.5 ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --noclean --target riscv64 --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f40-build-763042-122273/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=timeout=1209600uid=991gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --noclean --target riscv64 --nodeps /builddir/build/SPECS/flocq.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'} and shell False Building target platforms: riscv64 Building for target riscv64 setting SOURCE_DATE_EPOCH=1702339200 Wrote: /builddir/build/SRPMS/flocq-4.1.1-7.fc40.src.rpm Child return code was: 0 ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --noclean --target riscv64 --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f40-build-763042-122273/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=timeout=1209600uid=991gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --noclean --target riscv64 --nodeps /builddir/build/SPECS/flocq.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'} and shell False Building target platforms: riscv64 Building for target riscv64 setting SOURCE_DATE_EPOCH=1702339200 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.42rtAX + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea + /usr/lib/rpm/rpmuncompress -x /builddir/build/SOURCES/flocq-4.1.1.tar.gz + STATUS=0 + '[' 0 -ne 0 ']' + cd flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea + rm -rf /builddir/build/BUILD/flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea-SPECPARTS + /usr/bin/mkdir -p /builddir/build/BUILD/flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea-SPECPARTS + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . + sed -i 's,\(--coqlib \)[^[:blank:]]*,\1/usr/lib64/ocaml/coq,' Remakefile.in + autoconf -f configure.in:5: warning: prefer named diversions + RPM_EC=0 ++ jobs -p + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.dSTUJb + umask 022 + cd /builddir/build/BUILD + CFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Werror=implicit-function-declaration -Werror=implicit-int -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer ' + export CFLAGS + CXXFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer ' + export CXXFLAGS + FFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules ' + export FFLAGS + FCFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules ' + export FCFLAGS + VALAFLAGS=-g + export VALAFLAGS + RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-Wl,-z,relro -Clink-arg=-Wl,-z,now -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes --cap-lints=warn' + export RUSTFLAGS + LDFLAGS='-Wl,-z,relro -Wl,--as-needed -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes ' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib64: + export LT_SYS_LIBRARY_PATH + CC=gcc + export CC + CXX=g++ + export CXX + cd flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea + ./configure checking for coqc... /usr/bin/coqc checking Coq version... 8.17.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/ccVOaWUT.o: in function `.LEHE328': remake.cpp:(.text.startup+0x764): 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 + rm -f remake + ln -s /usr/bin/remake remake + remake -d -j4 all doc Building src/Version.vo Building src/Core/Raux.vo Building src/Core/Zaux.vo Building src/Core/Defs.vo /usr/bin/coqdep -R src Flocq src/Version.v | ./remake -r src/Version.vo /usr/bin/coqdep -R src Flocq src/Core/Raux.v | ./remake -r src/Core/Raux.vo /usr/bin/coqdep -R src Flocq src/Core/Zaux.v | ./remake -r src/Core/Zaux.vo /usr/bin/coqdep -R src Flocq src/Core/Defs.v | ./remake -r src/Core/Defs.vo /usr/bin/coqc -q -R src Flocq src/Version.v Building src/Core/Digits.vo /usr/bin/coqdep -R src Flocq src/Core/Digits.v | ./remake -r src/Core/Digits.vo Building src/Core/Float_prop.vo /usr/bin/coqdep -R src Flocq src/Core/Float_prop.v | ./remake -r src/Core/Float_prop.vo /usr/bin/coqc -q -R src Flocq src/Core/Zaux.v Building src/Core/FIX.vo /usr/bin/coqdep -R src Flocq src/Core/FIX.v | ./remake -r src/Core/FIX.vo Building src/Core/FLT.vo /usr/bin/coqdep -R src Flocq src/Core/FLT.v | ./remake -r src/Core/FLT.vo Building src/Core/Generic_fmt.vo /usr/bin/coqdep -R src Flocq src/Core/Generic_fmt.v | ./remake -r src/Core/Generic_fmt.vo Building src/Core/FLX.vo /usr/bin/coqdep -R src Flocq src/Core/FLX.v | ./remake -r src/Core/FLX.vo Building src/Core/Round_NE.vo Building src/Core/Round_pred.vo /usr/bin/coqdep -R src Flocq src/Core/Round_NE.v | ./remake -r src/Core/Round_NE.vo /usr/bin/coqdep -R src Flocq src/Core/Round_pred.v | ./remake -r src/Core/Round_pred.vo Building src/Core/Ulp.vo Building src/Core/FTZ.vo /usr/bin/coqdep -R src Flocq src/Core/FTZ.v | ./remake -r src/Core/FTZ.vo /usr/bin/coqdep -R src Flocq src/Core/Ulp.v | ./remake -r src/Core/Ulp.vo Building src/Core/Core.vo /usr/bin/coqdep -R src Flocq src/Core/Core.v | ./remake -r src/Core/Core.vo Building src/Calc/Bracket.vo /usr/bin/coqdep -R src Flocq src/Calc/Bracket.v | ./remake -r src/Calc/Bracket.vo Building src/Calc/Div.vo /usr/bin/coqdep -R src Flocq src/Calc/Div.v | ./remake -r src/Calc/Div.vo Building src/Calc/Operations.vo /usr/bin/coqdep -R src Flocq src/Calc/Operations.v | ./remake -r src/Calc/Operations.vo File "./src/Version.v", line 30, characters 6-18: Warning: Unused variable Empty_string might be a misspelled constructor. Use _ or _Empty_string to silence this warning. [unused-pattern-matching-variable,pattern-matching] Finished src/Version.vo Building src/Calc/Plus.vo /usr/bin/coqdep -R src Flocq src/Calc/Plus.v | ./remake -r src/Calc/Plus.vo Building src/Calc/Round.vo /usr/bin/coqdep -R src Flocq src/Calc/Round.v | ./remake -r src/Calc/Round.vo Building src/Calc/Sqrt.vo /usr/bin/coqdep -R src Flocq src/Calc/Sqrt.v | ./remake -r src/Calc/Sqrt.vo Building src/Prop/Div_sqrt_error.vo /usr/bin/coqdep -R src Flocq src/Prop/Div_sqrt_error.v | ./remake -r src/Prop/Div_sqrt_error.vo Building src/Prop/Mult_error.vo /usr/bin/coqdep -R src Flocq src/Prop/Mult_error.v | ./remake -r src/Prop/Mult_error.vo Building src/Prop/Plus_error.vo /usr/bin/coqdep -R src Flocq src/Prop/Plus_error.v | ./remake -r src/Prop/Plus_error.vo Building src/Prop/Relative.vo /usr/bin/coqdep -R src Flocq src/Prop/Relative.v | ./remake -r src/Prop/Relative.vo Building src/Prop/Sterbenz.vo /usr/bin/coqdep -R src Flocq src/Prop/Sterbenz.v | ./remake -r src/Prop/Sterbenz.vo Building src/Prop/Round_odd.vo /usr/bin/coqdep -R src Flocq src/Prop/Round_odd.v | ./remake -r src/Prop/Round_odd.vo Building src/Prop/Double_rounding.vo /usr/bin/coqdep -R src Flocq src/Prop/Double_rounding.v | ./remake -r src/Prop/Double_rounding.vo Building src/IEEE754/BinarySingleNaN.vo /usr/bin/coqdep -R src Flocq src/IEEE754/BinarySingleNaN.v | ./remake -r src/IEEE754/BinarySingleNaN.vo Building src/IEEE754/Binary.vo /usr/bin/coqdep -R src Flocq src/IEEE754/Binary.v | ./remake -r src/IEEE754/Binary.vo Building src/IEEE754/Bits.vo /usr/bin/coqdep -R src Flocq src/IEEE754/Bits.v | ./remake -r src/IEEE754/Bits.vo Building src/IEEE754/Int63Compat.vo /usr/bin/coqdep -R src Flocq src/IEEE754/Int63Compat.v | ./remake -r src/IEEE754/Int63Compat.vo Building src/IEEE754/Int63Copy.vo /usr/bin/coqdep -R src Flocq src/IEEE754/Int63Copy.v | ./remake -r src/IEEE754/Int63Copy.vo Building src/IEEE754/PrimFloat.vo /usr/bin/coqdep -R src Flocq src/IEEE754/PrimFloat.v | ./remake -r src/IEEE754/PrimFloat.vo Building src/Pff/Pff.vo /usr/bin/coqdep -R src Flocq src/Pff/Pff.v | ./remake -r src/Pff/Pff.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/Int63Copy.v Building src/Pff/Pff2FlocqAux.vo /usr/bin/coqdep -R src Flocq src/Pff/Pff2FlocqAux.v | ./remake -r src/Pff/Pff2FlocqAux.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,deprecated] 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,deprecated] 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,deprecated] 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,deprecated] 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,deprecated] /usr/bin/coqc -q -R src Flocq src/Pff/Pff.v 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,deprecated] 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,deprecated] 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,deprecated] 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,deprecated] Building src/Pff/Pff2Flocq.vo /usr/bin/coqdep -R src Flocq src/Pff/Pff2Flocq.v | ./remake -r src/Pff/Pff2Flocq.vo 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,deprecated] File "./src/Core/Zaux.v", line 858, characters 0-19: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition,deprecated] File "./src/Core/Zaux.v", line 858, characters 0-19: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo 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 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 /usr/bin/coqc -q -R src Flocq src/Core/Raux.v /usr/bin/coqc -q -R src Flocq src/Core/Digits.v Finished src/IEEE754/Int63Copy.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/Int63Compat.v 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] Finished src/IEEE754/Int63Compat.vo 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/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/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/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/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/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/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/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 /usr/bin/coqc -q -R src Flocq src/Core/Defs.v Finished src/Core/Digits.vo Finished src/Core/Defs.vo /usr/bin/coqc -q -R src Flocq src/Core/Round_pred.v /usr/bin/coqc -q -R src Flocq src/Core/Float_prop.v Finished src/Core/Float_prop.vo /usr/bin/coqc -q -R src Flocq src/Calc/Operations.v /usr/bin/coqc -q -R src Flocq src/Calc/Bracket.v File "./src/Pff/Pff.v", line 2322, 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 2322, 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 2336, 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 2336, 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 2336, 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] Finished src/Core/Round_pred.vo /usr/bin/coqc -q -R src Flocq src/Core/Generic_fmt.v File "./src/Pff/Pff.v", line 2489, 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 2489, 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 2489, 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 2489, 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 2497, 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 2497, 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 2497, 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 2590, 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 2590, 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 2592, 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 2592, 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 2592, 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 2592, 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] Finished src/Calc/Operations.vo File "./src/Pff/Pff.v", line 2636, 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 2636, 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/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,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] 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 660, characters 63-67: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition,deprecated] Finished src/Calc/Bracket.vo Finished src/Core/Generic_fmt.vo /usr/bin/coqc -q -R src Flocq src/Calc/Sqrt.v /usr/bin/coqc -q -R src Flocq src/Prop/Sterbenz.v /usr/bin/coqc -q -R src Flocq src/Calc/Div.v File "./src/Pff/Pff.v", line 3808, 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 3808, 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] Finished src/Prop/Sterbenz.vo /usr/bin/coqc -q -R src Flocq src/Core/Ulp.v Finished src/Calc/Sqrt.vo Finished src/Calc/Div.vo File "./src/Pff/Pff.v", line 5347, 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 5347, 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 5347, 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 5347, 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 5347, 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 5347, 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 5352, 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 5352, 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 5352, 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 5352, 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 5371, 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 5371, 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 5371, 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 5371, 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 5412, 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 5416, 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 5412, 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 5416, 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 5428, 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 5432, 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 5428, 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 5432, 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 5488, 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 5493, 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 5488, 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 5493, 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 5503, 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 5507, 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 5503, 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 5507, 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 6080, 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 6080, 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] Finished src/Core/Ulp.vo /usr/bin/coqc -q -R src Flocq src/Core/Round_NE.v Finished src/Core/Round_NE.vo /usr/bin/coqc -q -R src Flocq src/Core/FIX.v Finished src/Core/FIX.vo /usr/bin/coqc -q -R src Flocq src/Core/FLX.v Finished src/Core/FLX.vo /usr/bin/coqc -q -R src Flocq src/Core/FLT.v /usr/bin/coqc -q -R src Flocq src/Core/FTZ.v Finished src/Core/FTZ.vo Finished src/Core/FLT.vo /usr/bin/coqc -q -R src Flocq src/Core/Core.v Finished src/Core/Core.vo /usr/bin/coqc -q -R src Flocq src/Prop/Round_odd.v /usr/bin/coqc -q -R src Flocq src/Prop/Double_rounding.v /usr/bin/coqc -q -R src Flocq src/Prop/Relative.v 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 /usr/bin/coqc -q -R src Flocq src/Prop/Plus_error.v Finished src/Prop/Round_odd.vo /usr/bin/coqc -q -R src Flocq src/Calc/Round.v Finished src/Prop/Plus_error.vo /usr/bin/coqc -q -R src Flocq src/Prop/Mult_error.v 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,deprecated] 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,deprecated] Finished src/Calc/Round.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/BinarySingleNaN.v Finished src/Prop/Mult_error.vo /usr/bin/coqc -q -R src Flocq src/Prop/Div_sqrt_error.v 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/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/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 /usr/bin/coqc -q -R src Flocq src/Calc/Plus.v Finished src/Calc/Plus.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] File "./src/Pff/Pff.v", line 11654, 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 11654, 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 11654, 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 11654, 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 11654, characters 2-17: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition,deprecated] File "./src/IEEE754/BinarySingleNaN.v", line 2434, characters 16-18: Warning: Unused variable sx might be a misspelled constructor. Use _ or _sx to silence this warning. [unused-pattern-matching-variable,pattern-matching] File "./src/Pff/Pff.v", line 11698, 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 11698, 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 11698, 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 11698, 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 11698, characters 2-17: 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] File "./src/Pff/Pff.v", line 11808, 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 11808, 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 11808, 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 11808, 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 11808, characters 8-23: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition,deprecated] Finished src/Prop/Double_rounding.vo File "./src/Pff/Pff.v", line 11904, 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 11904, 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 11904, 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 11904, 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 11904, 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 11936, 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 11936, 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 11936, 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 11936, 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 11936, 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 12024, 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 12024, 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 12024, 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 12024, 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 12024, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, 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 12037, characters 15-30: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition,deprecated] Finished src/IEEE754/BinarySingleNaN.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/Binary.v /usr/bin/coqc -q -R src Flocq src/IEEE754/PrimFloat.v 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 Finished src/IEEE754/Binary.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/Bits.v 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,deprecated] 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,deprecated] File "./src/Pff/Pff.v", line 12939, 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 12939, 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 12939, 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 12939, 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] Finished src/IEEE754/Bits.vo 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 /usr/bin/coqc -q -R src Flocq src/Pff/Pff2FlocqAux.v Finished src/Pff/Pff2FlocqAux.vo /usr/bin/coqc -q -R src Flocq src/Pff/Pff2Flocq.v 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 rm -rf html mkdir -p html /usr/bin/coqdoc -toc -interpolate -utf8 -html -g -R src Flocq -d html \ --coqlib_url http://coq.inria.fr/distrib/current/stdlib \ src/Version.v src/Core/Raux.v src/Core/Zaux.v src/Core/Defs.v src/Core/Digits.v src/Core/Float_prop.v src/Core/FIX.v src/Core/FLT.v src/Core/FLX.v src/Core/FTZ.v src/Core/Generic_fmt.v src/Core/Round_pred.v src/Core/Round_NE.v src/Core/Ulp.v src/Core/Core.v src/Calc/Bracket.v src/Calc/Div.v src/Calc/Operations.v src/Calc/Plus.v src/Calc/Round.v src/Calc/Sqrt.v src/Prop/Div_sqrt_error.v src/Prop/Mult_error.v src/Prop/Plus_error.v src/Prop/Relative.v src/Prop/Sterbenz.v src/Prop/Round_odd.v src/Prop/Double_rounding.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Binary.v src/IEEE754/Bits.v src/IEEE754/Int63Compat.v src/IEEE754/Int63Copy.v src/IEEE754/PrimFloat.v src/Pff/Pff.v src/Pff/Pff2FlocqAux.v src/Pff/Pff2Flocq.v for f in html/*.html; do sed -e 's;Index;Go back to the Main page or Index.;' -i $f done Finished html/index.html Building doc Finished doc + RPM_EC=0 ++ jobs -p + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.ahPHDo + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64 ++ dirname /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64 + CFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Werror=implicit-function-declaration -Werror=implicit-int -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer ' + export CFLAGS + CXXFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer ' + export CXXFLAGS + FFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules ' + export FFLAGS + FCFLAGS='-O2 -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules ' + export FCFLAGS + VALAFLAGS=-g + export VALAFLAGS + RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-Wl,-z,relro -Clink-arg=-Wl,-z,now -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes --cap-lints=warn' + export RUSTFLAGS + LDFLAGS='-Wl,-z,relro -Wl,--as-needed -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes ' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib64: + export LT_SYS_LIBRARY_PATH + CC=gcc + export CC + CXX=g++ + export CXX + cd flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea + sed -i s,/usr/lib64,/builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/lib64, Remakefile + remake install Building install Finished install + cp -p src/Version.v /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/lib64/ocaml/coq/user-contrib/Flocq + cp -p src/Calc/Bracket.v src/Calc/Div.v src/Calc/Operations.v src/Calc/Plus.v src/Calc/Round.v src/Calc/Sqrt.v /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/lib64/ocaml/coq/user-contrib/Flocq/Calc + cp -p src/Core/Core.v src/Core/Defs.v src/Core/Digits.v src/Core/FIX.v src/Core/FLT.v src/Core/FLX.v src/Core/FTZ.v src/Core/Float_prop.v src/Core/Generic_fmt.v src/Core/Raux.v src/Core/Round_NE.v src/Core/Round_pred.v src/Core/Ulp.v src/Core/Zaux.v /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/lib64/ocaml/coq/user-contrib/Flocq/Core + cp -p src/IEEE754/Binary.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Bits.v src/IEEE754/Int63Compat.v src/IEEE754/Int63Copy.v src/IEEE754/PrimFloat.v /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/lib64/ocaml/coq/user-contrib/Flocq/IEEE754 + cp -p src/Pff/Pff.v src/Pff/Pff2Flocq.v src/Pff/Pff2FlocqAux.v /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/lib64/ocaml/coq/user-contrib/Flocq/Pff + cp -p src/Prop/Div_sqrt_error.v src/Prop/Double_rounding.v src/Prop/Mult_error.v src/Prop/Plus_error.v src/Prop/Relative.v src/Prop/Round_odd.v src/Prop/Sterbenz.v /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/lib64/ocaml/coq/user-contrib/Flocq/Prop + /usr/lib/rpm/check-buildroot + /usr/lib/rpm/redhat/brp-ldconfig + /usr/lib/rpm/brp-compress + /usr/lib/rpm/brp-strip /usr/bin/strip + /usr/lib/rpm/brp-strip-comment-note /usr/bin/strip /usr/bin/objdump + /usr/lib/rpm/redhat/brp-strip-lto /usr/bin/strip + /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip + /usr/lib/rpm/check-rpaths + /usr/lib/rpm/redhat/brp-mangle-shebangs + /usr/lib/rpm/brp-remove-la-files + env /usr/lib/rpm/redhat/brp-python-bytecompile '' 1 0 -j4 + /usr/lib/rpm/redhat/brp-python-hardlink Processing files: flocq-4.1.1-7.fc40.riscv64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.ygqLwN + umask 022 + cd /builddir/build/BUILD + cd flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea + DOCDIR=/builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/doc/flocq + export LC_ALL= + LC_ALL= + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea/AUTHORS /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea/NEWS.md /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea/README.md /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea/html /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/doc/flocq + RPM_EC=0 ++ jobs -p + exit 0 Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.smv8w1 + umask 022 + cd /builddir/build/BUILD + cd flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea + LICENSEDIR=/builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/licenses/flocq + export LC_ALL= + LC_ALL= + export LICENSEDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/licenses/flocq + cp -pr /builddir/build/BUILD/flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea/COPYING /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64/usr/share/licenses/flocq + RPM_EC=0 ++ jobs -p + exit 0 Provides: flocq = 4.1.1-7.fc40 flocq(riscv-64) = 4.1.1-7.fc40 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: flocq-source-4.1.1-7.fc40.riscv64 Provides: flocq-source = 4.1.1-7.fc40 flocq-source(riscv-64) = 4.1.1-7.fc40 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 /builddir/build/BUILDROOT/flocq-4.1.1-7.fc40.riscv64 Wrote: /builddir/build/RPMS/flocq-source-4.1.1-7.fc40.riscv64.rpm Wrote: /builddir/build/RPMS/flocq-4.1.1-7.fc40.riscv64.rpm Child return code was: 0