Mock Version: 2.6
Mock Version: 2.6
Mock Version: 2.6
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target x86_64 --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f33-build-side-34777-24329027-2517688/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 0x7fbdf2872a30>timeout=201600uid=1000gid=425user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False)
Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target x86_64 --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'} and shell False
Building target platforms: x86_64
Building for target x86_64
setting SOURCE_DATE_EPOCH=1606867200
Wrote: /builddir/build/SRPMS/flocq-3.3.1-8.fc33.src.rpm
Child return code was: 0
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target x86_64 --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f33-build-side-34777-24329027-2517688/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 0x7fbdf2872a30>timeout=201600uid=1000gid=425user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False)
Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target x86_64 --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'} and shell False
Building target platforms: x86_64
Building for target x86_64
setting SOURCE_DATE_EPOCH=1606867200
Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.QxwlXw
+ umask 022
+ cd /builddir/build/BUILD
+ cd /builddir/build/BUILD
+ rm -rf flocq-3.3.1
+ /usr/bin/gzip -dc /builddir/build/SOURCES/flocq-3.3.1.tar.gz
+ /usr/bin/tar -xof -
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd flocq-3.3.1
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.dDA7Qv
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-3.3.1
+ ./configure
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking for coqc... /usr/bin/coqc
checking Coq version... 8.12.1
checking for coqdep... /usr/bin/coqdep
checking for coqdoc... /usr/bin/coqdoc
configure: building remake...
/usr/bin/ld: /tmp/ccO96wQJ.o: in function `main':
remake.cpp:(.text.startup+0xaf5): 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/SpecFloatCompat.v
+ rm -f remake
+ ln -s /usr/bin/remake remake
+ remake -d -j6 all doc
Building src/Version.vo
Building src/Core/Raux.vo
Building src/Core/Zaux.vo
Building src/Core/Defs.vo
Building src/Core/Digits.vo
Building src/Core/Float_prop.vo
/usr/bin/coqdep -R src Flocq src/Core/Raux.v | ./remake -r src/Core/Raux.vo
/usr/bin/coqdep -R src Flocq src/Version.v | ./remake -r src/Version.vo
/usr/bin/coqdep -R src Flocq src/Core/Defs.v | ./remake -r src/Core/Defs.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/Digits.v | ./remake -r src/Core/Digits.vo
/usr/bin/coqdep -R src Flocq src/Core/Float_prop.v | ./remake -r src/Core/Float_prop.vo
Building src/Core/FIX.vo
Building src/IEEE754/SpecFloatCompat.vo
/usr/bin/coqdep -R src Flocq src/Core/FIX.v | ./remake -r src/Core/FIX.vo
Building src/Core/FLT.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/SpecFloatCompat.v | ./remake -r src/IEEE754/SpecFloatCompat.vo
/usr/bin/coqdep -R src Flocq src/Core/FLT.v | ./remake -r src/Core/FLT.vo
/usr/bin/coqc  -R src Flocq src/Version.v
Building src/Core/FLX.vo
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
/usr/bin/coqdep -R src Flocq src/Core/Generic_fmt.v | ./remake -r src/Core/Generic_fmt.vo
/usr/bin/coqc  -R src Flocq src/IEEE754/SpecFloatCompat.v
Building src/Core/Round_NE.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
Building src/Core/Ulp.vo
Building src/Core/Core.vo
/usr/bin/coqdep -R src Flocq src/Core/Ulp.v | ./remake -r src/Core/Ulp.vo
/usr/bin/coqdep -R src Flocq src/Core/Round_pred.v | ./remake -r src/Core/Round_pred.vo
/usr/bin/coqdep -R src Flocq src/Core/Core.v | ./remake -r src/Core/Core.vo
Building src/Calc/Bracket.vo
/usr/bin/coqdep -R src Flocq src/Calc/Bracket.v | ./remake -r src/Calc/Bracket.vo
Building src/Calc/Div.vo
/usr/bin/coqdep -R src Flocq src/Calc/Div.v | ./remake -r src/Calc/Div.vo
Building src/Calc/Operations.vo
Building src/Calc/Round.vo
Building src/Calc/Sqrt.vo
/usr/bin/coqdep -R src Flocq src/Calc/Operations.v | ./remake -r src/Calc/Operations.vo
/usr/bin/coqdep -R src Flocq src/Calc/Round.v | ./remake -r src/Calc/Round.vo
/usr/bin/coqdep -R src Flocq src/Calc/Sqrt.v | ./remake -r src/Calc/Sqrt.vo
Building src/Prop/Div_sqrt_error.vo
/usr/bin/coqdep -R src Flocq src/Prop/Div_sqrt_error.v | ./remake -r src/Prop/Div_sqrt_error.vo
Building src/Prop/Mult_error.vo
/usr/bin/coqdep -R src Flocq src/Prop/Mult_error.v | ./remake -r src/Prop/Mult_error.vo
Building src/Prop/Relative.vo
/usr/bin/coqdep -R src Flocq src/Prop/Relative.v | ./remake -r src/Prop/Relative.vo
Building src/Prop/Sterbenz.vo
/usr/bin/coqdep -R src Flocq src/Prop/Sterbenz.v | ./remake -r src/Prop/Sterbenz.vo
Building src/Prop/Plus_error.vo
/usr/bin/coqdep -R src Flocq src/Prop/Plus_error.v | ./remake -r src/Prop/Plus_error.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/PrimFloat.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/PrimFloat.v | ./remake -r src/IEEE754/PrimFloat.vo
Building src/IEEE754/BinarySingleNaN.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/BinarySingleNaN.v | ./remake -r src/IEEE754/BinarySingleNaN.vo
Building src/IEEE754/Binary.vo
Building src/IEEE754/Bits.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Binary.v | ./remake -r src/IEEE754/Binary.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Bits.v | ./remake -r src/IEEE754/Bits.vo
Building src/Pff/Pff.vo
/usr/bin/coqdep -R src Flocq src/Pff/Pff.v | ./remake -r src/Pff/Pff.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  -R src Flocq src/Pff/Pff.v
Finished src/Version.vo
Finished src/IEEE754/SpecFloatCompat.vo
/usr/bin/coqc  -R src Flocq src/Core/Zaux.v
File "./src/Core/Zaux.v", line 269, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Zaux.v", line 289, characters 0-17:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Zaux.v", line 309, characters 16-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Zaux.v", line 427, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Zaux.v", line 444, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/Zaux.vo
/usr/bin/coqc  -R src Flocq src/Core/Digits.v
/usr/bin/coqc  -R src Flocq src/Core/Raux.v
File "./src/Core/Digits.v", line 49, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 51, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 193, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 199, characters 0-28:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 199, characters 0-28:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 211, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 235, characters 0-28:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 235, characters 0-28:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 457, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 500, characters 0-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 511, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 540, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 597, characters 0-13:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 598, characters 0-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 602, characters 0-13:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 606, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 632, characters 0-28:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 634, characters 0-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 639, characters 0-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 654, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 674, characters 0-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 693, characters 0-40:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 693, characters 0-40:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 697, characters 0-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 701, characters 0-40:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 721, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 796, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 936, characters 0-13:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 946, characters 42-48:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 959, characters 0-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 969, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 990, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff.v", line 1090, characters 0-30:
Warning:
New coercion path [Z.of_nat; IZR] : nat >-> R is ambiguous with existing 
[INR] : nat >-> R. [ambiguous-paths,typechecker]
File "./src/Core/Digits.v", line 1018, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 1019, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 1039, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 1049, characters 61-67:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 1060, characters 29-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 1061, characters 29-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Digits.v", line 1081, characters 2-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/Digits.vo
File "./src/Core/Raux.v", line 1320, characters 11-17:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 1322, characters 14-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 1469, characters 0-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff.v", line 1295, characters 0-16:
Warning:
New coercion path [Z.of_nat; IZR] : nat >-> R is ambiguous with existing 
[INR] : nat >-> R. [ambiguous-paths,typechecker]
File "./src/Core/Raux.v", line 1771, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 1915, characters 0-13:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 2014, characters 0-61:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 2111, characters 2-34:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 2119, characters 2-34:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 2339, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Raux.v", line 2384, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/Raux.vo
/usr/bin/coqc  -R src Flocq src/Core/Defs.v
Finished src/Core/Defs.vo
/usr/bin/coqc  -R src Flocq src/Core/Float_prop.v
/usr/bin/coqc  -R src Flocq src/Core/Round_pred.v
File "./src/Core/Float_prop.v", line 363, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Float_prop.v", line 382, characters 20-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Float_prop.v", line 416, characters 24-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Float_prop.v", line 475, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Float_prop.v", line 478, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/Float_prop.vo
/usr/bin/coqc  -R src Flocq src/Calc/Bracket.v
/usr/bin/coqc  -R src Flocq src/Calc/Operations.v
Finished src/Core/Round_pred.vo
/usr/bin/coqc  -R src Flocq src/Core/Generic_fmt.v
File "./src/Calc/Operations.v", line 53, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Calc/Operations.vo
File "./src/Core/Generic_fmt.v", line 55, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 239, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 252, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 261, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 273, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 282, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 70, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 337, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 350, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 428, characters 0-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 371, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 393, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 439, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 442, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 525, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 547, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 558, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 496, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 505, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 590, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 633, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 660, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 618, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 741, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Bracket.v", line 671, characters 34-48:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Calc/Bracket.vo
File "./src/Core/Generic_fmt.v", line 1383, characters 16-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 1392, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 1529, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 1805, characters 0-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 1940, characters 2-43:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 2139, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 2142, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 2383, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Generic_fmt.v", line 2386, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/Generic_fmt.vo
/usr/bin/coqc  -R src Flocq src/Calc/Div.v
/usr/bin/coqc  -R src Flocq src/Prop/Sterbenz.v
/usr/bin/coqc  -R src Flocq src/Calc/Sqrt.v
/usr/bin/coqc  -R src Flocq src/Core/Ulp.v
File "./src/Calc/Div.v", line 83, characters 4-42:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 89, characters 2-40:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Div.v", line 91, characters 6-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 109, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Div.v", line 92, characters 4-42:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 120, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 127, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 136, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 142, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 60, characters 0-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 157, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 69, characters 0-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 159, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 78, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 164, characters 0-18:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 79, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Div.v", line 116, characters 2-70:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Sqrt.v", line 191, characters 2-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Div.v", line 153, characters 2-41:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Prop/Sterbenz.vo
File "./src/Calc/Div.v", line 156, characters 2-41:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 251, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Calc/Div.vo
Finished src/Calc/Sqrt.vo
File "./src/Core/Ulp.v", line 256, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 261, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 313, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 316, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 472, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 555, characters 11-17:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 577, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 601, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 614, characters 0-46:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 636, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 864, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 929, characters 0-44:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 952, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 975, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 979, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 980, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1103, characters 0-48:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1168, characters 0-48:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1352, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1354, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1356, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1398, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1400, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1545, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Ulp.v", line 1922, characters 0-48:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/Ulp.vo
/usr/bin/coqc  -R src Flocq src/Core/Round_NE.v
File "./src/Core/Round_NE.v", line 151, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Round_NE.v", line 212, characters 42-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Round_NE.v", line 219, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Round_NE.v", line 416, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Round_NE.v", line 418, characters 0-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Round_NE.v", line 425, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Round_NE.v", line 427, characters 20-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/Round_NE.v", line 437, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/Round_NE.vo
/usr/bin/coqc  -R src Flocq src/Core/FIX.v
File "./src/Core/FIX.v", line 89, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/FIX.vo
/usr/bin/coqc  -R src Flocq src/Core/FLX.v
File "./src/Core/FLX.v", line 51, characters 0-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLX.v", line 215, characters 0-54:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLX.v", line 224, characters 2-66:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLX.v", line 225, characters 2-75:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLX.v", line 230, characters 0-59:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLX.v", line 359, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/FLX.vo
/usr/bin/coqc  -R src Flocq src/Core/FTZ.v
/usr/bin/coqc  -R src Flocq src/Core/FLT.v
File "./src/Core/FTZ.v", line 51, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 55, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 48, characters 0-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 58, characters 0-58:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 61, characters 0-40:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 64, characters 0-44:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 66, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 97, characters 0-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 138, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 96, characters 26-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 108, characters 0-38:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 143, characters 30-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 189, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 154, characters 0-13:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 199, characters 0-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 201, characters 0-45:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 204, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 171, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 174, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 293, characters 0-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 298, characters 0-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FTZ.v", line 334, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 227, characters 30-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 257, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/FTZ.vo
File "./src/Core/FLT.v", line 339, characters 0-38:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 339, characters 0-38:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Core/FLT.v", line 377, characters 0-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Core/FLT.vo
/usr/bin/coqc  -R src Flocq src/Core/Core.v
/usr/bin/coqc  -R src Flocq src/Prop/Double_rounding.v
Finished src/Core/Core.vo
/usr/bin/coqc  -R src Flocq src/Calc/Round.v
/usr/bin/coqc  -R src Flocq src/Prop/Relative.v
/usr/bin/coqc  -R src Flocq src/Prop/Round_odd.v
File "./src/Prop/Double_rounding.v", line 125, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 206, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 91, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 71, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 150, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 221, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 233, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 286, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 317, characters 2-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 320, characters 2-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 378, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 390, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 383, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 428, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 507, characters 0-69:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 588, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 677, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 720, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 727, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 747, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 793, characters 6-12:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 806, characters 26-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 506, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 662, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 528, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 539, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 846, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 872, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Relative.v", line 879, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 1159, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Calc/Round.v", line 1168, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 463, characters 2-46:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 467, characters 2-49:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 716, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Calc/Round.vo
File "./src/Prop/Double_rounding.v", line 485, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 490, characters 2-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 500, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 769, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 502, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 800, characters 0-9:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 815, characters 0-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 816, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 832, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 841, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Prop/Relative.vo
/usr/bin/coqc  -R src Flocq src/IEEE754/Binary.v
/usr/bin/coqc  -R src Flocq src/IEEE754/BinarySingleNaN.v
/usr/bin/coqc  -R src Flocq src/Prop/Plus_error.v
File "./src/Prop/Round_odd.v", line 860, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 869, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Round_odd.v", line 955, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 591, characters 2-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 594, characters 2-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 609, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Prop/Round_odd.vo
File "./src/Prop/Double_rounding.v", line 693, characters 0-72:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 718, characters 0-254:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 53, characters 23-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 58, characters 20-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 65, characters 20-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 330, characters 0-9:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 354, characters 0-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 749, characters 0-273:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 409, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 413, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 427, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 433, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 523, characters 0-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 523, characters 0-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 571, characters 0-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Plus_error.v", line 571, characters 0-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Prop/Plus_error.vo
/usr/bin/coqc  -R src Flocq src/Prop/Mult_error.v
File "./src/Prop/Double_rounding.v", line 773, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 801, characters 0-60:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 804, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 834, characters 4-46:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 887, characters 6-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 907, characters 2-66:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 930, characters 4-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 931, characters 4-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 935, characters 4-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 938, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 940, characters 6-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 943, characters 6-12:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 986, characters 8-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1006, characters 4-42:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1017, characters 4-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1036, characters 0-108:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1039, characters 0-79:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1047, characters 2-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1048, characters 0-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1056, characters 2-45:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 74, characters 27-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 92, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1091, characters 6-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1094, characters 6-26:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1118, characters 4-60:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1143, characters 4-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1154, characters 6-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1201, characters 2-94:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1207, characters 6-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1211, characters 6-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1216, characters 6-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1227, characters 6-12:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 166, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 212, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 215, characters 0-62:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1264, characters 4-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1265, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 245, characters 0-9:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1291, characters 2-107:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 265, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1314, characters 8-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1337, characters 6-12:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1338, characters 2-110:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1347, characters 4-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1350, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1385, characters 0-79:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1395, characters 2-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1404, characters 2-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1405, characters 2-57:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1407, characters 4-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1409, characters 4-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1415, characters 4-98:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1431, characters 6-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 299, characters 0-46:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1438, characters 2-96:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 330, characters 0-72:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 331, characters 0-69:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1504, characters 10-72:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1509, characters 6-62:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1535, characters 4-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1546, characters 6-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Mult_error.v", line 353, characters 0-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1628, characters 0-80:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1628, characters 0-80:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1628, characters 0-80:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1628, characters 0-80:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1631, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 604, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1686, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1690, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Prop/Mult_error.vo
/usr/bin/coqc  -R src Flocq src/Prop/Div_sqrt_error.v
File "./src/IEEE754/BinarySingleNaN.v", line 631, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1694, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 700, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 691, characters 23-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1698, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 728, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 788, characters 23-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 798, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 814, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1753, characters 2-140:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1757, characters 2-140:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 949, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1761, characters 2-136:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1765, characters 2-94:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1151, characters 0-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1156, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1159, characters 44-58:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1162, characters 55-69:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1173, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1835, characters 4-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1836, characters 4-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1840, characters 4-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1843, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 103, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1845, characters 6-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1848, characters 6-12:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1865, characters 0-108:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1868, characters 0-79:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1875, characters 0-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1883, characters 2-45:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1331, characters 0-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1336, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1339, characters 44-58:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1342, characters 55-69:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1353, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1917, characters 2-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1943, characters 4-56:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1969, characters 4-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 1980, characters 6-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1430, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2011, characters 2-94:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2017, characters 6-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2021, characters 6-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2026, characters 6-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2037, characters 6-12:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 196, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2074, characters 4-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2075, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2099, characters 0-79:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2116, characters 2-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2117, characters 2-57:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2119, characters 4-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2121, characters 4-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2138, characters 4-28:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 1363, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2167, characters 6-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 1468, characters 7-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 283, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 287, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2207, characters 10-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 1487, characters 7-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2212, characters 6-58:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2239, characters 4-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2250, characters 6-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 322, characters 0-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2334, characters 0-91:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2334, characters 0-91:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2334, characters 0-91:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2334, characters 0-91:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2337, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 349, characters 4-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2396, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2400, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1539, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2404, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2408, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1640, characters 7-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 1659, characters 7-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 386, characters 4-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2467, characters 2-140:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2471, characters 2-140:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2475, characters 2-136:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2479, characters 2-94:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2549, characters 2-57:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2553, characters 2-67:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 450, characters 2-24:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 456, characters 4-53:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2590, characters 0-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2641, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2657, characters 4-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 498, characters 6-73:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2701, characters 4-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2734, characters 10-74:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2017, characters 2-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2055, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2747, characters 4-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2751, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 659, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2790, characters 10-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2795, characters 8-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 718, characters 0-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2838, characters 6-59:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2850, characters 8-56:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2855, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2860, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2861, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2881, characters 0-62:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2922, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2925, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2929, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Prop/Div_sqrt_error.vo
File "./src/Prop/Double_rounding.v", line 2970, characters 2-96:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2973, characters 2-100:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2978, characters 4-100:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 2983, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 2210, characters 2-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3060, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 2247, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 2271, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3076, characters 4-52:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Binary.v", line 2290, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3120, characters 4-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3165, characters 4-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3169, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3206, characters 10-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3211, characters 8-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3266, characters 6-59:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3278, characters 8-56:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3283, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3288, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3289, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3310, characters 0-73:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3353, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3356, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3360, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3403, characters 2-96:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3406, characters 2-100:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3411, characters 4-100:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3416, characters 4-10:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3482, characters 2-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3491, characters 2-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3495, characters 2-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3528, characters 4-48:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3533, characters 6-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3560, characters 0-71:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3568, characters 4-99:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3583, characters 4-93:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3593, characters 4-70:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3600, characters 6-75:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3605, characters 6-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3632, characters 0-79:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3636, characters 0-74:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3683, characters 2-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3686, characters 2-56:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3691, characters 2-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3695, characters 6-66:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/IEEE754/Binary.vo
/usr/bin/coqc  -R src Flocq src/IEEE754/Bits.v
File "./src/Prop/Double_rounding.v", line 3706, characters 10-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3710, characters 10-87:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/IEEE754/BinarySingleNaN.vo
/usr/bin/coqc  -R src Flocq src/IEEE754/PrimFloat.v
File "./src/Prop/Double_rounding.v", line 3727, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3831, characters 8-83:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 46, characters 2-34:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 49, characters 2-34:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 57, characters 2-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 59, characters 2-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 68, characters 2-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 69, characters 2-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 70, characters 2-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 88, characters 2-34:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3845, characters 4-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 91, characters 2-34:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 3853, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 102, characters 4-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 111, characters 4-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 112, characters 4-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 116, characters 2-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 178, characters 31-45:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 246, characters 0-150:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 246, characters 0-150:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 246, characters 0-150:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 248, characters 7-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 248, characters 7-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 248, characters 7-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 248, characters 7-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 256, characters 18-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 266, characters 0-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 272, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 273, characters 28-42:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 285, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 290, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 308, characters 2-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 316, characters 2-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 324, characters 6-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 328, characters 6-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 328, characters 6-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 330, characters 6-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 332, characters 6-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 334, characters 6-44:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 336, characters 6-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 336, characters 6-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 339, characters 6-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 373, characters 2-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 392, characters 0-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/IEEE754/PrimFloat.vo
File "./src/IEEE754/Bits.v", line 400, characters 18-39:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 402, characters 0-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 409, characters 0-60:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 413, characters 28-34:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 455, characters 0-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 474, characters 0-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4002, characters 8-83:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 479, characters 0-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 506, characters 18-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 512, characters 18-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 525, characters 0-14:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 530, characters 0-19:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 537, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 550, characters 0-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4019, characters 4-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4029, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 591, characters 8-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 596, characters 0-21:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/IEEE754/Bits.v", line 604, characters 0-28:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4065, characters 6-123:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/IEEE754/Bits.vo
File "./src/Prop/Double_rounding.v", line 4141, characters 8-83:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4215, characters 6-123:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4228, characters 4-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4236, characters 4-33:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4382, characters 0-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4383, characters 0-47:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4428, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4433, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4438, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4443, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4448, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4494, characters 2-94:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4497, characters 2-188:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4502, characters 2-196:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4507, characters 2-188:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Prop/Double_rounding.v", line 4512, characters 2-188:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Prop/Double_rounding.vo
Finished src/Pff/Pff.vo
/usr/bin/coqc  -R src Flocq src/Pff/Pff2FlocqAux.v
File "./src/Pff/Pff2FlocqAux.v", line 23, characters 0-24:
Warning:
New coercion path [BinInt.Z.of_nat; Rdefinitions.IZR] : nat >-> Rdefinitions.RbaseSymbolsImpl.R is ambiguous with existing 
[Raxioms.INR] : nat >-> Rdefinitions.RbaseSymbolsImpl.R.
[ambiguous-paths,typechecker]
File "./src/Pff/Pff2FlocqAux.v", line 174, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 177, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 198, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 206, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 251, characters 0-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 251, characters 0-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 264, characters 23-29:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 333, characters 0-44:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 363, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 368, characters 0-37:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 378, characters 0-42:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 400, characters 0-6:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 516, characters 0-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 545, characters 0-50:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 590, characters 0-30:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 620, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 636, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 718, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 751, characters 0-23:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 763, characters 0-27:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 777, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 792, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./src/Pff/Pff2FlocqAux.v", line 798, characters 0-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Finished src/Pff/Pff2FlocqAux.vo
/usr/bin/coqc  -R src Flocq src/Pff/Pff2Flocq.v
File "./src/Pff/Pff2Flocq.v", line 23, characters 0-32:
Warning:
New coercion path [Z.of_nat; IZR] : nat >-> R is ambiguous with existing 
[INR] : nat >-> R. [ambiguous-paths,typechecker]
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 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/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/PrimFloat.v src/IEEE754/SpecFloatCompat.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Binary.v src/IEEE754/Bits.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.2R3MSv
+ umask 022
+ cd /builddir/build/BUILD
+ '[' /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64 '!=' / ']'
+ rm -rf /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64
++ dirname /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64
+ mkdir -p /builddir/build/BUILDROOT
+ mkdir /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64
+ cd flocq-3.3.1
+ sed -i s,/usr/lib64,/builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/lib64, Remakefile
+ remake install
Building install
Finished install
+ cp -p src/Version.v /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/lib64/ocaml/coq/user-contrib/Flocq
+ cp -p src/Calc/Bracket.v src/Calc/Div.v src/Calc/Operations.v src/Calc/Round.v src/Calc/Sqrt.v /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/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-3.3.1-8.fc33.x86_64/usr/lib64/ocaml/coq/user-contrib/Flocq/Core
+ cp -p src/IEEE754/Binary.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Bits.v src/IEEE754/PrimFloat.v src/IEEE754/SpecFloatCompat.v src/IEEE754/SpecFloatCopy.v /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/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-3.3.1-8.fc33.x86_64/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-3.3.1-8.fc33.x86_64/usr/lib64/ocaml/coq/user-contrib/Flocq/Prop
+ cp -p opam /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/lib64/ocaml/coq/user-contrib/Flocq
+ /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/redhat/brp-python-bytecompile '' 1 0
+ /usr/lib/rpm/brp-python-hardlink
+ /usr/lib/rpm/redhat/brp-mangle-shebangs
Processing files: flocq-3.3.1-8.fc33.x86_64
Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.tTCEBv
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-3.3.1
+ DOCDIR=/builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/doc/flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export DOCDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/doc/flocq
+ cp -pr AUTHORS /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/doc/flocq
+ cp -pr NEWS.md /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/doc/flocq
+ cp -pr README.md /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/doc/flocq
+ cp -pr html /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/doc/flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.SvT7jv
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-3.3.1
+ LICENSEDIR=/builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/licenses/flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/licenses/flocq
+ cp -pr COPYING /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64/usr/share/licenses/flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: flocq = 3.3.1-8.fc33 flocq(x86-64) = 3.3.1-8.fc33
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Processing files: flocq-source-3.3.1-8.fc33.x86_64
Provides: flocq-source = 3.3.1-8.fc33 flocq-source(x86-64) = 3.3.1-8.fc33
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-3.3.1-8.fc33.x86_64
Wrote: /builddir/build/RPMS/flocq-source-3.3.1-8.fc33.x86_64.rpm
Wrote: /builddir/build/RPMS/flocq-3.3.1-8.fc33.x86_64.rpm
Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.vKmKiw
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-3.3.1
+ /usr/bin/rm -rf /builddir/build/BUILDROOT/flocq-3.3.1-8.fc33.x86_64
+ RPM_EC=0
++ jobs -p
+ exit 0
Child return code was: 0