Build:
- 0
2026-10-22 04:25.28: New job: build why3-coq.1.9.0 (c02edabeb8de)
2026-10-22 04:25.28: Waiting for resource in pool day11-builds
2026-10-22 05:39.22: Got resource from pool day11-builds
2026-10-22 05:39.22: [profile full] build why3-coq.1.9.0
2026-10-22 05:39.22: build why3-coq.1.9.0 (c02edabeb8de)
=== DEPENDENCIES (23 transitive) ===
base-threads.base ca51096a9c5b
base-unix.base 88a83b7ed333
compiler-cloning.enabled 1aa529c962c5
conf-gmp.5 d0211a82c71f
conf-linux-libc-dev.0 5ada59924ba9
conf-pkg-config.5 26be2768a637
coq-core.9.3.0 b98cfdf0c063
coq-stdlib.9.2.0 c09205f75c6e
dune.3.24.2 26ca61ae030f
menhir.20260209 d1ea8c88ec3b
menhirCST.20260209 4b4695d97c26
menhirGLR.20260209 aaeea559bc5d
menhirLib.20260209 b3ad34a1cc55
menhirSdk.20260209 0f7f4611a4ff
ocaml.5.5.1 b4ae7c74216a
ocaml-base-compiler.5.5.1 cae593a5c5a1
ocaml-compiler.5.5.1 22179c97969c
ocamlfind.1.9.9~preview 27baeb7469d0
rocq-core.9.3.0 8c8657ed1560
rocq-runtime.9.3.0 8049885af215
rocq-stdlib.9.2.0 86b118564d0b
why3.1.9.0 cf82745b8179
zarith.1.14 bddddc68b0d9
=== STDOUT ===
Processing: [default: loading data]
[why3-coq.1.9.0: extract]
-> retrieved why3-coq.1.9.0 (cached)
[why3-coq: touch configure]
+ /usr/bin/touch "configure" (CWD=/home/opam/.opam/default/.opam-switch/build/why3-coq.1.9.0)
[why3-coq: ./configure]
+ /home/opam/.opam/default/.opam-switch/build/why3-coq.1.9.0/./configure "--prefix" "/home/opam/.opam/default" "--disable-why3-lib" "--disable-frama-c" "--disable-ide" "--disable-js-of-ocaml" "--enable-coq-libs" (CWD=/home/opam/.opam/default/.opam-switch/build/why3-coq.1.9.0)
- checking executable suffix... <none>
- checking for ocamlc... ocamlc
- checking ocaml os type... Unix
- checking for gcc... gcc
- checking whether the C compiler works... yes
- checking for C compiler default output file name... a.out
- checking for suffix of executables...
- checking whether we are cross compiling... no
- checking for suffix of object files... o
- checking whether the compiler supports GNU C... yes
- checking whether gcc accepts -g... yes
- checking for gcc option to enable C11 features... none needed
- checking for a race-free mkdir -p... /usr/bin/mkdir -p
- checking for a BSD-compatible install... /usr/bin/install -c
- configure: ocaml version is 5.5.1
- configure: ocaml library path is /home/opam/.opam/default/lib/ocaml
- checking for ocamlopt... ocamlopt
- checking ocamlopt version... ok
- checking for ocamlc.opt... ocamlc.opt
- checking ocamlc.opt version... ok
- checking for ocamlopt.opt... ocamlopt.opt
- checking ocamlc.opt version... ok
- checking for ocamldep... ocamldep
- checking for ocamldep.opt... ocamldep.opt
- checking for ocamllex... ocamllex
- checking for ocamllex.opt... ocamllex.opt
- checking for ocamlyacc... ocamlyacc
- checking for ocamldoc... ocamldoc
- checking for ocamldoc.opt... ocamldoc.opt
- checking for dune... dune
- checking for menhir... menhir
- checking for ocamlfind... ocamlfind
- checking for Why3 using ocamlfind... yes
- checking for ppxlib using ocamlfind... no
- checking for sphinx-build... no
- configure: WARNING: cannot find sphinx-build, documentation disabled.
- checking for emacs... no
- configure: WARNING: cannot find emacs, compilation of why3.elc disabled.
- checking for zarith using ocamlfind... yes
- checking for /home/opam/.opam/default/lib/zarith/z.cmi... yes
- checking for camlzip using ocamlfind... no
- configure: WARNING: cannot find library camlzip; sessions files will not be compressed.
- checking for menhirLib using ocamlfind... yes
- checking for /home/opam/.opam/default/lib/menhirLib/menhirLib.cmi... yes
- checking for re using ocamlfind... no
- configure: WARNING: cannot find library re, using Str instead.
- checking for ocamlgraph using ocamlfind... no
- configure: WARNING: cannot find library ocamlgraph, hypothesis selection disabled.
- configure: WARNING: cannot find library ocamlgraph, stackify disabled.
- checking for mlmpfr... no
- checking for coqc... coqc
- checking Coq version... 9.3.0
- configure: WARNING: unrecognized Coq version, assuming Rocq 9.1
- checking for coqdep... coqdep
- checking for Flocq... File "./conftest.v", line 1, characters 15-28:
- Error: Cannot find a physical path bound to logical path Flocq.Version.
-
- no
- checking for Coq-interval... File "./conftest.v", line 1, characters 15-30:
- Error: Cannot find a physical path bound to logical path Interval.Tactic.
-
- no
- checking for pvs... no
- checking for isabelle... no
- checking for javac... no
- checking for java... no
- configure: creating ./config.status
- config.status: creating Makefile
- config.status: creating src/config.sh
- config.status: creating src/dune
- config.status: creating src/util/dune
- config.status: creating src/why3deps/dune
- config.status: creating src/jessie/Makefile
- config.status: creating src/jessie/.merlin
- config.status: creating bin/dune
- config.status: creating lib/plugins/dune
- config.status: creating plugins/cfg/dune
- config.status: creating lib/coq/version
- config.status: creating lib/pvs/version
- config.status: creating bench/java/Makefile
- config.status: creating doc/javaexamples/Makefile
- config.status: executing chmod commands
-
- Summary
- -----------------------------------------
- Verbose make : no
- OCaml compiler : yes
- Version : 5.5.1
- Library path : /home/opam/.opam/default/lib/ocaml
- Ocamlfind : yes
- Native compilation : yes
- Memory profiling : no (disabled by default)
- PPX : no (ppxlib not found)
- S-expressions support : no (requires ppx)
- Javascript support : no (disabled by user)
- MPFR support : no (mlmpfr not found)
- Re support : no (re not found)
- Build environment
- OCaml OS Type : Unix
- Build environment type : Posix
- Components
- Why3 library : no
- GTK IDE : no (disabled by user)
- Web IDE : no (Javascript support not available)
- Compressed sessions : no (camlzip not found)
- Hypothesis selection : no (ocamlgraph not found)
- Stackify : no (ocamlgraph not found)
- Invariant inference(exp): no (disabled by default)
- Inference with BDDs(exp): no (disabled by default)
- Frama-C support : no
- Documentation : no (sphinx-build not found)
- Support for interactive proof assistants
- Coq : yes
- Version : 9.3.0
- Library path : /home/opam/.opam/default/lib/coq
- Realization support : yes
- FP arithmetic : no (Flocq >= 3.4 not found)
- Interval arith. : no (Coq-interval not found)
- PVS : no (pvs not found)
- Isabelle : no (isabelle not found)
- Installable : yes
- Binary path : ${exec_prefix}/bin
- Library path : ${exec_prefix}/lib/why3
- Data path : ${prefix}/share/why3
- OCaml library path : /home/opam/.opam/default/lib/why3
- Relocatable : no
[why3-coq: make coq]
+ /usr/bin/make "-j39" "coq" (CWD=/home/opam/.opam/default/.opam-switch/build/why3-coq.1.9.0)
- Coqdep lib/coq/HighOrd.v
- Coqdep lib/coq/BuiltIn.v
- Coqdep lib/coq/WellFounded.v
- Coqdep lib/coq/int/Exponentiation.v
- Coqdep lib/coq/int/Abs.v
- Coqdep lib/coq/int/ComputerDivision.v
- Coqdep lib/coq/int/Div2.v
- Coqdep lib/coq/int/EuclideanDivision.v
- Coqdep lib/coq/int/Int.v
- Coqdep lib/coq/int/MinMax.v
- Coqdep lib/coq/int/Power.v
- Coqdep lib/coq/int/NumOf.v
- Coqdep lib/coq/bool/Bool.v
- Coqdep lib/coq/real/Abs.v
- Coqdep lib/coq/real/ExpLog.v
- Coqdep lib/coq/real/FromInt.v
- Coqdep lib/coq/real/MinMax.v
- Coqdep lib/coq/real/PowerReal.v
- Coqdep lib/coq/real/PowerInt.v
- Coqdep lib/coq/real/Real.v
- Coqdep lib/coq/real/RealInfix.v
- Coqdep lib/coq/real/Square.v
- Coqdep lib/coq/number/Divisibility.v
- Coqdep lib/coq/number/Gcd.v
- Coqdep lib/coq/number/Parity.v
- Coqdep lib/coq/number/Prime.v
- Coqdep lib/coq/number/Coprime.v
- Coqdep lib/coq/set/Set.v
- Coqdep lib/coq/set/Cardinal.v
- Coqdep lib/coq/set/Fset.v
- Coqdep lib/coq/set/FsetInduction.v
- Coqdep lib/coq/set/FsetInt.v
- Coqdep lib/coq/set/FsetSum.v
- Coqdep lib/coq/set/SetApp.v
- Coqdep lib/coq/set/SetAppInt.v
- Coqdep lib/coq/set/SetImp.v
- Coqdep lib/coq/set/SetImpInt.v
- Coqdep lib/coq/map/Map.v
- Coqdep lib/coq/map/Const.v
- Coqdep lib/coq/map/MapExt.v
- Coqdep lib/coq/map/Occ.v
- Coqdep lib/coq/map/MapPermut.v
- Coqdep lib/coq/map/MapInjection.v
- Coqdep lib/coq/list/List.v
- Coqdep lib/coq/list/Length.v
- Coqdep lib/coq/list/Mem.v
- Coqdep lib/coq/list/Nth.v
- Coqdep lib/coq/list/NthLength.v
- Coqdep lib/coq/list/HdTl.v
- Coqdep lib/coq/list/NthHdTl.v
- Coqdep lib/coq/list/Append.v
- Coqdep lib/coq/list/NthLengthAppend.v
- Coqdep lib/coq/list/Reverse.v
- Coqdep lib/coq/list/HdTlNoOpt.v
- Coqdep lib/coq/list/NthNoOpt.v
- Coqdep lib/coq/list/RevAppend.v
- Coqdep lib/coq/list/Combine.v
- Coqdep lib/coq/list/Distinct.v
- Coqdep lib/coq/list/NumOcc.v
- Coqdep lib/coq/list/Permut.v
- Coqdep lib/coq/option/Option.v
- Coqdep lib/coq/bv/BV_Gen.v
- Coqdep lib/coq/for_drivers/ComputerOfEuclideanDivision.v
- Coqdep lib/coq/bv/Pow2int.v
- Coqc lib/coq/BuiltIn.v
- Generate drivers/coq-realizations.aux
- File "./lib/coq/BuiltIn.v", line 11, characters 15-21:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require ZArith" or the deprecated "From Coq Require ZArith"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/BuiltIn.v", line 12, characters 15-20:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Rbase" or the deprecated "From Coq Require Rbase"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/BuiltIn.v", line 13, characters 15-21:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require String" or the deprecated "From Coq Require String"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/BuiltIn.v", line 14, characters 15-31:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require ClassicalEpsilon"
- or the deprecated "From Coq Require ClassicalEpsilon"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/BuiltIn.v", line 21, characters 0-8:
- Warning: Use of "Notation" keyword for abbreviations is deprecated, use
- "Abbreviation" instead.
- [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
- File "./lib/coq/BuiltIn.v", line 22, characters 0-8:
- Warning: Use of "Notation" keyword for abbreviations is deprecated, use
- "Abbreviation" instead.
- [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
- File "./lib/coq/BuiltIn.v", line 31, characters 0-8:
- Warning: Use of "Notation" keyword for abbreviations is deprecated, use
- "Abbreviation" instead.
- [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
- Coqc lib/coq/HighOrd.v
- Coqc lib/coq/WellFounded.v
- Coqc lib/coq/int/Int.v
- Coqc lib/coq/bool/Bool.v
- Coqc lib/coq/real/Real.v
- Coqc lib/coq/list/List.v
- Coqc lib/coq/option/Option.v
- Coqc lib/coq/map/Map.v
- Coqc lib/coq/map/MapExt.v
- Coqc lib/coq/list/Mem.v
- Coqc lib/coq/list/HdTl.v
- Coqc lib/coq/list/HdTlNoOpt.v
- Coqc lib/coq/list/Combine.v
- Coqc lib/coq/int/Exponentiation.v
- Coqc lib/coq/int/Abs.v
- Coqc lib/coq/int/MinMax.v
- Coqc lib/coq/int/NumOf.v
- Coqc lib/coq/list/Length.v
- Coqc lib/coq/list/Nth.v
- Coqc lib/coq/bv/Pow2int.v
- Coqc lib/coq/list/NthNoOpt.v
- File "./lib/coq/int/NumOf.v", line 18, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/map/Map.v", line 17, characters 15-31:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require ClassicalEpsilon"
- or the deprecated "From Coq Require ClassicalEpsilon"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/Real.v", line 207, characters 12-27:
- Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/real/Real.v", line 207, characters 12-27:
- Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/real/Real.v", line 207, characters 12-27:
- Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/real/Real.v", line 207, characters 12-27:
- Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/real/Real.v", line 207, characters 12-27:
- Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
- [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/map/Const.v
- Coqc lib/coq/map/Occ.v
- File "./lib/coq/map/MapExt.v", line 17, characters 15-31:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require ClassicalEpsilon"
- or the deprecated "From Coq Require ClassicalEpsilon"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/map/MapExt.v", line 22, characters 0-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- Coqc lib/coq/real/Abs.v
- Coqc lib/coq/real/ExpLog.v
- Coqc lib/coq/real/FromInt.v
- Coqc lib/coq/real/MinMax.v
- Coqc lib/coq/real/RealInfix.v
- Coqc lib/coq/real/Square.v
- File "./lib/coq/list/HdTlNoOpt.v", line 19, characters 0-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/HdTlNoOpt.v", line 35, characters 0-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/int/Exponentiation.v", line 43, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/Nth.v", line 22, characters 0-116:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/Nth.v", line 22, characters 64-72:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Nth.v", line 22, characters 64-72:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthNoOpt.v", line 21, characters 0-121:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/NthNoOpt.v", line 21, characters 74-82:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthNoOpt.v", line 21, characters 74-82:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Nth.v", line 44, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/Nth.v", line 44, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/Nth.v", line 45, characters 9-17:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Nth.v", line 45, characters 9-17:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthNoOpt.v", line 39, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthNoOpt.v", line 39, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthNoOpt.v", line 40, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthNoOpt.v", line 40, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 19, characters 2-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 24, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/MinMax.v", line 17, characters 15-25:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Rbasic_fun"
- or the deprecated "From Coq Require Rbasic_fun"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 31, characters 2-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 36, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/MinMax.v", line 55, characters 0-17:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/MinMax.v", line 62, characters 0-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/MinMax.v", line 69, characters 0-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/MinMax.v", line 76, characters 0-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 44, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/int/Abs.v", line 17, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 52, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 53, characters 17-23:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Zorder" or the deprecated "From Coq Require Zorder"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 53, characters 17-23:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Zorder" or the deprecated "From Coq Require Zorder"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/int/MinMax.v", line 17, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 60, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 65, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 70, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 75, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 80, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- Coqc lib/coq/list/NthHdTl.v
- File "./lib/coq/bv/Pow2int.v", line 85, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 90, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 95, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 100, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 105, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 110, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 115, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 14, characters 8-24:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rtrigo_def"
- or the deprecated "From Coq Require Reals.Rtrigo_def"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 120, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 125, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 130, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 15, characters 8-20:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rpower"
- or the deprecated "From Coq Require Reals.Rpower"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/int/EuclideanDivision.v
- Coqc lib/coq/int/ComputerDivision.v
- File "./lib/coq/bv/Pow2int.v", line 135, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 140, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 145, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/Length.v", line 18, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/ExpLog.v", line 27, characters 0-12:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 150, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 30, characters 15-23:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Exp_prop"
- or the deprecated "From Coq Require Exp_prop"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/ExpLog.v", line 37, characters 0-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 40, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lra" or the deprecated "From Coq Require Lra"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 155, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 160, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 165, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 170, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 57, characters 15-27:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rpower"
- or the deprecated "From Coq Require Reals.Rpower"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 175, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 180, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 185, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 190, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 195, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 200, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 205, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- Coqc lib/coq/int/Power.v
- Coqc lib/coq/real/PowerInt.v
- Coqc lib/coq/list/NthLength.v
- Coqc lib/coq/list/Append.v
- File "./lib/coq/bv/Pow2int.v", line 210, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 215, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 220, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 225, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 230, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 235, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 240, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 245, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 250, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 255, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 260, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 265, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 270, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 275, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/map/Occ.v", line 19, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/Pow2int.v", line 280, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 285, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 290, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 295, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 300, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 305, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 310, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 315, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 320, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 325, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 330, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 335, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 340, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 345, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 351, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 356, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 361, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 366, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 371, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 376, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/Pow2int.v", line 381, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 98, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 107, characters 0-19:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 130, characters 0-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/ExpLog.v", line 137, characters 0-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Square.v", line 14, characters 8-20:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.R_sqrt"
- or the deprecated "From Coq Require Reals.R_sqrt"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/Abs.v", line 14, characters 8-24:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rbasic_fun"
- or the deprecated "From Coq Require Reals.Rbasic_fun"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/set/Set.v
- File "./lib/coq/real/Abs.v", line 41, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Abs.v", line 67, characters 0-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Abs.v", line 75, characters 0-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Abs.v", line 83, characters 0-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Abs.v", line 92, characters 0-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Square.v", line 35, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Square.v", line 43, characters 0-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Square.v", line 50, characters 0-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Square.v", line 59, characters 0-42:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/real/Square.v", line 67, characters 0-44:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/NthLength.v", line 21, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 33, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 33, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 34, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 34, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 55, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 55, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 56, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 56, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 81, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 81, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 82, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 82, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/map/Occ.v", line 56, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Zwf" or the deprecated "From Coq Require Zwf"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/int/ComputerDivision.v", line 18, characters 15-20:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Zquot" or the deprecated "From Coq Require Zquot"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/int/ComputerDivision.v", line 18, characters 21-24:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/int/EuclideanDivision.v", line 18, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/list/NthHdTl.v", line 21, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/list/NthHdTl.v", line 33, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthHdTl.v", line 33, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthHdTl.v", line 34, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthHdTl.v", line 34, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Append.v", line 33, characters 15-25:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lists.List"
- or the deprecated "From Coq Require Lists.List"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/list/Append.v", line 63, characters 12-22:
- Warning: Notation app_length is deprecated since 8.20.
- Use length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Append.v", line 63, characters 12-22:
- Warning: Notation app_length is deprecated since 8.20.
- Use length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Append.v", line 63, characters 12-22:
- Warning: Notation app_length is deprecated since 8.20.
- Use length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/list/NthLengthAppend.v
- Coqc lib/coq/list/Reverse.v
- Coqc lib/coq/list/Distinct.v
- File "./lib/coq/int/Power.v", line 17, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/PowerInt.v", line 14, characters 8-24:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rfunctions"
- or the deprecated "From Coq Require Reals.Rfunctions"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/int/Power.v", line 21, characters 0-8:
- Warning: Use of "Notation" keyword for abbreviations is deprecated, use
- "Abbreviation" instead.
- [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
- File "./lib/coq/real/PowerInt.v", line 20, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/number/Parity.v
- File "./lib/coq/set/Set.v", line 20, characters 15-31:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require ClassicalEpsilon"
- or the deprecated "From Coq Require ClassicalEpsilon"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/set/Set.v", line 25, characters 0-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/set/Set.v", line 44, characters 0-16:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
- Coqc lib/coq/real/PowerReal.v
- File "./lib/coq/list/NthLengthAppend.v", line 24, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 39, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 39, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 40, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 40, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/map/MapPermut.v
- Coqc lib/coq/map/MapInjection.v
- File "./lib/coq/list/NthLengthAppend.v", line 66, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 66, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since Stdlib 9.0.
- Use Z.eqb_eq instead.
- [deprecated-reference-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 67, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 67, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since Stdlib 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/int/Div2.v
- Coqc lib/coq/bv/BV_Gen.v
- Coqc lib/coq/for_drivers/ComputerOfEuclideanDivision.v
- File "./lib/coq/list/Reverse.v", line 52, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/Reverse.v", line 63, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/Reverse.v", line 79, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- Coqc lib/coq/set/Cardinal.v
- File "./lib/coq/list/Reverse.v", line 98, characters 12-27:
- Warning: Notation List.rev_length is deprecated since 8.20.
- Use List.length_rev instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Reverse.v", line 98, characters 12-27:
- Warning: Notation List.rev_length is deprecated since 8.20.
- Use List.length_rev instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/list/Reverse.v", line 98, characters 12-27:
- Warning: Notation List.rev_length is deprecated since 8.20.
- Use List.length_rev instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/list/NumOcc.v
- Coqc lib/coq/list/RevAppend.v
- File "./lib/coq/real/PowerReal.v", line 14, characters 8-24:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rtrigo_def"
- or the deprecated "From Coq Require Reals.Rtrigo_def"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/PowerReal.v", line 15, characters 8-20:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rpower"
- or the deprecated "From Coq Require Reals.Rpower"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/PowerReal.v", line 16, characters 8-20:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.R_sqrt"
- or the deprecated "From Coq Require Reals.R_sqrt"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/number/Divisibility.v
- File "./lib/coq/bv/BV_Gen.v", line 24, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 35, characters 2-28:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 39, characters 2-24:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 45, characters 2-26:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/int/Div2.v", line 17, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 48, characters 5-8:
- Warning: "From Coq" has been replaced by "From Stdlib".
- [deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 48, characters 0-32:
- Warning: Library File Stdlib.Vectors.Bvector is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-library-file-since-8.20,deprecated-since-8.20,deprecated-library-file,deprecated,default]
- File "./lib/coq/for_drivers/ComputerOfEuclideanDivision.v", line 20, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 52, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 52, characters 9-16:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 52, characters 9-16:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 65, characters 2-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/map/MapInjection.v", line 33, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/map/MapInjection.v", line 33, characters 19-28:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Peano_dec"
- or the deprecated "From Coq Require Peano_dec"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 73, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 78, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 86, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 93, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 97, characters 2-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 105, characters 2-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 118, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 129, characters 2-38:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 140, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 152, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 162, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 171, characters 2-58:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 175, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 184, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/set/Cardinal.v", line 22, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 197, characters 2-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 202, characters 0-12:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 223, characters 0-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 229, characters 2-31:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 243, characters 2-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 247, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 256, characters 0-30:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 260, characters 2-57:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 264, characters 2-30:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 269, characters 2-28:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 276, characters 2-32:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 281, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 310, characters 2-42:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 317, characters 2-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 323, characters 2-42:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 330, characters 2-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 336, characters 2-44:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 343, characters 2-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 349, characters 2-39:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 356, characters 2-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 362, characters 2-59:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 362, characters 20-33:
- Warning: Reference BshiftRl_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 362, characters 20-33:
- Warning: Reference BshiftRl_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 368, characters 12-25:
- Warning: Reference BshiftRl_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 369, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 373, characters 8-21:
- Warning: Reference BshiftRl_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 374, characters 9-17:
- Warning: Reference BshiftRl is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 374, characters 19-24:
- Warning: Reference Bhigh is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 386, characters 0-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 396, characters 2-24:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 408, characters 0-5:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 413, characters 2-59:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 413, characters 20-33:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 413, characters 20-33:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 420, characters 2-24:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 435, characters 2-32:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 447, characters 2-57:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 453, characters 2-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 460, characters 2-29:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 471, characters 12-25:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 472, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 476, characters 8-21:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 477, characters 9-17:
- Warning: Reference BshiftRa is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 477, characters 19-24:
- Warning: Reference Bhigh is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NumOcc.v", line 22, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/list/NumOcc.v", line 27, characters 0-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 492, characters 2-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 500, characters 43-50:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 500, characters 74-87:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 501, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 503, characters 16-24:
- Warning: Reference BshiftRa is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 503, characters 26-31:
- Warning: Reference Bhigh is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 510, characters 43-56:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 512, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 513, characters 8-21:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 518, characters 8-21:
- Warning: Reference BshiftRa_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 519, characters 9-17:
- Warning: Reference BshiftRa is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 519, characters 19-24:
- Warning: Reference Bhigh is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 539, characters 2-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 548, characters 0-5:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 553, characters 2-58:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 553, characters 20-32:
- Warning: Reference BshiftL_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 553, characters 20-32:
- Warning: Reference BshiftL_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 39, characters 15-25:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Znumtheory"
- or the deprecated "From Coq Require Znumtheory"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 556, characters 134-146:
- Warning: Reference BshiftL_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 40, characters 0-8:
- Warning: Use of "Notation" keyword for abbreviations is deprecated, use
- "Abbreviation" instead.
- [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 557, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Divisibility.v", line 51, characters 6-17:
- Warning: Notation Zone_divide is deprecated since Stdlib 9.1.
- Use Z.divide_1_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 51, characters 6-17:
- Warning: Notation Zone_divide is deprecated since Stdlib 9.1.
- Use Z.divide_1_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 57, characters 6-15:
- Warning: Notation Zdivide_0 is deprecated since Stdlib 9.1.
- Use Z.divide_0_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 57, characters 6-15:
- Warning: Notation Zdivide_0 is deprecated since Stdlib 9.1.
- Use Z.divide_0_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 65, characters 6-27:
- Warning: Notation Zmult_divide_compat_l is deprecated since Stdlib 9.1.
- Use Z.mul_divide_mono_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 65, characters 6-27:
- Warning: Notation Zmult_divide_compat_l is deprecated since Stdlib 9.1.
- Use Z.mul_divide_mono_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 73, characters 6-27:
- Warning: Notation Zmult_divide_compat_r is deprecated since Stdlib 9.1.
- Use Z.mul_divide_mono_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 73, characters 6-27:
- Warning: Notation Zmult_divide_compat_r is deprecated since Stdlib 9.1.
- Use Z.mul_divide_mono_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 81, characters 6-19:
- Warning: Reference Zdivide_opp_r is deprecated since Stdlib 9.1.
- Use Z.divide_opp_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 81, characters 6-19:
- Warning: Reference Zdivide_opp_r is deprecated since Stdlib 9.1.
- Use Z.divide_opp_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 89, characters 6-19:
- Warning: Reference Zdivide_opp_l is deprecated since Stdlib 9.1.
- Use Z.divide_opp_l instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 577, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Divisibility.v", line 89, characters 6-19:
- Warning: Reference Zdivide_opp_l is deprecated since Stdlib 9.1.
- Use Z.divide_opp_l instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 97, characters 6-23:
- Warning: Reference Zdivide_opp_l_rev is deprecated since Stdlib 9.1.
- Use Z.divide_opp_l instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 97, characters 6-23:
- Warning: Reference Zdivide_opp_l_rev is deprecated since Stdlib 9.1.
- Use Z.divide_opp_l instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 105, characters 6-23:
- Warning: Reference Zdivide_opp_r_rev is deprecated since Stdlib 9.1.
- Use Z.divide_opp_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 105, characters 6-23:
- Warning: Reference Zdivide_opp_r_rev is deprecated since Stdlib 9.1.
- Use Z.divide_opp_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 113, characters 6-20:
- Warning: Notation Zdivide_plus_r is deprecated since Stdlib 9.1.
- Use Z.divide_add_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 113, characters 6-20:
- Warning: Notation Zdivide_plus_r is deprecated since Stdlib 9.1.
- Use Z.divide_add_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 121, characters 6-21:
- Warning: Notation Zdivide_minus_l is deprecated since Stdlib 9.1.
- Use Z.divide_sub_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 121, characters 6-21:
- Warning: Notation Zdivide_minus_l is deprecated since Stdlib 9.1.
- Use Z.divide_sub_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 130, characters 6-20:
- Warning: Notation Zdivide_mult_r is deprecated since Stdlib 9.1.
- Use Z.divide_mul_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 130, characters 6-20:
- Warning: Notation Zdivide_mult_r is deprecated since Stdlib 9.1.
- Use Z.divide_mul_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 138, characters 6-20:
- Warning: Notation Zdivide_mult_l is deprecated since Stdlib 9.1.
- Use Z.divide_mul_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 138, characters 6-20:
- Warning: Notation Zdivide_mult_l is deprecated since Stdlib 9.1.
- Use Z.divide_mul_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 145, characters 6-22:
- Warning: Notation Zdivide_factor_l is deprecated since Stdlib 9.1.
- Use Z.divide_factor_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 145, characters 6-22:
- Warning: Notation Zdivide_factor_l is deprecated since Stdlib 9.1.
- Use Z.divide_factor_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 590, characters 62-74:
- Warning: Reference BshiftL_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 591, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Divisibility.v", line 152, characters 6-22:
- Warning: Notation Zdivide_factor_r is deprecated since Stdlib 9.1.
- Use Z.divide_factor_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 152, characters 6-22:
- Warning: Notation Zdivide_factor_r is deprecated since Stdlib 9.1.
- Use Z.divide_factor_l instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 159, characters 6-15:
- Warning: Notation Zdivide_1 is deprecated since Stdlib 9.1.
- Use Z.divide_1_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 159, characters 6-15:
- Warning: Notation Zdivide_1 is deprecated since Stdlib 9.1.
- Use Z.divide_1_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 183, characters 6-20:
- Warning: Notation Zdivide_bounds is deprecated since Stdlib 9.1.
- Use Z.absle_divide instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 183, characters 6-20:
- Warning: Notation Zdivide_bounds is deprecated since Stdlib 9.1.
- Use Z.absle_divide instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 607, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 614, characters 0-5:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 618, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 625, characters 28-35:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 633, characters 2-33:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 636, characters 34-41:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 637, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 639, characters 13-18:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 639, characters 13-18:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 647, characters 58-65:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 648, characters 27-34:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 649, characters 11-15:
- Warning: Reference Bnil is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 651, characters 6-11:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 655, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 658, characters 9-14:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 662, characters 54-61:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 664, characters 2-17:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 664, characters 9-16:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 207, characters 10-21:
- Warning: Reference Zdivide_mod is deprecated since Stdlib 9.1.
- Use Z.mod0_divide instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 207, characters 10-21:
- Warning: Reference Zdivide_mod is deprecated since Stdlib 9.1.
- Use Z.mod0_divide instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 679, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 692, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 698, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 704, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 711, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 722, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 726, characters 2-53:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 730, characters 2-78:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 734, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 740, characters 2-20:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 746, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/NumOcc.v", line 107, characters 0-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 760, characters 42-47:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 761, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 774, characters 42-47:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 775, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 781, characters 58-65:
- Warning: Reference Bvector is deprecated since 8.20.
- Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 784, characters 2-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 790, characters 12-17:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 790, characters 24-29:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 790, characters 12-17:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 790, characters 24-29:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 791, characters 44-49:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 792, characters 15-20:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 805, characters 15-20:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 822, characters 13-18:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 833, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- Coqc lib/coq/list/Permut.v
- File "./lib/coq/bv/BV_Gen.v", line 843, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 849, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 854, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 863, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 871, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 877, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 886, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 891, characters 22-27:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 929, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 957, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 965, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 972, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 978, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 983, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 990, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 997, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1022, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1044, characters 2-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1055, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- Coqc lib/coq/number/Prime.v
- Coqc lib/coq/number/Gcd.v
- File "./lib/coq/bv/BV_Gen.v", line 1066, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1090, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1108, characters 2-29:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1125, characters 2-14:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1131, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1157, characters 2-53:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1166, characters 2-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1182, characters 2-52:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1191, characters 2-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1207, characters 2-30:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1218, characters 2-34:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1223, characters 2-10:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1235, characters 2-10:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1240, characters 2-53:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1240, characters 21-26:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1240, characters 21-26:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1245, characters 2-53:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1249, characters 2-40:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1256, characters 2-53:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1261, characters 2-35:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1274, characters 12-17:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1274, characters 12-17:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1276, characters 15-20:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1283, characters 12-17:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1283, characters 12-17:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1285, characters 15-20:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1293, characters 2-17:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1302, characters 2-39:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1310, characters 2-26:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1320, characters 2-31:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1325, characters 2-26:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1330, characters 2-33:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1337, characters 2-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1352, characters 2-48:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1360, characters 2-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1368, characters 8-21:
- Warning: Reference BshiftRl_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1369, characters 9-17:
- Warning: Reference BshiftRl is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1369, characters 19-24:
- Warning: Reference Bhigh is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1386, characters 2-44:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1391, characters 2-87:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1396, characters 2-31:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1400, characters 2-23:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1416, characters 9-16:
- Warning: Reference BshiftL is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1416, characters 18-23:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1417, characters 8-20:
- Warning: Reference BshiftL_iter is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1442, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1469, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1474, characters 2-23:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1480, characters 0-24:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1485, characters 2-23:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1490, characters 2-10:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1497, characters 2-10:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1507, characters 2-23:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1511, characters 2-25:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1516, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1524, characters 2-22:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1685, characters 9-14:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1733, characters 9-14:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1740, characters 2-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1743, characters 24-29:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1744, characters 2-23:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1753, characters 37-42:
- Warning: Reference Bsign is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1772, characters 2-76:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1781, characters 2-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1791, characters 2-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/list/Permut.v", line 23, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1818, characters 2-76:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1827, characters 2-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1835, characters 2-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1863, characters 2-62:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1871, characters 2-11:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Gcd.v", line 25, characters 0-8:
- Warning: Use of "Notation" keyword for abbreviations is deprecated, use
- "Abbreviation" instead.
- [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 31, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 31, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 40, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 40, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 49, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 49, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 59, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 59, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1902, characters 2-76:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Gcd.v", line 73, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 73, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1911, characters 2-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Gcd.v", line 83, characters 6-14:
- Warning: Reference Zgcd_ass is deprecated since Stdlib 9.1.
- Use Z.gcd_assoc instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 83, characters 6-14:
- Warning: Reference Zgcd_ass is deprecated since Stdlib 9.1.
- Use Z.gcd_assoc instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1920, characters 2-18:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Gcd.v", line 99, characters 6-12:
- Warning: Notation Zgcd_0 is deprecated since Stdlib 9.1.
- Use Z.gcd_0_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 99, characters 6-12:
- Warning: Notation Zgcd_0 is deprecated since Stdlib 9.1.
- Use Z.gcd_0_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1930, characters 2-60:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Gcd.v", line 108, characters 6-12:
- Warning: Notation Zgcd_0 is deprecated since Stdlib 9.1.
- Use Z.gcd_0_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 108, characters 6-12:
- Warning: Notation Zgcd_0 is deprecated since Stdlib 9.1.
- Use Z.gcd_0_r instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 118, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 118, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 119, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 119, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 122, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 122, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1945, characters 13-21:
- Warning: Reference Zdiv_0_r is deprecated since Stdlib 9.1.
- Use Z.div_0_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1945, characters 13-21:
- Warning: Reference Zdiv_0_r is deprecated since Stdlib 9.1.
- Use Z.div_0_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1945, characters 13-21:
- Warning: Reference Zdiv_0_r is deprecated since Stdlib 9.1.
- Use Z.div_0_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 131, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 131, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 132, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 132, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 134, characters 6-24:
- Warning: Notation Zis_gcd_for_euclid is deprecated since 8.17.
- [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 134, characters 6-24:
- Warning: Notation Zis_gcd_for_euclid is deprecated since 8.17.
- [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 135, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 135, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1947, characters 13-21:
- Warning: Reference Zmod_0_r is deprecated since Stdlib 9.1.
- Use Z.mod_0_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1947, characters 13-21:
- Warning: Reference Zmod_0_r is deprecated since Stdlib 9.1.
- Use Z.mod_0_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1947, characters 13-21:
- Warning: Reference Zmod_0_r is deprecated since Stdlib 9.1.
- Use Z.mod_0_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 1960, characters 2-61:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1968, characters 2-15:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1983, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 1987, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2064, characters 2-39:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2070, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2078, characters 2-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Prime.v", line 22, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/number/Prime.v", line 22, characters 19-29:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Znumtheory"
- or the deprecated "From Coq Require Znumtheory"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2084, characters 2-39:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2090, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2095, characters 2-39:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2101, characters 2-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Prime.v", line 35, characters 14-20:
- Warning: Notation prime' is deprecated since Stdlib 9.1. Use Z.prime instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2110, characters 2-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2116, characters 2-48:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2121, characters 2-47:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2127, characters 0-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2133, characters 0-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2138, characters 2-39:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2143, characters 2-20:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2152, characters 2-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Prime.v", line 50, characters 6-13:
- Warning: Reference prime_2 is deprecated since Stdlib 9.1.
- Use Z.prime_2 instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Prime.v", line 50, characters 6-13:
- Warning: Reference prime_2 is deprecated since Stdlib 9.1.
- Use Z.prime_2 instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Prime.v", line 57, characters 6-13:
- Warning: Reference prime_3 is deprecated since Stdlib 9.1.
- Use Z.prime_3 instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Prime.v", line 57, characters 6-13:
- Warning: Reference prime_3 is deprecated since Stdlib 9.1.
- Use Z.prime_3 instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Prime.v", line 68, characters 10-24:
- Warning: Reference prime_divisors is deprecated since Stdlib 9.1.
- Use Z.divide_prime_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Prime.v", line 68, characters 10-24:
- Warning: Reference prime_divisors is deprecated since Stdlib 9.1.
- Use Z.divide_prime_r instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 170, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 170, characters 6-17:
- Warning: Reference Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 172, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 172, characters 6-17:
- Warning: Notation Zgcd_is_pos is deprecated since Stdlib 9.1.
- Use Z.gcd_nonneg instead.
- [deprecated-syntactic-definition-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 173, characters 6-18:
- Warning: Reference Zis_gcd_mult is deprecated since Stdlib 9.1.
- Use Z.gcd_mul_mono_l instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 173, characters 6-18:
- Warning: Reference Zis_gcd_mult is deprecated since Stdlib 9.1.
- Use Z.gcd_mul_mono_l instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 174, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Gcd.v", line 174, characters 6-17:
- Warning: Reference Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2171, characters 2-24:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2204, characters 2-10:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2212, characters 2-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2220, characters 2-152:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2230, characters 2-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2245, characters 2-38:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2282, characters 2-8:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2377, characters 2-27:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2423, characters 4-10:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2424, characters 12-17:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2424, characters 12-17:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2432, characters 12-17:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2432, characters 12-17:
- Warning: Reference Bcons is deprecated since 8.20.
- Consider [list bool] instead. See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
- [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2441, characters 2-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/bv/BV_Gen.v", line 2580, characters 2-13:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/set/Cardinal.v", line 616, characters 26-41:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 616, characters 26-41:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 616, characters 26-41:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 617, characters 23-38:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 617, characters 23-38:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 617, characters 23-38:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/number/Coprime.v
- File "./lib/coq/set/Cardinal.v", line 635, characters 26-41:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 635, characters 26-41:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 635, characters 26-41:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 635, characters 65-80:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 635, characters 65-80:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 635, characters 65-80:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/map/MapInjection.v", line 156, characters 15-21:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require ZArith" or the deprecated "From Coq Require ZArith"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 30, characters 0-7:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Coprime.v", line 34, characters 20-42:
- Warning: Reference Znumtheory.Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 34, characters 20-42:
- Warning: Reference Znumtheory.Zgcd_is_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 35, characters 6-28:
- Warning: Reference Znumtheory.Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 35, characters 6-28:
- Warning: Reference Znumtheory.Zis_gcd_gcd is deprecated since Stdlib 9.1.
- Use Z.gcd instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 44, characters 0-9:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Coprime.v", line 71, characters 0-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Coprime.v", line 72, characters 6-22:
- Warning: Reference Znumtheory.Gauss is deprecated since Stdlib 9.1.
- Use Z.gauss instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 72, characters 6-22:
- Warning: Reference Znumtheory.Gauss is deprecated since Stdlib 9.1.
- Use Z.gauss instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 81, characters 0-21:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/number/Coprime.v", line 82, characters 6-27:
- Warning: Reference Znumtheory.prime_mult is deprecated since Stdlib 9.1.
- Use Z.divide_prime_mul instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 82, characters 6-27:
- Warning: Reference Znumtheory.prime_mult is deprecated since Stdlib 9.1.
- Use Z.divide_prime_mul instead.
- [deprecated-reference-since-Stdlib-9.1,deprecated-since-Stdlib-9.1,deprecated-reference,deprecated,default]
- File "./lib/coq/number/Coprime.v", line 90, characters 0-16:
- Warning: This interactive proof is not started by the "Proof" command.
- [missing-proof-command,fragile,default]
- File "./lib/coq/set/Cardinal.v", line 752, characters 8-23:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 752, characters 8-23:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 752, characters 8-23:
- Warning: Notation List.app_length is deprecated since 8.20.
- Use List.length_app instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 833, characters 12-27:
- Warning: Notation List.map_length is deprecated since 8.20.
- Use List.length_map instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 833, characters 12-27:
- Warning: Notation List.map_length is deprecated since 8.20.
- Use List.length_map instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 833, characters 12-27:
- Warning: Notation List.map_length is deprecated since 8.20.
- Use List.length_map instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 858, characters 24-40:
- Warning: Notation List.prod_length is deprecated since 8.20.
- Use List.length_prod instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 858, characters 24-40:
- Warning: Notation List.prod_length is deprecated since 8.20.
- Use List.length_prod instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 858, characters 24-40:
- Warning: Notation List.prod_length is deprecated since 8.20.
- Use List.length_prod instead.
- [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/set/Fset.v
- File "./lib/coq/set/Fset.v", line 18, characters 15-31:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require ClassicalEpsilon"
- or the deprecated "From Coq Require ClassicalEpsilon"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/set/Fset.v", line 18, characters 32-35:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/set/Fset.v", line 19, characters 8-30:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Logic.ProofIrrelevance"
- or the deprecated "From Coq Require Logic.ProofIrrelevance"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/set/FsetInt.v
- Coqc lib/coq/set/FsetInduction.v
- Coqc lib/coq/set/FsetSum.v
- Coqc lib/coq/set/SetApp.v
- Coqc lib/coq/set/SetImp.v
- File "./lib/coq/set/FsetInt.v", line 19, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 19, characters 15-18:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Lia" or the deprecated "From Coq Require Lia"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/set/SetAppInt.v
- Coqc lib/coq/set/SetImpInt.v
-> compiled why3-coq.1.9.0
[why3-coq: make install-coq]
+ /usr/bin/make "install-coq" (CWD=/home/opam/.opam/default/.opam-switch/build/why3-coq.1.9.0)
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq
- /usr/bin/install -c -m 644 lib/coq/version /home/opam/.opam/default/lib/why3/coq/
- /usr/bin/install -c -m 644 lib/coq/BuiltIn.vo lib/coq/HighOrd.vo lib/coq/WellFounded.vo /home/opam/.opam/default/lib/why3/coq/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/int
- /usr/bin/install -c -m 644 lib/coq/int/Exponentiation.vo lib/coq/int/Abs.vo lib/coq/int/ComputerDivision.vo lib/coq/int/Div2.vo lib/coq/int/EuclideanDivision.vo lib/coq/int/Int.vo lib/coq/int/MinMax.vo lib/coq/int/Power.vo lib/coq/int/NumOf.vo /home/opam/.opam/default/lib/why3/coq/int/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/bool
- /usr/bin/install -c -m 644 lib/coq/bool/Bool.vo /home/opam/.opam/default/lib/why3/coq/bool/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/real
- /usr/bin/install -c -m 644 lib/coq/real/Abs.vo lib/coq/real/ExpLog.vo lib/coq/real/FromInt.vo lib/coq/real/MinMax.vo lib/coq/real/PowerInt.vo lib/coq/real/PowerReal.vo lib/coq/real/Real.vo lib/coq/real/RealInfix.vo lib/coq/real/Square.vo /home/opam/.opam/default/lib/why3/coq/real/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/number
- /usr/bin/install -c -m 644 lib/coq/number/Divisibility.vo lib/coq/number/Gcd.vo lib/coq/number/Parity.vo lib/coq/number/Prime.vo lib/coq/number/Coprime.vo /home/opam/.opam/default/lib/why3/coq/number/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/set
- /usr/bin/install -c -m 644 lib/coq/set/Set.vo lib/coq/set/Cardinal.vo lib/coq/set/Fset.vo lib/coq/set/FsetInduction.vo lib/coq/set/FsetInt.vo lib/coq/set/FsetSum.vo lib/coq/set/SetApp.vo lib/coq/set/SetAppInt.vo lib/coq/set/SetImp.vo lib/coq/set/SetImpInt.vo /home/opam/.opam/default/lib/why3/coq/set/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/map
- /usr/bin/install -c -m 644 lib/coq/map/Map.vo lib/coq/map/Const.vo lib/coq/map/MapExt.vo lib/coq/map/Occ.vo lib/coq/map/MapPermut.vo lib/coq/map/MapInjection.vo /home/opam/.opam/default/lib/why3/coq/map/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/list
- /usr/bin/install -c -m 644 lib/coq/list/List.vo lib/coq/list/Length.vo lib/coq/list/Mem.vo lib/coq/list/Nth.vo lib/coq/list/NthLength.vo lib/coq/list/HdTl.vo lib/coq/list/NthHdTl.vo lib/coq/list/Append.vo lib/coq/list/NthLengthAppend.vo lib/coq/list/Reverse.vo lib/coq/list/HdTlNoOpt.vo lib/coq/list/NthNoOpt.vo lib/coq/list/RevAppend.vo lib/coq/list/Combine.vo lib/coq/list/Distinct.vo lib/coq/list/NumOcc.vo lib/coq/list/Permut.vo /home/opam/.opam/default/lib/why3/coq/list/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/option
- /usr/bin/install -c -m 644 lib/coq/option/Option.vo /home/opam/.opam/default/lib/why3/coq/option/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/bv
- /usr/bin/install -c -m 644 lib/coq/bv/Pow2int.vo lib/coq/bv/BV_Gen.vo /home/opam/.opam/default/lib/why3/coq/bv/
- /usr/bin/mkdir -p /home/opam/.opam/default/lib/why3/coq/for_drivers
- /usr/bin/install -c -m 644 lib/coq/for_drivers/ComputerOfEuclideanDivision.vo /home/opam/.opam/default/lib/why3/coq/for_drivers/
- /usr/bin/mkdir -p /home/opam/.opam/default/share/why3/drivers
- /usr/bin/install -c -m 644 drivers/coq-realizations.aux /home/opam/.opam/default/share/why3/drivers/
-> installed why3-coq.1.9.0
[WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config
=== STDERR ===
2026-10-22 05:43.15: OK: build why3-coq.1.9.0 (runc: 119.9s, disk: 161KB)
2026-10-22 05:43.15: Job succeeded