Build:
- 0
2026-06-24 16:18.49: New job: build why3-coq.1.8.2 (3d2acf391193)
2026-06-24 16:18.49: Waiting for resource in pool day11-builds
2026-06-24 17:13.18: Got resource from pool day11-builds
2026-06-24 17:13.18: [profile full] build why3-coq.1.8.2
2026-06-24 17:13.19: build why3-coq.1.8.2 (3d2acf391193)
=== DEPENDENCIES (23 transitive) ===
base-threads.base c9e7bdbf5823
base-unix.base 7d1428be9ddb
compiler-cloning.enabled 439a1fc77aa6
conf-gmp.5 be11edf77089
conf-linux-libc-dev.0 2d4ad9bc3a8f
conf-pkg-config.5 d5de2c6a88f9
coq-core.9.1.1 0083f048c36f
coq-stdlib.9.0.0 b59824c83d71
dune.3.23.1 a59dd9b14fe3
menhir.20260209 2dfcdff6beb1
menhirCST.20260209 ca14cdeaa1bc
menhirGLR.20260209 5ba1fed6b7bb
menhirLib.20260209 93342fcbef2d
menhirSdk.20260209 28fda6618c58
ocaml.5.5.0 383268832c4b
ocaml-base-compiler.5.5.0 522c248944c8
ocaml-compiler.5.5.0 eb1a8babf54c
ocamlfind.1.9.8 b506a15fcd6c
rocq-core.9.1.1 4ab0dd1574f1
rocq-runtime.9.1.1 5c8d6a381281
rocq-stdlib.9.0.0 40eee100e6a7
why3.1.8.2 06195545bc9e
zarith.1.14 c48bd7ff5430
=== STDOUT ===
Processing: [default: loading data]
[why3-coq.1.8.2: extract]
-> retrieved why3-coq.1.8.2 (cached)
[why3-coq: touch configure]
+ /usr/bin/touch "configure" (CWD=/home/opam/.opam/default/.opam-switch/build/why3-coq.1.8.2)
[why3-coq: ./configure]
+ /home/opam/.opam/default/.opam-switch/build/why3-coq.1.8.2/./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.8.2)
- 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.0
- 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 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.1.1
- configure: WARNING: unrecognized Coq version, assuming Coq 8.20
- 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 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 lib/why3/META
- config.status: creating .merlin
- config.status: creating src/jessie/Makefile
- config.status: creating src/jessie/.merlin
- 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.0
- 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.1.1
- Library path : /home/opam/.opam/default/lib/coq
- Realization support : yes
- FP arithmetic : no (Flocq >= 3.4 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.8.2)
- cp src/util/json_base.ml src/trywhy3/json_base.ml
- Menhir src/util/json_parser.mly
- cp src/util/json_base.mli src/trywhy3/json_base.mli
- Ocamllex src/util/json_lexer.mll
- cp src/util/json_lexer.mli src/trywhy3/json_lexer.mli
- Ocamllex src/why3doc/doc_lexer.mll
- Ocamldep src/tools/why3pp.ml
- Ocamldep src/isabelle-client/isabelle_client_main.ml
- Coqdep lib/coq/for_drivers/ComputerOfEuclideanDivision.v
- Coqdep lib/coq/bv/BV_Gen.v
- Coqdep lib/coq/bv/Pow2int.v
- 52 states, 495 transitions, table size 2292 bytes
- Coqdep lib/coq/option/Option.v
- Coqdep lib/coq/list/Permut.v
- Coqdep lib/coq/list/NumOcc.v
- Coqdep lib/coq/list/Distinct.v
- 120 states, 706 transitions, table size 3544 bytes
- 1763 additional bytes used for bindings
- Coqdep lib/coq/list/Combine.v
- Coqdep lib/coq/list/RevAppend.v
- Coqdep lib/coq/list/NthNoOpt.v
- Coqdep lib/coq/list/HdTlNoOpt.v
- Coqdep lib/coq/list/Reverse.v
- Coqdep lib/coq/list/NthLengthAppend.v
- Coqdep lib/coq/list/Append.v
- Coqdep lib/coq/list/NthHdTl.v
- Coqdep lib/coq/list/HdTl.v
- Coqdep lib/coq/list/NthLength.v
- Coqdep lib/coq/list/Nth.v
- Coqdep lib/coq/list/Mem.v
- Coqdep lib/coq/list/Length.v
- Coqdep lib/coq/list/List.v
- Coqdep lib/coq/map/MapInjection.v
- Coqdep lib/coq/map/MapPermut.v
- Coqdep lib/coq/map/Occ.v
- Coqdep lib/coq/map/MapExt.v
- Coqdep lib/coq/map/Const.v
- Coqdep lib/coq/map/Map.v
- Coqdep lib/coq/set/SetImpInt.v
- Coqdep lib/coq/set/SetImp.v
- Coqdep lib/coq/set/SetAppInt.v
- Coqdep lib/coq/set/SetApp.v
- Coqdep lib/coq/set/FsetSum.v
- Coqdep lib/coq/set/FsetInt.v
- Coqdep lib/coq/set/FsetInduction.v
- Coqdep lib/coq/set/Fset.v
- Coqdep lib/coq/set/Cardinal.v
- Coqdep lib/coq/number/Coprime.v
- Coqdep lib/coq/set/Set.v
- Coqdep lib/coq/number/Gcd.v
- Coqdep lib/coq/number/Parity.v
- Coqdep lib/coq/number/Prime.v
- Coqdep lib/coq/real/RealInfix.v
- Coqdep lib/coq/number/Divisibility.v
- Coqdep lib/coq/real/Trigonometry.v
- Coqdep lib/coq/real/Square.v
- Coqdep lib/coq/real/Real.v
- Coqdep lib/coq/real/PowerReal.v
- Coqdep lib/coq/real/PowerInt.v
- Coqdep lib/coq/real/MinMax.v
- Coqdep lib/coq/real/FromInt.v
- Coqdep lib/coq/real/ExpLog.v
- Coqdep lib/coq/real/Abs.v
- Coqdep lib/coq/bool/Bool.v
- Coqdep lib/coq/int/NumOf.v
- Coqdep lib/coq/int/Power.v
- Coqdep lib/coq/int/MinMax.v
- Coqdep lib/coq/int/Int.v
- Coqdep lib/coq/int/EuclideanDivision.v
- Coqdep lib/coq/int/Div2.v
- Coqdep lib/coq/int/ComputerDivision.v
- Coqdep lib/coq/int/Abs.v
- Coqdep lib/coq/int/Exponentiation.v
- Coqdep lib/coq/WellFounded.v
- Coqdep lib/coq/HighOrd.v
- Coqdep lib/coq/BuiltIn.v
- Ocamldep src/why3session/why3session_main.ml
- Ocamldep src/tools/why3shell.ml
- Ocamldep src/why3session/why3session_create.ml
- Ocamldep src/why3session/why3session_output.ml
- Ocamldep src/why3session/why3session_update.ml
- Ocamldep src/why3session/why3session_latex.ml
- Ocamldep src/why3session/why3session_html.ml
- Ocamldep src/why3session/why3session_info.ml
- Ocamldep src/why3session/why3session_lib.ml
- Ocamldep src/ide/why3web.ml
- Ocamllex plugins/tptp/tptp_lexer.mll
- Ocamldep src/ide/wserver.ml
- Ocamllex src/tools/why3wc.mll
- Ocamllex plugins/python/py_lexer.mll
- Menhir plugins/tptp/tptp_parser.mly
- Ocamllex plugins/coma/coma_lexer.mll
- Menhir src/parser/parser_common.mly plugins/coma/coma_parser.mly
- Menhir plugins/python/py_parser.mly
- Ocamllex plugins/cfg/cfg_lexer.mll
- Ocamllex plugins/microc/mc_lexer.mll
- Menhir plugins/microc/mc_parser.mly
- Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly
- 69 states, 1256 transitions, table size 5438 bytes
- 1453 additional bytes used for bindings
- Ocamllex plugins/parser/dimacs.mll
- 77 states, 473 transitions, table size 2354 bytes
- 1504 additional bytes used for bindings
- Generate src/util/config.ml
- 101 states, 1563 transitions, table size 6858 bytes
- 3126 additional bytes used for bindings
- Ocamllex src/util/rc.mll
- Ocamllex src/util/lexlib.mll
- 34 states, 434 transitions, table size 1940 bytes
- 1293 additional bytes used for bindings
- Ocamllex src/parser/lexer.mll
- Menhir src/parser/parser_common.mly src/parser/parser.mly
- Menhir src/parser/parser_common.mly
- Menhir src/driver/driver_parser.mly
- 39 states, 600 transitions, table size 2634 bytes
- 1338 additional bytes used for bindings
- 48 states, 1889 transitions, table size 7844 bytes
- 3073 additional bytes used for bindings
- Ocamllex src/driver/driver_lexer.mll
- Ocamllex src/driver/sexp.mll
- Ocamllex src/session/xml.mll
- 173 states, 4796 transitions, table size 20222 bytes
- 9853 additional bytes used for bindings
- Ocamllex src/session/strategy_parser.mll
- 33 states, 370 transitions, table size 1678 bytes
- 34 states, 1366 transitions, table size 5668 bytes
- 117 states, 1396 transitions, table size 6286 bytes
- 3556 additional bytes used for bindings
- 251 states, 6731 transitions, table size 28430 bytes
- 16559 additional bytes used for bindings
- cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml
- 174 states, 4831 transitions, table size 20368 bytes
- 9859 additional bytes used for bindings
- cp src/util/json_parser.ml src/trywhy3/json_parser.ml
- 307 states, 15627 transitions, table size 64350 bytes
- 59 states, 799 transitions, table size 3550 bytes
- 2611 additional bytes used for bindings
- cp src/util/json_lexer.ml src/trywhy3/json_lexer.ml
- cp src/util/json_parser.mli src/trywhy3/json_parser.mli
- Ocamldep src/why3doc/doc_main.ml
- Ocamldep src/why3doc/doc_lexer.ml
- Ocamldep src/why3doc/doc_def.ml
- Ocamldep src/why3doc/doc_html.ml
- Read 3 sample input sentences and 3 error messages.
- menhir --explain --strict src/parser/parser_common.mly src/parser/parser.mly --base src/parser/parser --compile-errors \
- src/parser/handcrafted.messages > src/parser/parser_messages.ml
- Read 3 sample input sentences and 3 error messages.
- Ocamldep src/tools/why3bench.ml
- Ocamldep src/tools/why3wc.ml
- Ocamldep src/tools/why3show.ml
- Ocamldep src/tools/why3replay.ml
- Ocamldep src/tools/why3realize.ml
- Ocamldep src/tools/why3prove.ml
- Ocamldep src/tools/why3execute.ml
- Ocamldep src/tools/why3config.ml
- Ocamldep src/tools/main.ml
- Ocamldep plugins/cfg/cfg_ast.mli
- Ocamldep plugins/microc/mc_ast.mli
- Ocamldep src/tools/why3extract.ml
- Ocamldep plugins/python/py_ast.mli
- Ocamldep plugins/tptp/tptp_ast.mli
- Ocamldep plugins/cfg/cfg_main.ml
- Ocamldep plugins/cfg/subregion_analysis.ml
- Ocamldep plugins/cfg/cfg_paths.ml
- Ocamldep plugins/cfg/cfg_lexer.ml
- Ocamldep plugins/cfg/cfg_parser.ml
- Ocamldep plugins/microc/mc_main.ml
- Ocamldep plugins/microc/mc_parser.ml
- Ocamldep plugins/microc/mc_printer.ml
- Ocamldep plugins/microc/mc_lexer.ml
- Ocamldep plugins/python/py_main.ml
- Ocamldep plugins/python/py_lexer.ml
- Ocamldep plugins/python/py_parser.ml
- Ocamldep plugins/coma/coma_main.ml
- Ocamldep plugins/coma/coma_lexer.ml
- Ocamldep plugins/coma/coma_typing.ml
- Ocamldep plugins/coma/coma_parser.ml
- Ocamldep plugins/coma/coma_syntax.ml
- Ocamldep plugins/coma/coma_logic.ml
- Ocamldep plugins/tptp/tptp_printer.ml
- Ocamldep plugins/tptp/tptp_typing.ml
- Ocamldep plugins/tptp/tptp_lexer.ml
- Ocamldep plugins/tptp/tptp_parser.ml
- Ocamldep plugins/parser/dimacs.ml
- Ocamldep plugins/strategies/forward_propagation.ml
- Ocamldep src/session/unix_scheduler.ml
- Ocamldep plugins/parser/genequlin.ml
- Ocamldep src/driver/driver_ast.mli
- Ocamldep src/session/json_util.ml
- Ocamldep src/session/itp_server.ml
- Ocamldep src/session/controller_itp.ml
- Ocamldep src/session/itp_communication.ml
- Ocamldep src/session/server_utils.ml
- Ocamldep src/session/strategy_parser.ml
- Ocamldep src/session/strategy.ml
- Ocamldep src/session/session_itp.ml
- Ocamldep src/session/termcode.ml
- Ocamldep src/session/xml.ml
- Ocamldep src/session/compress.ml
- Ocamldep src/printer/mathematica.ml
- Ocamldep src/printer/simplify.ml
- Ocamldep src/printer/yices.ml
- Ocamldep src/printer/cvc3.ml
- Ocamldep src/printer/gappa.ml
- Ocamldep src/printer/isabelle.ml
- Ocamldep src/printer/smtv2.ml
- Ocamldep src/printer/pvs.ml
- Ocamldep src/printer/coq.ml
- Ocamldep src/printer/alt_ergo.ml
- Ocamldep src/printer/smtv1.ml
- Ocamldep src/printer/cntexmp_printer.ml
- Ocamldep src/printer/why3printer.ml
- Ocamldep src/transform/keep_only_arithmetic.ml
- Ocamldep src/transform/reflection.ml
- Ocamldep src/transform/prepare_for_counterexmp.ml
- Ocamldep src/transform/induction_pr.ml
- Ocamldep src/transform/induction.ml
- Ocamldep src/transform/congruence.ml
- Ocamldep src/transform/cut.ml
- Ocamldep src/transform/destruct.ml
- Ocamldep src/transform/ind_itp.ml
- Ocamldep src/transform/introduction.ml
- Ocamldep src/transform/subst.ml
- Ocamldep src/transform/apply.ml
- Ocamldep src/transform/eliminate_literal.ml
- Ocamldep src/transform/case.ml
- Ocamldep src/transform/generic_arg_trans_utils.ml
- Ocamldep src/transform/smoke_detector.ml
- Ocamldep src/transform/prop_curry.ml
- Ocamldep src/transform/instantiate_predicate.ml
- Ocamldep src/transform/eliminate_epsilon.ml
- Ocamldep src/transform/lift_epsilon.ml
- Ocamldep src/transform/abstraction.ml
- Ocamldep src/transform/close_epsilon.ml
- Ocamldep src/transform/filter_trigger.ml
- Ocamldep src/transform/encoding_twin.ml
- Ocamldep src/transform/simplify_array.ml
- Ocamldep src/transform/encoding_sort.ml
- Ocamldep src/transform/encoding_tags_full.ml
- Ocamldep src/transform/encoding_tags.ml
- Ocamldep src/transform/encoding_guards.ml
- Ocamldep src/transform/encoding_guards_full.ml
- Ocamldep src/transform/encoding_select.ml
- Ocamldep src/transform/encoding.ml
- Ocamldep src/transform/discriminate.ml
- Ocamldep src/transform/libencoding.ml
- Ocamldep src/transform/eliminate_algebraic.ml
- Ocamldep src/transform/eliminate_if.ml
- Ocamldep src/transform/eliminate_let.ml
- Ocamldep src/transform/eliminate_inductive.ml
- Ocamldep src/transform/eliminate_symbol.ml
- Ocamldep src/transform/eliminate_unknown_lsymbols.ml
- Ocamldep src/transform/eliminate_unknown_types.ml
- Ocamldep src/transform/abstract_quantifiers.ml
- Ocamldep src/transform/extensional.ml
- Ocamldep src/transform/eliminate_definition.ml
- Ocamldep src/transform/detect_polymorphism.ml
- Ocamldep src/transform/remove_unused.ml
- Ocamldep src/transform/compute.ml
- Ocamldep src/transform/reduction_engine.ml
- Ocamldep src/transform/args_wrapper.ml
- Ocamldep src/transform/split_goal.ml
- Ocamldep src/transform/inlining.ml
- Ocamldep src/transform/simplify_formula.ml
- Ocamldep src/parser/sexp_parser.ml
- Ocamldep src/parser/mlw_printer.ml
- Ocamldep src/parser/lexer.ml
- Ocamldep src/parser/report.ml
- Ocamldep src/parser/typing.ml
- Ocamldep src/parser/parser.ml
- Ocamldep src/parser/parser_messages.ml
- Ocamldep src/parser/glob.ml
- Ocamldep src/parser/ptree_helpers.ml
- Ocamldep src/parser/ptree.ml
- Ocamldep src/extract/java.ml
- Ocamldep src/extract/cakeml.ml
- Ocamldep src/extract/ocaml.ml
- Ocamldep src/extract/c.ml
- Ocamldep src/extract/ml_printer.ml
- Ocamldep src/extract/pdriver.ml
- Ocamldep src/extract/mlinterp.ml
- Ocamldep src/mlw/pinterp.ml
- Ocamldep src/extract/compile.ml
- Ocamldep src/mlw/rac.ml
- Ocamldep src/extract/mltree.ml
- Ocamldep src/mlw/pinterp_core.ml
- Ocamldep src/mlw/big_real.ml
- Ocamldep src/mlw/check_ce.ml
- Ocamldep src/mlw/dexpr.ml
- Ocamldep src/mlw/pmodule.ml
- Ocamldep src/mlw/vc.ml
- Ocamldep src/mlw/typeinv.ml
- Ocamldep src/mlw/eval_match.ml
- Ocamldep src/mlw/ity.ml
- Ocamldep src/driver/smtv2_model_parser.ml
- Ocamldep src/mlw/pdecl.ml
- Ocamldep src/mlw/expr.ml
- Ocamldep src/driver/sexp.ml
- Ocamldep src/driver/driver.ml
- Ocamldep src/driver/driver_lexer.ml
- Ocamldep src/driver/smtv2_model_defs.ml
- Ocamldep src/driver/driver_parser.ml
- Ocamldep src/driver/autodetection.ml
- Ocamldep src/driver/call_provers.ml
- Ocamldep src/driver/whyconf.ml
- Ocamldep src/driver/prove_client.ml
- Ocamldep src/core/model_parser.ml
- Ocamldep src/core/env.ml
- Ocamldep src/core/printer.ml
- Ocamldep src/core/trans.ml
- Ocamldep src/core/pretty.ml
- Ocamldep src/core/dterm.ml
- Ocamldep src/core/task.ml
- Ocamldep src/core/keywords.ml
- Ocamldep src/core/parser_tokens.ml
- Ocamldep src/core/theory.ml
- Ocamldep src/core/coercion.ml
- Ocamldep src/core/decl.ml
- Ocamldep src/core/pattern.ml
- Ocamldep src/core/term.ml
- Ocamldep src/core/ty.ml
- Ocamldep src/core/ident.ml
- Ocamldep src/util/re.ml
- Ocamldep src/util/pqueue.ml
- Ocamldep src/util/vector.ml
- Ocamldep src/util/plugin.ml
- Ocamldep src/util/constant.ml
- Ocamldep src/util/number.ml
- Ocamldep src/util/bigInt.ml
- Ocamldep src/util/print_tree.ml
- Ocamldep src/util/rc.ml
- Ocamldep src/util/sysutil.ml
- Ocamldep src/util/cmdline.ml
- Ocamldep src/util/lexlib.ml
- Ocamldep src/util/loc.ml
- Ocamldep src/util/json_lexer.ml
- Ocamldep src/util/debug.ml
- Ocamldep src/util/json_parser.ml
- Ocamldep src/util/json_base.ml
- Ocamldep src/util/hashcons.ml
- Ocamldep src/util/getopt.ml
- Ocamldep src/util/wstdlib.ml
- Ocamldep src/util/diffmap.ml
- Ocamldep src/util/hcpt.ml
- Ocamldep src/util/weakhtbl.ml
- Ocamldep src/util/exthtbl.ml
- Ocamldep src/util/extset.ml
- Ocamldep src/util/extmap.ml
- Ocamldep src/util/pp.ml
- Ocamldep src/util/strings.ml
- Ocamldep src/util/opt.ml
- Ocamldep src/util/lists.ml
- Ocamldep src/util/util.ml
- Ocamldep src/util/mlmpfr_wrapper.ml
- Ocamldep src/util/exn_printer.ml
- Ocamldep src/trywhy3/worker_proto.ml
- Ocamldep src/util/config.ml
- Ocamldep src/util/mysexplib.ml
- Ocamldep src/trywhy3/why3_worker.ml
- Ocamldep src/trywhy3/json_lexer.ml
- Ocamldep src/trywhy3/trywhy3.ml
- Ocamldep src/trywhy3/shortener.ml
- Ocamldep src/trywhy3/bindings.ml
- Ocamldep src/trywhy3/json_base.ml
- Ocamldep src/trywhy3/json_parser.ml
- 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]
- Coqc lib/coq/WellFounded.v
- Coqc lib/coq/HighOrd.v
- Coqc lib/coq/bool/Bool.v
- Coqc lib/coq/int/Int.v
- Coqc lib/coq/real/Real.v
- Coqc lib/coq/list/List.v
- Coqc lib/coq/option/Option.v
- Coqc lib/coq/int/Exponentiation.v
- Coqc lib/coq/int/Abs.v
- Coqc lib/coq/int/MinMax.v
- Coqc lib/coq/bv/Pow2int.v
- Coqc lib/coq/list/Length.v
- Coqc lib/coq/list/Mem.v
- Coqc lib/coq/list/Nth.v
- Coqc lib/coq/list/HdTl.v
- Coqc lib/coq/list/HdTlNoOpt.v
- Coqc lib/coq/list/NthNoOpt.v
- Coqc lib/coq/list/Combine.v
- 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/real/Abs.v
- Coqc lib/coq/real/FromInt.v
- Coqc lib/coq/real/ExpLog.v
- Coqc lib/coq/real/MinMax.v
- Coqc lib/coq/real/RealInfix.v
- Coqc lib/coq/real/Square.v
- Coqc lib/coq/int/NumOf.v
- Coqc lib/coq/map/Map.v
- Coqc lib/coq/map/MapExt.v
- 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/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/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]
- Coqc lib/coq/int/EuclideanDivision.v
- Coqc lib/coq/int/ComputerDivision.v
- File "./lib/coq/list/NthNoOpt.v", line 21, characters 74-82:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthNoOpt.v", line 40, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-9.0,deprecated-syntactic-definition,deprecated,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/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]
- 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]
- Coqc lib/coq/int/Power.v
- Coqc lib/coq/real/PowerInt.v
- File "./lib/coq/list/Nth.v", line 22, characters 64-72:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-9.0,deprecated-syntactic-definition,deprecated,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/list/Nth.v", line 44, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/Nth.v", line 45, characters 9-17:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-9.0,deprecated-syntactic-definition,deprecated,default]
- 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]
- Coqc lib/coq/list/NthHdTl.v
- 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/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]
- 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 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]
- Coqc lib/coq/real/Trigonometry.v
- 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]
- Coqc lib/coq/list/NthLength.v
- Coqc lib/coq/list/Append.v
- 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/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]
- Coqc lib/coq/map/Const.v
- 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]
- Coqc lib/coq/map/Occ.v
- File "./lib/coq/int/EuclideanDivision.v", line 24, characters 18-22:
- Warning: Notation Zmod is deprecated since 8.17.
- Use Coq.ZArith.BinIntDef.Z.modulo instead
- [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/int/EuclideanDivision.v", line 24, characters 18-22:
- Warning: Notation Zmod is deprecated since 8.17.
- Use Coq.ZArith.BinIntDef.Z.modulo instead
- [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
- File "./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/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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 34, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 56, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLength.v", line 82, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-9.0,deprecated-syntactic-definition,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/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]
- 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]
- 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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthHdTl.v", line 34, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/real/Trigonometry.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/Trigonometry.v", line 15, 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]
- File "./lib/coq/real/Trigonometry.v", line 16, 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/Trigonometry.v", line 17, characters 8-21:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Rtrigo1"
- or the deprecated "From Coq Require Reals.Rtrigo1"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- File "./lib/coq/real/Trigonometry.v", line 18, characters 8-19:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals.Ratan"
- or the deprecated "From Coq Require Reals.Ratan"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/number/Parity.v
- Coqc lib/coq/list/Distinct.v
- Coqc lib/coq/list/NthLengthAppend.v
- Coqc lib/coq/list/Reverse.v
- Coqc lib/coq/real/PowerReal.v
- File "./lib/coq/real/Trigonometry.v", line 24, characters 15-20:
- Warning: Loading Stdlib without prefix is deprecated.
- Use "From Stdlib Require Reals" or the deprecated "From Coq Require Reals"
- for compatibility with older Coq versions.
- [deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
- Coqc lib/coq/set/Set.v
- Coqc lib/coq/int/Div2.v
- Coqc lib/coq/bv/BV_Gen.v
- Coqc lib/coq/for_drivers/ComputerOfEuclideanDivision.v
- 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/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/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/list/NthLengthAppend.v", line 39, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,deprecated,default]
- File "./lib/coq/list/NthLengthAppend.v", line 40, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-9.0,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 48, characters 0-32:
- 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/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/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/list/NthLengthAppend.v", line 66, characters 12-23:
- Warning: Reference Zeq_bool_if is deprecated since 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-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 9.0. Use Z.eqb_eq instead.
- [deprecated-reference-since-9.0,deprecated-since-9.0,deprecated-reference,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/list/NthLengthAppend.v", line 67, characters 5-13:
- Warning: Notation Zeq_bool is deprecated since 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-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 9.0. Use Z.eqb instead.
- [deprecated-syntactic-definition-since-9.0,deprecated-since-9.0,deprecated-syntactic-definition,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]
- 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 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]
- 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/set/Set.v", line 141, characters 0-54:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- Coqc lib/coq/number/Divisibility.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]
- 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]
- Coqc lib/coq/list/NumOcc.v
- Coqc lib/coq/list/RevAppend.v
- File "./lib/coq/bv/BV_Gen.v", line 338, 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 338, 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 344, 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 349, 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 350, 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 350, 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/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 389, 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 389, 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/map/Occ.v", line 247, characters 0-19:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/map/Occ.v", line 247, characters 0-19:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/map/Occ.v", line 247, characters 0-19:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 447, 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 452, 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 453, 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 453, 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 476, 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 476, 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 479, 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 479, 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 486, 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 489, 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 494, 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 495, 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 495, 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 529, 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 529, 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 532, 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/set/Set.v", line 335, characters 2-29:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,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/bv/BV_Gen.v", line 566, 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/set/Set.v", line 335, characters 2-29:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Set.v", line 348, characters 0-27:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Set.v", line 348, characters 0-27:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 601, 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 612, 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 615, 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 615, 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 623, 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 624, 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 625, 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 627, 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 634, 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 638, 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 640, 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 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/number/Divisibility.v", line 206, characters 8-12:
- Warning: Notation Zmod is deprecated since 8.17.
- Use Coq.ZArith.BinIntDef.Z.modulo instead
- [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
- File "./lib/coq/number/Divisibility.v", line 206, characters 8-12:
- Warning: Notation Zmod is deprecated since 8.17.
- Use Coq.ZArith.BinIntDef.Z.modulo instead
- [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/set/Cardinal.v
- Coqc lib/coq/list/Permut.v
- File "./lib/coq/bv/BV_Gen.v", line 736, 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 750, 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 757, 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 766, 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 766, 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 766, 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 766, 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 767, 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 768, 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 781, 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 798, 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 867, 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]
- Coqc lib/coq/map/MapInjection.v
- Coqc lib/coq/map/MapPermut.v
- File "./lib/coq/bv/BV_Gen.v", line 997, characters 52-56:
- Warning: Notation Zmod is deprecated since 8.17.
- Use Coq.ZArith.BinIntDef.Z.modulo instead
- [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
- Coqc lib/coq/number/Gcd.v
- Coqc lib/coq/number/Prime.v
- 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 1216, 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 1216, 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 1250, 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 1250, 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 1252, 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 1259, 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 1259, 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 1261, 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 1344, 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 1345, 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 1345, 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/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/bv/BV_Gen.v", line 1392, 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 1392, 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/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 1393, 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/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/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/bv/BV_Gen.v", line 1639, 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 1687, 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 1697, 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 1707, 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/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/number/Prime.v", line 36, characters 0-10:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/number/Prime.v", line 36, characters 0-10:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/bv/BV_Gen.v", line 2346, 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 2346, 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 2354, 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 2354, 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]
- Coqc lib/coq/number/Coprime.v
- File "./lib/coq/set/Cardinal.v", line 168, characters 4-41:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 169, characters 53-94:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 170, characters 4-21:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 187, characters 4-21:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 192, characters 51-61:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 446, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 474, characters 4-41:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Cardinal.v", line 603, 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 603, 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 603, 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 604, 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 604, 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 604, 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 622, 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 622, 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 622, 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 622, 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 622, 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 622, 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/set/Cardinal.v", line 739, 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 739, 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 739, 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 820, 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 820, 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 820, 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 845, 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 845, 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 845, 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]
- File "./lib/coq/set/Fset.v", line 105, characters 20-30:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Fset.v", line 111, characters 42-52:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Fset.v", line 120, characters 12-22:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Fset.v", line 165, characters 0-37:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/Fset.v", line 165, characters 0-37:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- Coqc lib/coq/set/FsetInduction.v
- Coqc lib/coq/set/FsetInt.v
- Coqc lib/coq/set/FsetSum.v
- Coqc lib/coq/set/SetApp.v
- Coqc lib/coq/set/SetImp.v
- File "./lib/coq/set/SetImp.v", line 56, characters 0-10:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- 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]
- File "./lib/coq/set/FsetInt.v", line 130, characters 0-32:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 131, characters 0-30:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 186, characters 6-16:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 187, characters 6-34:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 187, characters 6-34:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 188, characters 6-34:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 188, characters 6-34:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 218, characters 0-69:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 218, characters 0-69:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 218, characters 0-69:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 233, characters 2-71:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 233, characters 2-71:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 233, characters 2-71:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 233, characters 2-71:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 233, characters 2-71:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 235, characters 17-69:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 235, characters 17-69:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 235, characters 17-69:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 268, characters 26-36:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetInt.v", line 268, characters 37-47:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 104, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 105, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- Coqc lib/coq/set/SetAppInt.v
- Coqc lib/coq/set/SetImpInt.v
- File "./lib/coq/set/FsetSum.v", line 116, characters 7-17:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 117, characters 7-17:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 118, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 119, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 125, characters 58-68:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 125, characters 58-68:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 125, characters 58-68:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 128, characters 58-68:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 128, characters 58-68:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 128, characters 58-68:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 180, characters 2-44:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 180, characters 2-44:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 183, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 184, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 213, characters 2-44:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 213, characters 2-44:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 216, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 217, characters 4-14:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 315, characters 0-10:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/FsetSum.v", line 316, characters 0-10:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
- File "./lib/coq/set/SetImpInt.v", line 51, characters 0-10:
- Warning:
- "auto with *" was used through the default "intuition_solver" tactic.
- This will be replaced by just "auto" in the future.
- [intuition-auto-with-star,deprecated-since-8.17,deprecated,default]
-> compiled why3-coq.1.8.2
[why3-coq: make install-coq]
+ /usr/bin/make "install-coq" (CWD=/home/opam/.opam/default/.opam-switch/build/why3-coq.1.8.2)
- /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 lib/coq/real/Trigonometry.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.8.2
[WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config
=== STDERR ===
2026-06-24 17:14.23: OK: build why3-coq.1.8.2 (runc: 51.2s, disk: 115KB)
2026-06-24 17:14.23: Job succeeded