Mock Version: 5.5
Mock Version: 5.5
Mock Version: 5.5
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --noclean --target ppc64le --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f38-build-50763671-6068491/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x7fff9a73fe90>timeout=201600uid=1000gid=425user='mockbuild'nspawn_args=['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.tg81w61w:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']unshare_net=TrueprintOutput=False)
Using nspawn with args ['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.tg81w61w:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']
Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', '89ae98c51e144b83a9b0d8a324364170', '-D', '/var/lib/mock/f38-build-50763671-6068491/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.tg81w61w:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;<mock-chroot>\\007"', '--setenv=PS1=<mock-chroot> \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bs --noclean --target ppc64le --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;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False
Building target platforms: ppc64le
Building for target ppc64le
setting SOURCE_DATE_EPOCH=1697587200
Wrote: /builddir/build/SRPMS/flocq-4.1.1-2.fc38.src.rpm
Child return code was: 0
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --noclean --target ppc64le --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f38-build-50763671-6068491/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x7fff9a73fe90>timeout=201600uid=1000gid=425user='mockbuild'nspawn_args=['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.tg81w61w:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']unshare_net=TrueprintOutput=False)
Using nspawn with args ['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.tg81w61w:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']
Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', 'b9c8de067fbe48299a1a8c9e29dd0f8a', '-D', '/var/lib/mock/f38-build-50763671-6068491/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.tg81w61w:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;<mock-chroot>\\007"', '--setenv=PS1=<mock-chroot> \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bb --noclean --target ppc64le --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;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False
Building target platforms: ppc64le
Building for target ppc64le
setting SOURCE_DATE_EPOCH=1697587200
Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.Ok2rIw
+ 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
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ sed -i 's,\(--coqlib \)[^[:blank:]]*,\1/usr/lib64/ocaml/coq,' Remakefile.in
+ sed -i 's/@COQC@.* -R src Flocq/& -native-compiler yes/' 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.rIhA4G
+ umask 022
+ cd /builddir/build/BUILD
+ CFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection '
+ export CFLAGS
+ CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection '
+ export CXXFLAGS
+ FFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules '
+ export FFLAGS
+ FCFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ 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  '
+ 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/ccOLvl0O.o: in function `main':
remake.cpp:(.text.startup+0xc64): 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 -j8 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
Building src/Core/Digits.vo
/usr/bin/coqdep -R src Flocq src/Core/Raux.v | ./remake -r src/Core/Raux.vo
Building src/Core/Float_prop.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
Building src/Core/FIX.vo
Building src/Core/FLT.vo
/usr/bin/coqdep -R src Flocq src/Core/Digits.v | ./remake -r src/Core/Digits.vo
/usr/bin/coqdep -R src Flocq src/Core/FIX.v | ./remake -r src/Core/FIX.vo
/usr/bin/coqdep -R src Flocq src/Core/Float_prop.v | ./remake -r src/Core/Float_prop.vo
/usr/bin/coqdep -R src Flocq src/Core/FLT.v | ./remake -r src/Core/FLT.vo
Building src/Core/FLX.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Version.v
Building src/Core/FTZ.vo
/usr/bin/coqdep -R src Flocq src/Core/FLX.v | ./remake -r src/Core/FLX.vo
/usr/bin/coqdep -R src Flocq src/Core/FTZ.v | ./remake -r src/Core/FTZ.vo
Building src/Core/Generic_fmt.vo
Building src/Core/Round_NE.vo
/usr/bin/coqdep -R src Flocq src/Core/Generic_fmt.v | ./remake -r src/Core/Generic_fmt.vo
/usr/bin/coqdep -R src Flocq src/Core/Round_NE.v | ./remake -r src/Core/Round_NE.vo
Building src/Core/Round_pred.vo
/usr/bin/coqdep -R src Flocq src/Core/Round_pred.v | ./remake -r src/Core/Round_pred.vo
Building src/Core/Ulp.vo
/usr/bin/coqdep -R src Flocq src/Core/Ulp.v | ./remake -r src/Core/Ulp.vo
Building src/Core/Core.vo
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
/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
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Zaux.v
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
Building src/Prop/Mult_error.vo
/usr/bin/coqdep -R src Flocq src/Prop/Div_sqrt_error.v | ./remake -r src/Prop/Div_sqrt_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
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Building src/Prop/Relative.vo
Building src/Prop/Sterbenz.vo
/usr/bin/coqdep -R src Flocq src/Prop/Relative.v | ./remake -r src/Prop/Relative.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
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]
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
Building src/IEEE754/Int63Compat.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Bits.v | ./remake -r src/IEEE754/Bits.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Int63Compat.v | ./remake -r src/IEEE754/Int63Compat.vo
Building src/IEEE754/Int63Copy.vo
Building src/IEEE754/PrimFloat.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Int63Copy.v | ./remake -r src/IEEE754/Int63Copy.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
Finished src/Version.vo
Building src/Pff/Pff2FlocqAux.vo
/usr/bin/coqdep -R src Flocq src/Pff/Pff2FlocqAux.v | ./remake -r src/Pff/Pff2FlocqAux.vo
Building src/Pff/Pff2Flocq.vo
/usr/bin/coqdep -R src Flocq src/Pff/Pff2Flocq.v | ./remake -r src/Pff/Pff2Flocq.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/IEEE754/Int63Copy.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Pff/Pff.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
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]
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]
Finished src/IEEE754/Int63Copy.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/IEEE754/Int63Compat.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
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/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/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/IEEE754/Int63Compat.vo
File "./src/Pff/Pff.v", line 241, characters 21-29:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 241, characters 21-29:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 243, characters 6-17:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 243, characters 6-17:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 456, characters 6-14:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 456, characters 6-14:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 464, characters 21-32:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 464, characters 21-32:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/Zaux.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Raux.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Digits.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff.v", line 632, characters 25-33:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 632, characters 25-33:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 633, characters 18-29:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 633, characters 18-29:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 655, characters 20-28:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 655, characters 20-28:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 673, characters 6-17:
Warning: Notation lt_le_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 673, characters 6-17:
Warning: Notation lt_le_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 714, characters 6-15:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 714, characters 6-15:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 790, characters 6-19:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 790, characters 6-19:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 882, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 882, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 889, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 889, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 900, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 900, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/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/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/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/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 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/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 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2279, characters 8-15:
Warning: Notation lt_0_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2279, characters 8-15:
Warning: Notation lt_0_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2293, characters 28-34:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2293, characters 28-34:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2348, characters 8-14:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2348, characters 8-14:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/Raux.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Defs.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Digits.vo
Finished src/Core/Defs.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Float_prop.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Round_pred.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Float_prop.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Calc/Operations.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Calc/Bracket.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,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 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 -native-compiler yes 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]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,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]
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]
Finished src/Calc/Operations.vo
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 -native-compiler yes src/Prop/Sterbenz.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Calc/Sqrt.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Ulp.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Calc/Div.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,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]
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
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 -native-compiler yes src/Core/Round_NE.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Round_NE.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/FIX.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/FIX.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/FLX.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/FLX.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/FTZ.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/FLT.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/FTZ.vo
Finished src/Core/FLT.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Core/Core.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Core.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Calc/Round.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Prop/Relative.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Prop/Double_rounding.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Prop/Round_odd.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
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/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]
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/Prop/Relative.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Prop/Plus_error.v
Finished src/Calc/Round.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/IEEE754/BinarySingleNaN.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Calc/Plus.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Prop/Round_odd.vo
Finished src/Calc/Plus.vo
Finished src/Prop/Plus_error.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Prop/Mult_error.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Prop/Mult_error.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Prop/Div_sqrt_error.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,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 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Div_sqrt_error.vo
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/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/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Double_rounding.vo
Finished src/IEEE754/BinarySingleNaN.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/IEEE754/PrimFloat.v
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/IEEE754/Binary.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,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]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,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/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/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
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]
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/Binary.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/IEEE754/Bits.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
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]
Finished src/IEEE754/Bits.vo
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]
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 -native-compiler yes src/Pff/Pff2FlocqAux.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Pff/Pff2FlocqAux.vo
/usr/bin/coqc  -q -R src Flocq -native-compiler yes src/Pff/Pff2Flocq.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,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 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;<a href="index.html">Index</a>;Go back to the <a href="../index.html">Main page</a> or <a href="index.html">Index</a>.;' -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.08VqjV
+ umask 022
+ cd /builddir/build/BUILD
+ '[' /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le '!=' / ']'
+ rm -rf /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le
++ dirname /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le
+ mkdir -p /builddir/build/BUILDROOT
+ mkdir /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le
+ CFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection '
+ export CFLAGS
+ CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection '
+ export CXXFLAGS
+ FFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules '
+ export FFLAGS
+ FCFLAGS='-O2 -flto=auto -ffat-lto-objects -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  -m64 -mcpu=power8 -mtune=power8 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ 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  '
+ 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-2.fc38.ppc64le/usr/lib64, Remakefile
+ remake install
Building install
Finished install
+ cp -p src/Version.v /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/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-2.fc38.ppc64le/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-2.fc38.ppc64le/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-2.fc38.ppc64le/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-2.fc38.ppc64le/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-2.fc38.ppc64le/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 -j8
+ /usr/lib/rpm/redhat/brp-python-hardlink
Processing files: flocq-4.1.1-2.fc38.ppc64le
Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.UezsRR
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea
+ DOCDIR=/builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/doc/flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export DOCDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/doc/flocq
+ cp -pr AUTHORS /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/doc/flocq
+ cp -pr NEWS.md /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/doc/flocq
+ cp -pr README.md /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/doc/flocq
+ cp -pr html /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/doc/flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.Kq0wIT
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-flocq-4.1.1-eb9be7d328d3521208834e5a9f326fc56fc2acea
+ LICENSEDIR=/builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/licenses/flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/licenses/flocq
+ cp -pr COPYING /builddir/build/BUILDROOT/flocq-4.1.1-2.fc38.ppc64le/usr/share/licenses/flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: flocq = 4.1.1-2.fc38 flocq(ppc-64) = 4.1.1-2.fc38 ocaml(NFlocq_Calc_Bracket) = 20ba3b1ac2be233da40aa18c0c92292e ocaml(NFlocq_Calc_Div) = 70b57be4560f0ccdf90d3b20b2734baa ocaml(NFlocq_Calc_Operations) = 191fff00bb0875bb5c77b93af01b2ff8 ocaml(NFlocq_Calc_Plus) = 1911781aaedbe5691306c4cd5aa875b3 ocaml(NFlocq_Calc_Round) = 8db6fb73b2835cd18b881201207be9ea ocaml(NFlocq_Calc_Sqrt) = 154f823df5e5ad9bd062ab3b72f4e402 ocaml(NFlocq_Core_Core) = 106a655baa1dbdbaf6cc2f74b12bc828 ocaml(NFlocq_Core_Defs) = 132b24e99d3a5669fbb9feae3bb4ab0e ocaml(NFlocq_Core_Digits) = 9e1310413c913a287784d9e1207c99bb ocaml(NFlocq_Core_FIX) = 623c74745f56657c760f2b3e25ec9b03 ocaml(NFlocq_Core_FLT) = 284f67b699b86802d59614fe94330310 ocaml(NFlocq_Core_FLX) = 2a990cdf5108527c7e8c42ab64e7daac ocaml(NFlocq_Core_FTZ) = 025bb6f80cb61078d5a1f87b7cfde706 ocaml(NFlocq_Core_Float_prop) = f5675f67124519610bafc7fd78d6265f ocaml(NFlocq_Core_Generic_fmt) = a2463e4363999b165b83188ef11e6437 ocaml(NFlocq_Core_Raux) = 10a1868c65be4137786833a740b846ac ocaml(NFlocq_Core_Round_NE) = 77281a77cf83b8c709f0b1924aaa6d2a ocaml(NFlocq_Core_Round_pred) = 4a775618d4a694a66eeb0a4cd72772c4 ocaml(NFlocq_Core_Ulp) = 5a4d967c5a6be13e862c764cb397e9cf ocaml(NFlocq_Core_Zaux) = a0906b16b454ba59d23c1c323e4d6186 ocaml(NFlocq_IEEE754_Binary) = d01e3fdce7e79e0a8eff138b7b083e36 ocaml(NFlocq_IEEE754_BinarySingleNaN) = 0bc45688e525687c976c86dfe298201b ocaml(NFlocq_IEEE754_Bits) = 02f8abafdf5a2cf2f63c8dd9cc1103e1 ocaml(NFlocq_IEEE754_Int63Compat) = 6f8103fc607390b8cb8fa9017242952f ocaml(NFlocq_IEEE754_Int63Copy) = f94367b94aac3b54806fd1bf60e77ac6 ocaml(NFlocq_IEEE754_PrimFloat) = cb81fa86241801bf20bffcdbeef910fb ocaml(NFlocq_Pff_Pff) = 8b5b17d8dd671cfbfcca3aaf1b149bfe ocaml(NFlocq_Pff_Pff2Flocq) = 1c8f9f0ef3727f52aa7272fd23a2e961 ocaml(NFlocq_Pff_Pff2FlocqAux) = c424294a68e1b46ced9952de29e30cd3 ocaml(NFlocq_Prop_Div_sqrt_error) = 880586ab6e9403820fbaad4a9c0192f9 ocaml(NFlocq_Prop_Double_rounding) = 000178d3a1384a193a0a1ce757f05f58 ocaml(NFlocq_Prop_Mult_error) = 9bd5e908d5b5062713a7bf614fdf8ff2 ocaml(NFlocq_Prop_Plus_error) = c833fbc97b29301dbd5c77147d5f34fb ocaml(NFlocq_Prop_Relative) = fbda8ac260e7bdb35642607d4874f979 ocaml(NFlocq_Prop_Round_odd) = 9a109b3770a5f8c56ecea12a1580096a ocaml(NFlocq_Prop_Sterbenz) = 4083f77c8b3bbf23409705232a9ae698 ocaml(NFlocq_Version) = f31d9a7a4c6b92d183d55cb4b02d4f49 ocamlx(NFlocq_Calc_Bracket) = a1e05642f6d8551d01fd744a20616e38 ocamlx(NFlocq_Calc_Div) = 0019948c311a44d71256e54d1e5ad988 ocamlx(NFlocq_Calc_Operations) = e8f093e6fc23d9775f79f979fec80b86 ocamlx(NFlocq_Calc_Plus) = 36139389931e92b9971d2c6edefc1f0c ocamlx(NFlocq_Calc_Round) = 61ebcc36a502a480de43b260eff46080 ocamlx(NFlocq_Calc_Sqrt) = 85d1e70e0cb416941fc8470f0dfcf9b6 ocamlx(NFlocq_Core_Core) = 472f51dca0a91ef3b34bccbebdd2c216 ocamlx(NFlocq_Core_Defs) = 98568f22f0f1a59f027e58e5df9792e9 ocamlx(NFlocq_Core_Digits) = eb8348028e8c89ad24bfd9dd6d8e60e3 ocamlx(NFlocq_Core_FIX) = 1801ee276a87985feead0544e5236627 ocamlx(NFlocq_Core_FLT) = 3d7ae5c0ccaadb2c2f932c19e248fbf8 ocamlx(NFlocq_Core_FLX) = b67a6e06e6da4411eeb418a657baf0e2 ocamlx(NFlocq_Core_FTZ) = 7b68115dde32be4ac6588335066a7fa0 ocamlx(NFlocq_Core_Float_prop) = b82f4ccaea95130cd640cb7e397bf056 ocamlx(NFlocq_Core_Generic_fmt) = 39d8b8dd73998543157621ac341952cd ocamlx(NFlocq_Core_Raux) = 46c2091c7586b4b13d0f9cfb48e66549 ocamlx(NFlocq_Core_Round_NE) = bbd4bce9f54bad24332abc2974f34c5e ocamlx(NFlocq_Core_Round_pred) = 31678e92ec900f3ae38e7f593cef8a5e ocamlx(NFlocq_Core_Ulp) = a00f02dc7c617e5daa51ce6bb3917274 ocamlx(NFlocq_Core_Zaux) = 54b26278f618199cadf17432f3b28b23 ocamlx(NFlocq_IEEE754_Binary) = db08d3b3e384ca03689522ae935909a8 ocamlx(NFlocq_IEEE754_BinarySingleNaN) = f5c47d600e4e75f0af9291695263d513 ocamlx(NFlocq_IEEE754_Bits) = 4b2952479bfe31c6418b19da44c74b70 ocamlx(NFlocq_IEEE754_Int63Compat) = 5223ea67c12603665570ef3d587b9d41 ocamlx(NFlocq_IEEE754_Int63Copy) = 45e67c2dbd07aec6307a23a1db1e9576 ocamlx(NFlocq_IEEE754_PrimFloat) = 18fbd0bc37ecda7911ca76f3ef4910ed ocamlx(NFlocq_Pff_Pff) = 9b689b49762fa2b2239a0a52f216fd7c ocamlx(NFlocq_Pff_Pff2Flocq) = a1a9fd0b70f4f2b4ad5455b9f544c8c3 ocamlx(NFlocq_Pff_Pff2FlocqAux) = 0cc574fccfc4c2f8583e71ab12402dae ocamlx(NFlocq_Prop_Div_sqrt_error) = 1e6750c59b9d6213ea7fcaba82985ca9 ocamlx(NFlocq_Prop_Double_rounding) = e5e382de281d985729515dcce805d176 ocamlx(NFlocq_Prop_Mult_error) = 4d0863cfd6d455ccf9b49b6e229b93d1 ocamlx(NFlocq_Prop_Plus_error) = 19a50d1d47f18e09a0d105f5e8616d85 ocamlx(NFlocq_Prop_Relative) = 23dad7b1348eb7ddf14e6476f0f6644a ocamlx(NFlocq_Prop_Round_odd) = 5cc532f9338fda69c6cd7de14b8e2c13 ocamlx(NFlocq_Prop_Sterbenz) = 0a61d6693f8bd7f009d0c1080d98a363 ocamlx(NFlocq_Version) = 8f2f3001d51467ec2d056fe8b6447992
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Requires: ocaml(AcyclicGraph) = 6db97d4aba38e99b1ce79c13c9dc26ae ocaml(CArray) = 3bf67d1381824155797389de8a32d728 ocaml(CAst) = e6f0ae1977289571e268f9f4798f45af ocaml(CDebug) = a0c286baa9a2b79d6bec187ce25083a3 ocaml(CEphemeron) = 7a5613ac8c99a7839b27f0eb26c409cc ocaml(CList) = 963264b024cbb32e5211e7abb601d1fc ocaml(CMap) = b5f62fbd6f9416f40b63b0dac2bac8a8 ocaml(CPrimitives) = b572f5424b98ffcb8968be2d42112246 ocaml(CSet) = 10548a97a94e3c63dea0f824f53da608 ocaml(CSig) = 93d511bb9f97d6117a9dba3706ab0743 ocaml(CUnix) = 59f179ae315fc18388551aa9972e0dfc ocaml(CamlinternalFormatBasics) = 8f8f634558798ee408df3c50a5539b15 ocaml(CamlinternalLazy) = 5365fec4a58da3e2d8fa2186f77d9be4 ocaml(Constr) = 670799fa78880c542c37d64b3baf38aa ocaml(Context) = 233f361cbf25095b743d2afa636ee001 ocaml(Conv_oracle) = a9dd31ebef4b0f31606274cf6690f783 ocaml(Cooking) = 2c425c1e71f2ea9e68941efc72edf46e ocaml(Declarations) = aaa7cf86083c22fe0bdc650b9766d7f2 ocaml(Environ) = 52e9defc7fd393e51d052bac59d8446f ocaml(Esubst) = a96ceb099c2f1fb6d9584a61b57ee72b ocaml(Evar) = 5410ca5e116902547a19a06b75d92579 ocaml(Exninfo) = 1108fbdf2827b6d2494e3e4bca2b55f0 ocaml(Float64) = 919fb2eabc120f3c4e0129cfc56531e2 ocaml(Genlambda) = 56cbe0a8daebf59b513cd61e5af4c4a0 ocaml(Hashcons) = 04171b8e413a80692dcbea1031ff4542 ocaml(Hashset) = b5af2da2ba0f0aa4ffcd46fea97b6074 ocaml(Int) = 5d7dae0fd8a18e8d5aa73a19ee3bbc40 ocaml(Loc) = de5fd01aaa49ae97f2332d9b30807adc ocaml(Mod_subst) = 883ff24157873ad45c0b936416e276f3 ocaml(NCoq_Arith_Factorial) = 47c7b266b79270b8f0b15b1720ee87aa ocaml(NCoq_Arith_PeanoNat) = 1d70648159fea896330b722effcda00c ocaml(NCoq_Bool_Bool) = d5e3820210fece680272192a53606d50 ocaml(NCoq_Bool_Sumbool) = f3b2aadd3ec4d4a29848475f7316959e ocaml(NCoq_Classes_Morphisms) = 1bdbf76503a06382644347d42d2cddf0 ocaml(NCoq_Classes_Morphisms_Prop) = 8dc18d10a83bafa73f8c06b66e514d49 ocaml(NCoq_Classes_RelationClasses) = d91638f3f38485aaeb3d2e9028952e21 ocaml(NCoq_Floats_FloatAxioms) = 7f13775cfc7b4eadd6f92533a755b3fc ocaml(NCoq_Floats_FloatClass) = dbd845bb26aa9b4a768cdf11ce1788d3 ocaml(NCoq_Floats_FloatOps) = 3e07cc3d1ab4793f6833907565007e25 ocaml(NCoq_Floats_PrimFloat) = 4efe75d4ce70c0839531af6b55a05218 ocaml(NCoq_Floats_SpecFloat) = c3320d5a18ae624200f8243464a12515 ocaml(NCoq_Init_Datatypes) = ba14e8401b72fef301fdb473e3d2bafa ocaml(NCoq_Init_Decimal) = a621a9c215aec9d7e16885a0b523e497 ocaml(NCoq_Init_Hexadecimal) = 89179eec46359242ebf24e32c6fb6f13 ocaml(NCoq_Init_Logic) = 5844583c4d0cb46a11802ac8553e2206 ocaml(NCoq_Init_Nat) = 0e426f499ecc6441a0c78e922372ac9d ocaml(NCoq_Init_Number) = aab1d75d4dbd4729ce71c397398cc45e ocaml(NCoq_Init_Peano) = c08de57feb63472602832118f771ac58 ocaml(NCoq_Init_Specif) = 62e06202f4fd1331cd5f556440e30b6c ocaml(NCoq_Init_Wf) = aabb09f2e37b54489b8a2b02eb8330ba ocaml(NCoq_Lists_List) = 983adfe7b13f4c4334ca68f5997c595c ocaml(NCoq_NArith_BinNat) = 5a233cf05757a167e63428cf2398e8e8 ocaml(NCoq_Numbers_BinNums) = 5d537f42a06df908f38b8169b430149a ocaml(NCoq_Numbers_Cyclic_Abstract_CarryType) = 88cb96a6646a43dc3c42f6cb8ca2715d ocaml(NCoq_Numbers_Cyclic_Int63_PrimInt63) = bbc7b2d5e9bbc38993cf387aef80ce9d ocaml(NCoq_Numbers_Cyclic_Int63_Uint63) = 7c2272ca3504a372170c1d49252f1949 ocaml(NCoq_PArith_BinPos) = e44ceb5a5503da0ba401248b814fd16e ocaml(NCoq_Program_Basics) = 84d6c3405bd68df089341f4153a1804d ocaml(NCoq_QArith_QArith_base) = 4fcf743fb695aeb5b1b6af244c0a814f ocaml(NCoq_QArith_Qabs) = d76f5466f08fe0973b1bc57de3ce0bfa ocaml(NCoq_QArith_Qreduction) = 2a363df47677d2989d0e7db3f0f42f2f ocaml(NCoq_Reals_Alembert) = bd621c0797eefa33a2ba3ac492e59f2c ocaml(NCoq_Reals_Cauchy_ConstructiveCauchyReals) = 05cdd62010014222a803e745ec5e3513 ocaml(NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult) = 7b510e1b8cd5f31ca30caa209ffaf040 ocaml(NCoq_Reals_Cauchy_QExtra) = 33aee1bf52f94ddce9f6c701ed1b50d6 ocaml(NCoq_Reals_RIneq) = 118b37e0d4458879243ea0cf5a6aaa74 ocaml(NCoq_Reals_R_sqrt) = 7c68a8177547bd1f3d2a24dd520b575a ocaml(NCoq_Reals_Raxioms) = 57db10cb6c048406738751134bed8f57 ocaml(NCoq_Reals_Rbasic_fun) = b0ccd7c3ee2e625be2c337b3a7b0139e ocaml(NCoq_Reals_Rdefinitions) = edcffca6cffd1a5625b0332e96f629cd ocaml(NCoq_Reals_Rfunctions) = 56d35e592bc110754aeb2ae506ec1866 ocaml(NCoq_Reals_Rpow_def) = ed5398f03390306ffb4d5a073a7d4bc9 ocaml(NCoq_Reals_Rpower) = 271353e4557931dc792c4eef3727bde6 ocaml(NCoq_Reals_Rsqrt_def) = 550a37f43b8210a23da8d305167a2aaa ocaml(NCoq_Reals_Rtrigo_def) = d5df5cd7858823627e0032404dde6688 ocaml(NCoq_Reals_Rtrigo_fun) = 79007b47d4df2031b6637fdfa61ece9b ocaml(NCoq_Relations_Relation_Definitions) = ac7c54de55154e1e6fa55367d66f6f11 ocaml(NCoq_Structures_OrdersTac) = b4a592883b667daf1534538003f4f02d ocaml(NCoq_ZArith_BinInt) = a6355607a6aec47df884d02e09314e4f ocaml(NCoq_ZArith_BinIntDef) = 87e7ef8712a02a67ec9ae27e1680ee70 ocaml(NCoq_ZArith_ZArith_dec) = 48ed3be92b393f44ef814ef7217b8452 ocaml(NCoq_ZArith_Zbool) = 0780b0ab8a7dd60117d04ce4148ecd41 ocaml(NCoq_ZArith_Zeven) = a030e2000395803d4d23b612d9a79b70 ocaml(NCoq_ZArith_Znat) = 94da1a4df208ddb46df1700004658560 ocaml(NCoq_ZArith_Zorder) = 91a0eda56c8beb7c6644252da846d0f5 ocaml(NCoq_ZArith_Zpower) = 7b9d7348df09e815db99d60e29c11a6f ocaml(NCoq_setoid_ring_Ring_theory) = 4ad8bfe2179da4d9177ac6b283df8bf1 ocaml(NFlocq_Calc_Bracket) = 20ba3b1ac2be233da40aa18c0c92292e ocaml(NFlocq_Calc_Operations) = 191fff00bb0875bb5c77b93af01b2ff8 ocaml(NFlocq_Calc_Round) = 8db6fb73b2835cd18b881201207be9ea ocaml(NFlocq_Core_Defs) = 132b24e99d3a5669fbb9feae3bb4ab0e ocaml(NFlocq_Core_Digits) = 9e1310413c913a287784d9e1207c99bb ocaml(NFlocq_Core_FIX) = 623c74745f56657c760f2b3e25ec9b03 ocaml(NFlocq_Core_FLT) = 284f67b699b86802d59614fe94330310 ocaml(NFlocq_Core_Generic_fmt) = a2463e4363999b165b83188ef11e6437 ocaml(NFlocq_Core_Raux) = 10a1868c65be4137786833a740b846ac ocaml(NFlocq_Core_Ulp) = 5a4d967c5a6be13e862c764cb397e9cf ocaml(NFlocq_Core_Zaux) = a0906b16b454ba59d23c1c323e4d6186 ocaml(NFlocq_IEEE754_Binary) = d01e3fdce7e79e0a8eff138b7b083e36 ocaml(NFlocq_IEEE754_BinarySingleNaN) = 0bc45688e525687c976c86dfe298201b ocaml(NFlocq_Pff_Pff) = 8b5b17d8dd671cfbfcca3aaf1b149bfe ocaml(Names) = 2ea9132743d37e1af5c8327b5dc400b1 ocaml(Nativecode) = 842a27615e40a598a3aabe25b3b65322 ocaml(Nativeconv) = 8d892045979e0114aa149472891fd7cd ocaml(Nativelib) = c14db6be2a471852ffc636e36467ec57 ocaml(Nativevalues) = 50c4bb93028b49d5f9a3462bd4dda4e2 ocaml(Opaqueproof) = 999bfd5f937c49fe3b1b03eafd7a3c8b ocaml(Parray) = 3587b91abccbee918d16a0ecc7071866 ocaml(Pp) = b42c7d685f7cf8e56cb9e5cb72b082aa ocaml(Predicate) = e10f527c1e68b4fcf4187c345bdd22e5 ocaml(Range) = 346d147227354e938de6b932d04d6b3d ocaml(Reduction) = 061463a7ecc6882acd7c10c1c6cf2653 ocaml(Retroknowledge) = 921f47b24ba103d9c6a00670a3a8a6c8 ocaml(Rtree) = 3aeff8b2ebba7f5453fc613375ce0644 ocaml(SList) = 87266e831aa0fb41e7e69d43dba10e03 ocaml(Sorts) = e73c70ce289f5c49f0cf7f5a0ceeefc2 ocaml(Stdlib) = 79b0e9d3b6f7fed07eb3cc2abb961b91 ocaml(Stdlib__Array) = 622d88fad859d0d0f019e691fc4fa865 ocaml(Stdlib__Bigarray) = 994a14f10d5ae081663b52b790ee11d3 ocaml(Stdlib__Buffer) = 4b09c9a6d0622bbf5a3829234b481822 ocaml(Stdlib__Complex) = 4555217c759e89d65daa8f682eb09b35 ocaml(Stdlib__Either) = 26845df28d19584687a38a1ab814c3f9 ocaml(Stdlib__Format) = b6edb97b685819e873481fe05723c8bc ocaml(Stdlib__Int32) = a71ea5238030770647165f659f80b1ab ocaml(Stdlib__Int64) = 0fa5587c47baf16a06837c7dedfc2518 ocaml(Stdlib__Lazy) = 01430d340c028322c7247031a874e355 ocaml(Stdlib__List) = ee222542f6f8195441543b8b399b64b9 ocaml(Stdlib__Map) = 978f82916b5a172c11d2b72719d85680 ocaml(Stdlib__Obj) = 25794d29f7f4018768ea900e331a2bf3 ocaml(Stdlib__Seq) = b63511032211eae4b567ba313cd72962 ocaml(Stdlib__Set) = 871d2ee2167ac9e7977fa13994cf4658 ocaml(Stdlib__Uchar) = c0dde02a556a6d79e363ad365d165d57 ocaml(Term) = 7a45b29ea54c962bdd7f36b12dac3b17 ocaml(TransparentState) = 1dab58426370af71f458b92a6fb5ef06 ocaml(UGraph) = 2fd6f0b34adce97d21c5d93b17310f9b ocaml(Uint63) = 5150bcb618feddc1f891db28ba2fa04b ocaml(Univ) = f7225d1b1091516b25bcad262c410029 ocaml(Unix) = 84bb8ec8ae50f70acba86f5b72088b1c ocaml(Util) = 82442e4e897c61e9ffd5234974e104ef ocaml(Values) = cb3ff5d5b665cb384fb59c1413884523 ocaml(Vmbytecodes) = 0ec5367f45655d3cfc46db2e6443e395 ocaml(Vmemitcodes) = 346ef462a1e0243aad6f2621f358e795 ocaml(Vmvalues) = 1faa9be887b3fe66b213790f9bb1a3d8 ocamlx(CamlinternalLazy) = 0573444d7d158417dbd5f4f46081e73b ocamlx(NFlocq_Calc_Bracket) = a1e05642f6d8551d01fd744a20616e38 ocamlx(NFlocq_Calc_Operations) = e8f093e6fc23d9775f79f979fec80b86 ocamlx(NFlocq_Calc_Round) = 61ebcc36a502a480de43b260eff46080 ocamlx(NFlocq_Core_Defs) = 98568f22f0f1a59f027e58e5df9792e9 ocamlx(NFlocq_Core_Digits) = eb8348028e8c89ad24bfd9dd6d8e60e3 ocamlx(NFlocq_Core_FIX) = 1801ee276a87985feead0544e5236627 ocamlx(NFlocq_Core_FLT) = 3d7ae5c0ccaadb2c2f932c19e248fbf8 ocamlx(NFlocq_Core_Generic_fmt) = 39d8b8dd73998543157621ac341952cd ocamlx(NFlocq_Core_Raux) = 46c2091c7586b4b13d0f9cfb48e66549 ocamlx(NFlocq_Core_Ulp) = a00f02dc7c617e5daa51ce6bb3917274 ocamlx(NFlocq_Core_Zaux) = 54b26278f618199cadf17432f3b28b23 ocamlx(NFlocq_IEEE754_Binary) = db08d3b3e384ca03689522ae935909a8 ocamlx(NFlocq_IEEE754_BinarySingleNaN) = f5c47d600e4e75f0af9291695263d513 ocamlx(NFlocq_Pff_Pff) = 9b689b49762fa2b2239a0a52f216fd7c ocamlx(Nativecode) = 5a7e0e94055b1546ca43d838d54c067d ocamlx(Nativevalues) = dbcd9cbff7a6549a641c25e4afb7c276 rtld(GNU_HASH)
Processing files: flocq-source-4.1.1-2.fc38.ppc64le
Provides: flocq-source = 4.1.1-2.fc38 flocq-source(ppc-64) = 4.1.1-2.fc38
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-2.fc38.ppc64le
Wrote: /builddir/build/RPMS/flocq-source-4.1.1-2.fc38.ppc64le.rpm
Wrote: /builddir/build/RPMS/flocq-4.1.1-2.fc38.ppc64le.rpm
Child return code was: 0