=> Bootstrap dependency digest>=20211023: found digest-20220214
===> Skipping vulnerability checks.
WARNING: No /usr/pkg/pkgdb/pkg-vulnerabilities file found.
WARNING: To fix run: `/usr/sbin/pkg_admin -K /usr/pkg/pkgdb fetch-pkg-vulnerabilities'.
===> Building for why3-1.8.0
Generate src/util/config.ml
Ocamllex src/util/rc.mll
Ocamllex src/util/lexlib.mll
Menhir src/util/json_parser.mly
Ocamllex src/util/json_lexer.mll
Ocamllex src/parser/lexer.mll
39 states, 600 transitions, table size 2634 bytes
1338 additional bytes used for bindings
52 states, 495 transitions, table size 2292 bytes
48 states, 1889 transitions, table size 7844 bytes
3073 additional bytes used for bindings
Menhir src/parser/parser_common.mly src/parser/parser.mly
Menhir src/parser/parser_common.mly
Menhir src/driver/driver_parser.mly
Ocamllex src/driver/driver_lexer.mll
174 states, 4831 transitions, table size 20368 bytes
9859 additional bytes used for bindings
Ocamllex src/driver/sexp.mll
34 states, 1366 transitions, table size 5668 bytes
Ocamllex src/session/xml.mll
Ocamllex src/session/strategy_parser.mll
cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml
33 states, 370 transitions, table size 1678 bytes
117 states, 1396 transitions, table size 6286 bytes
3556 additional bytes used for bindings
59 states, 799 transitions, table size 3550 bytes
2611 additional bytes used for bindings
Menhir plugins/tptp/tptp_parser.mly
Menhir src/parser/parser_common.mly plugins/coma/coma_parser.mly
Ocamllex plugins/python/py_lexer.mll
Ocamllex plugins/coma/coma_lexer.mll
Ocamllex plugins/tptp/tptp_lexer.mll
Menhir plugins/python/py_parser.mly
69 states, 1256 transitions, table size 5438 bytes
1453 additional bytes used for bindings
101 states, 1563 transitions, table size 6858 bytes
3126 additional bytes used for bindings
Ocamllex plugins/microc/mc_lexer.mll
Menhir plugins/microc/mc_parser.mly
251 states, 6731 transitions, table size 28430 bytes
16559 additional bytes used for bindings
77 states, 473 transitions, table size 2354 bytes
1504 additional bytes used for bindings
Ocamllex plugins/cfg/cfg_lexer.mll
Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly
Ocamllex plugins/parser/dimacs.mll
34 states, 434 transitions, table size 1940 bytes
1293 additional bytes used for bindings
173 states, 4796 transitions, table size 20222 bytes
9853 additional bytes used for bindings
Ocamllex src/tools/why3wc.mll
Ocamldep src/ide/gconfig.ml
Ocamldep src/ide/ide_utils.ml
Ocamldep src/ide/why3ide.ml
307 states, 15627 transitions, table size 64350 bytes
Ocamldep src/ide/wserver.ml
Read 3 sample input sentences and 3 error messages.
Ocamldep src/ide/why3web.ml
Ocamldep src/why3session/why3session_lib.ml
Ocamldep src/why3session/why3session_info.ml
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
Ocamldep src/why3session/why3session_html.ml
Ocamldep src/why3session/why3session_latex.ml
Ocamldep src/why3session/why3session_update.ml
Ocamldep src/why3session/why3session_output.ml
Ocamldep src/why3session/why3session_create.ml
Ocamldep src/why3session/why3session_main.ml
Ocamldep src/tools/why3shell.ml
Coqdep   lib/coq/BuiltIn.v
Coqdep   lib/coq/HighOrd.v
Coqdep   lib/coq/WellFounded.v
Coqdep   lib/coq/int/Exponentiation.v
Read 3 sample input sentences and 3 error messages.
Coqdep   lib/coq/int/Abs.v
Coqdep   lib/coq/int/ComputerDivision.v
Coqdep   lib/coq/int/Div2.v
Coqdep   lib/coq/int/EuclideanDivision.v
Coqdep   lib/coq/int/Int.v
Coqdep   lib/coq/int/MinMax.v
Coqdep   lib/coq/int/Power.v
Coqdep   lib/coq/int/NumOf.v
Coqdep   lib/coq/bool/Bool.v
Coqdep   lib/coq/real/Abs.v
Coqdep   lib/coq/real/ExpLog.v
Coqdep   lib/coq/real/FromInt.v
Coqdep   lib/coq/real/MinMax.v
Coqdep   lib/coq/real/PowerInt.v
Coqdep   lib/coq/real/PowerReal.v
Coqdep   lib/coq/real/Real.v
Coqdep   lib/coq/real/RealInfix.v
Coqdep   lib/coq/real/Square.v
Coqdep   lib/coq/real/Trigonometry.v
Coqdep   lib/coq/number/Divisibility.v
Coqdep   lib/coq/number/Gcd.v
Coqdep   lib/coq/number/Parity.v
Coqdep   lib/coq/number/Prime.v
Coqdep   lib/coq/number/Coprime.v
Coqdep   lib/coq/set/Set.v
Coqdep   lib/coq/set/Cardinal.v
Coqdep   lib/coq/set/Fset.v
Coqdep   lib/coq/set/FsetInduction.v
Coqdep   lib/coq/set/FsetInt.v
Coqdep   lib/coq/set/FsetSum.v
Coqdep   lib/coq/set/SetApp.v
Coqdep   lib/coq/set/SetAppInt.v
Coqdep   lib/coq/set/SetImp.v
Coqdep   lib/coq/set/SetImpInt.v
Coqdep   lib/coq/map/Map.v
Coqdep   lib/coq/map/Const.v
Coqdep   lib/coq/map/MapExt.v
Coqdep   lib/coq/map/Occ.v
Coqdep   lib/coq/map/MapPermut.v
Coqdep   lib/coq/map/MapInjection.v
Coqdep   lib/coq/list/List.v
Coqdep   lib/coq/list/Length.v
Coqdep   lib/coq/list/Mem.v
Coqdep   lib/coq/list/Nth.v
Coqdep   lib/coq/list/NthLength.v
Coqdep   lib/coq/list/HdTl.v
Coqdep   lib/coq/list/NthHdTl.v
Coqdep   lib/coq/list/Append.v
Coqdep   lib/coq/list/NthLengthAppend.v
Coqdep   lib/coq/list/Reverse.v
Coqdep   lib/coq/list/HdTlNoOpt.v
Coqdep   lib/coq/list/NthNoOpt.v
Coqdep   lib/coq/list/RevAppend.v
Coqdep   lib/coq/list/Combine.v
Coqdep   lib/coq/list/Distinct.v
Coqdep   lib/coq/list/NumOcc.v
Coqdep   lib/coq/list/Permut.v
Coqdep   lib/coq/option/Option.v
Coqdep   lib/coq/bv/Pow2int.v
Coqdep   lib/coq/bv/BV_Gen.v
Coqdep   lib/coq/for_drivers/ComputerOfEuclideanDivision.v
Ocamldep src/isabelle-client/isabelle_client_main.ml
Ocamldep src/tools/why3pp.ml
Ocamllex src/why3doc/doc_lexer.mll
120 states, 706 transitions, table size 3544 bytes
1763 additional bytes used for bindings
cp src/util/json_base.ml src/trywhy3/json_base.ml
cp src/util/json_base.mli src/trywhy3/json_base.mli
cp src/util/json_parser.ml src/trywhy3/json_parser.ml
cp src/util/json_lexer.ml src/trywhy3/json_lexer.ml
cp src/util/json_parser.mli src/trywhy3/json_parser.mli
cp src/util/json_lexer.mli src/trywhy3/json_lexer.mli
Ocamldep src/util/exn_printer.ml
Ocamldep src/util/mysexplib.ml
Ocamldep src/util/config.ml
Ocamldep src/util/bigInt.ml
Ocamldep src/util/util.ml
Ocamldep src/util/mlmpfr_wrapper.ml
Ocamldep src/util/opt.ml
Ocamldep src/util/lists.ml
Ocamldep src/util/strings.ml
Ocamldep src/util/extmap.ml
Ocamldep src/util/pp.ml
Ocamldep src/util/extset.ml
Ocamldep src/util/exthtbl.ml
Ocamldep src/util/weakhtbl.ml
Ocamldep src/util/diffmap.ml
Ocamldep src/util/hcpt.ml
Ocamldep src/util/hashcons.ml
Ocamldep src/util/wstdlib.ml
Ocamldep src/util/getopt.ml
Ocamldep src/util/json_base.ml
Ocamldep src/util/json_parser.ml
Ocamldep src/util/json_lexer.ml
Ocamldep src/util/debug.ml
Ocamldep src/util/loc.ml
Ocamldep src/util/print_tree.ml
Ocamldep src/util/cmdline.ml
Ocamldep src/util/lexlib.ml
Ocamldep src/util/sysutil.ml
Ocamldep src/util/rc.ml
Ocamldep src/util/plugin.ml
Ocamldep src/util/constant.ml
Ocamldep src/util/number.ml
Ocamldep src/util/pqueue.ml
Ocamldep src/util/re.ml
Ocamldep src/core/ident.ml
Ocamldep src/util/vector.ml
Ocamldep src/core/ty.ml
Ocamldep src/core/term.ml
Ocamldep src/core/pattern.ml
Ocamldep src/core/decl.ml
Ocamldep src/core/coercion.ml
Ocamldep src/core/parser_tokens.ml
Ocamldep src/core/theory.ml
Ocamldep src/core/keywords.ml
Ocamldep src/core/task.ml
Ocamldep src/core/pretty.ml
Ocamldep src/core/dterm.ml
Ocamldep src/core/env.ml
Ocamldep src/core/trans.ml
Ocamldep src/core/model_parser.ml
Ocamldep src/core/printer.ml
Ocamldep src/driver/prove_client.ml
Ocamldep src/driver/whyconf.ml
Ocamldep src/driver/call_provers.ml
Ocamldep src/driver/driver_parser.ml
Ocamldep src/driver/driver_lexer.ml
Ocamldep src/driver/driver.ml
Ocamldep src/driver/autodetection.ml
Ocamldep src/driver/sexp.ml
Ocamldep src/driver/smtv2_model_defs.ml
Ocamldep src/driver/smtv2_model_parser.ml
Ocamldep src/mlw/ity.ml
Ocamldep src/mlw/expr.ml
Ocamldep src/mlw/pdecl.ml
Ocamldep src/mlw/eval_match.ml
Ocamldep src/mlw/typeinv.ml
Ocamldep src/mlw/vc.ml
Ocamldep src/mlw/pmodule.ml
Ocamldep src/mlw/dexpr.ml
Ocamldep src/mlw/big_real.ml
Ocamldep src/mlw/pinterp_core.ml
Ocamldep src/mlw/pinterp.ml
Ocamldep src/mlw/rac.ml
Ocamldep src/mlw/check_ce.ml
Ocamldep src/extract/compile.ml
Ocamldep src/extract/mltree.ml
Ocamldep src/extract/mlinterp.ml
Ocamldep src/extract/pdriver.ml
Ocamldep src/extract/ml_printer.ml
Ocamldep src/extract/c.ml
Ocamldep src/extract/ocaml.ml
Ocamldep src/extract/cakeml.ml
Ocamldep src/parser/ptree.ml
Ocamldep src/extract/java.ml
Ocamldep src/parser/ptree_helpers.ml
Ocamldep src/parser/glob.ml
Ocamldep src/parser/parser_messages.ml
Ocamldep src/parser/typing.ml
Ocamldep src/parser/parser.ml
Ocamldep src/parser/report.ml
Ocamldep src/parser/lexer.ml
Ocamldep src/parser/sexp_parser.ml
Ocamldep src/transform/simplify_formula.ml
Ocamldep src/parser/mlw_printer.ml
Ocamldep src/transform/inlining.ml
Ocamldep src/transform/args_wrapper.ml
Ocamldep src/transform/split_goal.ml
Ocamldep src/transform/reduction_engine.ml
Ocamldep src/transform/compute.ml
Ocamldep src/transform/detect_polymorphism.ml
Ocamldep src/transform/remove_unused.ml
Ocamldep src/transform/eliminate_definition.ml
Ocamldep src/transform/extensional.ml
Ocamldep src/transform/abstract_quantifiers.ml
Ocamldep src/transform/eliminate_unknown_lsymbols.ml
Ocamldep src/transform/eliminate_symbol.ml
Ocamldep src/transform/eliminate_unknown_types.ml
Ocamldep src/transform/eliminate_inductive.ml
Ocamldep src/transform/eliminate_let.ml
Ocamldep src/transform/libencoding.ml
Ocamldep src/transform/eliminate_if.ml
Ocamldep src/transform/eliminate_algebraic.ml
Ocamldep src/transform/encoding.ml
Ocamldep src/transform/encoding_select.ml
Ocamldep src/transform/discriminate.ml
Ocamldep src/transform/encoding_guards_full.ml
Ocamldep src/transform/encoding_tags_full.ml
Ocamldep src/transform/encoding_guards.ml
Ocamldep src/transform/encoding_tags.ml
Ocamldep src/transform/encoding_twin.ml
Ocamldep src/transform/simplify_array.ml
Ocamldep src/transform/encoding_sort.ml
Ocamldep src/transform/abstraction.ml
Ocamldep src/transform/close_epsilon.ml
Ocamldep src/transform/filter_trigger.ml
Ocamldep src/transform/lift_epsilon.ml
Ocamldep src/transform/eliminate_epsilon.ml
Ocamldep src/transform/instantiate_predicate.ml
Ocamldep src/transform/smoke_detector.ml
Ocamldep src/transform/prop_curry.ml
Ocamldep src/transform/eliminate_literal.ml
Ocamldep src/transform/generic_arg_trans_utils.ml
Ocamldep src/transform/case.ml
Ocamldep src/transform/apply.ml
Ocamldep src/transform/subst.ml
Ocamldep src/transform/introduction.ml
Ocamldep src/transform/ind_itp.ml
Ocamldep src/transform/destruct.ml
Ocamldep src/transform/congruence.ml
Ocamldep src/transform/cut.ml
Ocamldep src/transform/induction.ml
Ocamldep src/transform/induction_pr.ml
Ocamldep src/transform/prepare_for_counterexmp.ml
Ocamldep src/transform/reflection.ml
Ocamldep src/transform/keep_only_arithmetic.ml
Ocamldep src/printer/cntexmp_printer.ml
Ocamldep src/printer/alt_ergo.ml
Ocamldep src/printer/why3printer.ml
Ocamldep src/printer/smtv1.ml
Ocamldep src/printer/coq.ml
Ocamldep src/printer/smtv2.ml
Ocamldep src/printer/pvs.ml
Ocamldep src/printer/isabelle.ml
Ocamldep src/printer/simplify.ml
Ocamldep src/printer/gappa.ml
Ocamldep src/printer/cvc3.ml
Ocamldep src/printer/yices.ml
Ocamldep src/printer/mathematica.ml
Ocamldep src/session/compress.ml
Ocamldep src/session/xml.ml
Ocamldep src/session/termcode.ml
Ocamldep src/session/session_itp.ml
Ocamldep src/session/strategy.ml
Ocamldep src/session/strategy_parser.ml
Ocamldep src/session/server_utils.ml
Ocamldep src/session/itp_communication.ml
Ocamldep src/session/controller_itp.ml
Ocamldep src/session/itp_server.ml
Ocamldep src/session/unix_scheduler.ml
Ocamldep src/session/json_util.ml
Ocamldep src/driver/driver_ast.mli
Ocamldep plugins/parser/genequlin.ml
Ocamldep plugins/transform/hypothesis_selection.ml
Ocamldep plugins/parser/dimacs.ml
Ocamldep plugins/strategies/forward_propagation.ml
Ocamldep plugins/tptp/tptp_parser.ml
Ocamldep plugins/tptp/tptp_typing.ml
Ocamldep plugins/tptp/tptp_printer.ml
Ocamldep plugins/tptp/tptp_lexer.ml
Ocamldep plugins/coma/coma_logic.ml
Ocamldep plugins/coma/coma_parser.ml
Ocamldep plugins/coma/coma_syntax.ml
Ocamldep plugins/coma/coma_lexer.ml
Ocamldep plugins/coma/coma_typing.ml
Ocamldep plugins/coma/coma_main.ml
Ocamldep plugins/python/py_parser.ml
Ocamldep plugins/python/py_lexer.ml
Ocamldep plugins/python/py_main.ml
Ocamldep plugins/microc/mc_parser.ml
Ocamldep plugins/microc/mc_lexer.ml
Ocamldep plugins/microc/mc_printer.ml
Ocamldep plugins/microc/mc_main.ml
Ocamldep plugins/cfg/cfg_parser.ml
Ocamldep plugins/cfg/cfg_lexer.ml
Ocamldep plugins/cfg/cfg_paths.ml
Ocamldep plugins/cfg/subregion_analysis.ml
Ocamldep plugins/cfg/cfg_main.ml
Ocamldep plugins/cfg/stackify.ml
Ocamldep plugins/cfg/cfg_stackify.ml
Ocamldep plugins/tptp/tptp_ast.mli
Ocamldep plugins/python/py_ast.mli
Ocamldep plugins/microc/mc_ast.mli
Ocamldep plugins/cfg/cfg_ast.mli
Ocamldep src/tools/main.ml
Ocamldep src/tools/why3config.ml
Ocamldep src/tools/why3execute.ml
Ocamldep src/tools/why3extract.ml
Ocamldep src/tools/why3realize.ml
Ocamldep src/tools/why3prove.ml
Ocamldep src/tools/why3replay.ml
Ocamldep src/tools/why3show.ml
Ocamldep src/tools/why3wc.ml
Ocamldep src/tools/why3bench.ml
Ocamldep src/why3doc/doc_lexer.ml
Ocamldep src/why3doc/doc_main.ml
Ocamldep src/why3doc/doc_html.ml
Ocamldep src/trywhy3/json_base.ml
Ocamldep src/why3doc/doc_def.ml
Ocamldep src/trywhy3/json_parser.ml
Ocamldep src/trywhy3/json_lexer.ml
Ocamldep src/trywhy3/bindings.ml
Ocamldep src/trywhy3/trywhy3.ml
Ocamldep src/trywhy3/shortener.ml
Ocamldep src/trywhy3/why3_worker.ml
Ocamldep src/trywhy3/worker_proto.ml
mkdir lib/plugins
Ocamlc   src/util/config.mli
Ocamlc   src/util/bigInt.mli
Ocamlc   src/util/exn_printer.mli
Ocamlc   src/util/util.mli
Ocamlc   src/util/mlmpfr_wrapper.mli
Ocamlc   src/util/opt.mli
Ocamlc   src/util/lists.mli
Ocamlc   src/util/strings.mli
Ocamlc   src/util/pp.mli
Ocamlc   src/util/extmap.mli
Ocamlc   src/util/exthtbl.mli
Ocamlc   src/util/weakhtbl.mli
Ocamlc   src/util/hcpt.mli
Ocamlc   src/util/hashcons.mli
Ocamlc   src/util/getopt.mli
Ocamlc   src/util/json_base.mli
Ocamlc   src/util/print_tree.mli
Ocamlc   src/util/sysutil.mli
Ocamlc   src/util/cmdline.mli
Ocamlc   src/util/number.mli
Ocamlc   src/util/lexlib.mli
Ocamlc   src/util/vector.mli
Ocamlc   src/util/re.ml
Ocamlc   src/util/pqueue.mli
Ocamlc   src/driver/prove_client.mli
Ocamlc   src/driver/sexp.mli
Ocamlc   src/driver/smtv2_model_parser.mli
Ocamlc   src/mlw/big_real.mli
Linking src/util/ppx_debug_optim
File "src/util/re.ml", line 1:
Warning 70 [missing-mli]: Cannot find interface file.
Ocamlc   src/extract/c.mli
findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/pkg/lib/ocaml, /usr/pkg/lib/ocaml/compiler-libs
Ocamlc   src/extract/cakeml.mli
Ocamlc   src/extract/java.mli
Ocamlc   src/extract/ocaml.mli
Ocamlc   src/parser/parser_messages.mli
Ocamlc   src/transform/remove_unused.mli
Ocamlc   src/transform/extensional.mli
Ocamlc   src/transform/abstract_quantifiers.mli
Ocamlc   src/transform/eliminate_unknown_types.mli
Ocamlc   src/transform/eliminate_unknown_lsymbols.mli
Ocamlc   src/transform/eliminate_symbol.mli
Ocamlc   src/transform/encoding_select.mli
Ocamlc   src/transform/encoding_guards_full.mli
Ocamlc   src/transform/encoding_tags_full.mli
Ocamlc   src/transform/encoding_tags.mli
Ocamlc   src/transform/encoding_twin.mli
Ocamlc   src/transform/encoding_sort.mli
Ocamlc   src/transform/encoding_guards.mli
Ocamlc   src/transform/simplify_array.mli
Ocamlc   src/transform/filter_trigger.mli
Ocamlc   src/transform/lift_epsilon.mli
Ocamlc   src/transform/prop_curry.mli
Ocamlc   src/transform/instantiate_predicate.mli
Ocamlc   src/transform/case.mli
Ocamlc   src/transform/congruence.mli
Ocamlc   src/transform/induction.mli
Ocamlc   src/transform/induction_pr.mli
Ocamlc   src/transform/prepare_for_counterexmp.mli
Ocamlc   src/printer/alt_ergo.mli
Ocamlc   src/transform/keep_only_arithmetic.mli
Ocamlc   src/printer/smtv1.mli
Ocamlc   src/printer/why3printer.mli
Ocamlc   src/printer/smtv2.mli
Ocamlc   src/printer/pvs.mli
Ocamlc   src/printer/coq.mli
Ocamlc   src/printer/isabelle.mli
Ocamlc   src/printer/simplify.mli
Ocamlc   src/printer/gappa.mli
Ocamlc   src/printer/cvc3.mli
Ocamlc   src/printer/yices.mli
Ocamlc   src/printer/mathematica.mli
Ocamlc   src/session/compress.mli
Ocamlc   src/session/xml.mli
Ocamlc   src/session/unix_scheduler.mli
Ocamlc   src/util/exn_printer.ml
Ocamlc   src/util/mlmpfr_wrapper.ml
Ocamlc   src/util/util.ml
Ocamlc   src/util/config.ml
Ocamlc   src/util/opt.ml
Ocamlc   src/util/lists.ml
Ocamlc   src/util/strings.ml
Ocamlc   src/util/pp.ml
Ocamlc   src/util/extmap.ml
Ocamlc   src/util/weakhtbl.ml
Ocamlc   src/util/exthtbl.ml
Ocamlc   src/util/hcpt.ml
Ocamlc   src/util/hashcons.ml
Ocamlc   src/util/getopt.ml
Ocamlc   src/util/json_base.ml
Ocamlc   src/util/print_tree.ml
Ocamlc   src/util/cmdline.ml
Ocamlc   src/util/sysutil.ml
Ocamlc   src/util/vector.ml
Ocamlc   src/util/pqueue.ml
Ocamlc   src/driver/prove_client.ml
Ocamlc   src/mlw/big_real.ml
Ocamlc   src/driver/sexp.ml
Ocamlc   src/parser/parser_messages.ml
File "src/util/vector.ml", line 22, characters 22-30:
22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t =
                           ^^^^^^^^
Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
Ocamlc   src/session/compress.ml
Ocamlc   src/session/unix_scheduler.ml
Ocamlc   plugins/parser/genequlin.mli
Ocamlc   plugins/parser/dimacs.mli
Ocamlc   plugins/tptp/tptp_printer.mli
Ocamlc   plugins/python/py_main.mli
Ocamlc   plugins/microc/mc_main.mli
Ocamlc   plugins/coma/coma_main.mli
Ocamlc   plugins/cfg/cfg_stackify.mli
Ocamlc   plugins/strategies/forward_propagation.mli
Ocamlc   plugins/transform/hypothesis_selection.mli
Ocamlc   src/tools/main.mli
Ocamlc   src/tools/why3config.mli
Ocamlc   src/tools/why3execute.mli
Ocamlc   src/tools/why3extract.mli
Ocamlc   src/tools/why3prove.mli
Ocamlc   src/tools/why3realize.mli
Ocamlc   src/tools/why3replay.mli
Ocamlc   src/tools/why3show.mli
Ocamlc   src/tools/why3bench.mli
Ocamlc   src/tools/why3wc.mli
Ocamlc   src/ide/why3ide.mli
Ocamlc   src/ide/ide_utils.mli
Ocamlc   src/ide/wserver.mli
Ocamlc   src/ide/why3web.mli
Ocamlc   src/why3session/why3session_main.mli
Ocamlc   src/tools/why3shell.mli
Ocamlc   src/isabelle-client/isabelle_client_main.mli
Ocamlc   src/why3doc/doc_html.mli
Ocamlc   src/tools/why3pp.mli
Ocamlc   src/why3doc/doc_main.mli
gcc -Wall -O -g -o src/server/logging.o -c src/server/logging.c
Ocamlc   src/why3doc/doc_lexer.mli
gcc -Wall -O -g -o src/server/arraylist.o -c src/server/arraylist.c
gcc -Wall -O -g -o src/server/options.o -c src/server/options.c
gcc -Wall -O -g -o src/server/queue.o -c src/server/queue.c
gcc -Wall -O -g -o src/server/readbuf.o -c src/server/readbuf.c
gcc -Wall -O -g -o src/server/request.o -c src/server/request.c
gcc -Wall -O -g -o src/server/proc.o -c src/server/proc.c
gcc -Wall -O -g -o src/server/writebuf.o -c src/server/writebuf.c
gcc -Wall -O -g -o src/server/server-unix.o -c src/server/server-unix.c
gcc -Wall -O -g -o src/server/server-win.o -c src/server/server-win.c
gcc -Wall -O -g -o src/server/cpulimit-unix.o -c src/server/cpulimit-unix.c
gcc -Wall -O -g -o src/server/cpulimit-win.o -c src/server/cpulimit-win.c
Coqc     lib/coq/BuiltIn.v
Generate drivers/coq-realizations.aux
Generate drivers/pvs-realizations.aux
Generate drivers/isabelle-realizations.aux
Ocamlopt src/util/exn_printer.ml
Ocamlopt src/util/config.ml
Ocamlc   src/util/mysexplib.ml
Ocamlopt src/util/mlmpfr_wrapper.ml
Ocamlopt src/util/opt.ml
Ocamlopt src/util/util.ml
Ocamlopt src/util/lists.ml
Ocamlopt src/util/strings.ml
Ocamlopt src/util/pp.ml
Ocamlopt src/util/extmap.ml
Ocamlc   src/util/extset.mli
Ocamlopt src/util/exthtbl.ml
Ocamlopt src/util/weakhtbl.ml
Ocamlc   src/util/diffmap.mli
Ocamlopt src/util/hcpt.ml
Ocamlopt src/util/hashcons.ml
Ocamlc   src/util/wstdlib.mli
Ocamlopt src/util/getopt.ml
Ocamlopt src/util/json_base.ml
Ocamlc   src/util/json_parser.mli
Ocamlc   src/util/debug.mli
Ocamlc   src/util/loc.mli
Ocamlopt src/util/print_tree.ml
Ocamlopt src/util/cmdline.ml
Ocamlopt src/util/sysutil.ml
Ocamlc   src/util/plugin.mli
Ocamlc   src/util/constant.mli
Ocamlopt src/util/vector.ml
Ocamlopt src/util/re.ml
Ocamlc   src/core/ident.mli
Ocamlc   src/core/parser_tokens.mli
Ocamlopt src/driver/prove_client.ml
Ocamlc   src/driver/driver_ast.mli
File "src/util/vector.ml", line 22, characters 22-30:
22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t =
                           ^^^^^^^^
Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
Ocamlc   src/driver/smtv2_model_defs.mli
Ocamlopt src/driver/sexp.ml
Ocamlopt src/mlw/big_real.ml
Ocamlopt src/parser/parser_messages.ml
Ocamlopt src/session/unix_scheduler.ml
Ocamlopt src/session/compress.ml
Ocamlc   src/util/bigInt.ml
Ocamlc   src/util/extset.ml
Ocamlc   src/util/diffmap.ml
Ocamlc   src/util/wstdlib.ml
Ocamlc   src/util/json_parser.ml
Ocamlc   src/util/debug.ml
Ocamlc   src/util/loc.ml
Ocamlc   src/util/lexlib.ml
Ocamlc   src/util/plugin.ml
Ocamlc   src/util/number.ml
Ocamlc   src/util/constant.ml
Ocamlc   src/core/ident.ml
Ocamlc   src/core/parser_tokens.ml
Ocamlc   src/driver/smtv2_model_defs.ml
Ocamlc   src/session/xml.ml
gcc -Wall -o lib/why3server src/server/logging.o src/server/arraylist.o src/server/options.o src/server/queue.o src/server/readbuf.o src/server/request.o src/server/proc.o src/server/writebuf.o src/server/server-unix.o src/server/server-win.o
gcc -Wall -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o
Ocamlopt src/ide/ide_utils.ml
Ocamlopt src/util/mysexplib.ml
Ocamlopt src/util/diffmap.ml
Ocamlopt src/util/extset.ml
Ocamlopt src/util/json_parser.ml
Ocamlc   src/util/json_lexer.mli
Ocamlopt src/util/debug.ml
Ocamlc   src/util/rc.mli
Ocamlopt src/util/pqueue.ml
Ocamlc   src/core/ty.mli
Ocamlc   src/parser/glob.mli
Ocamlc   src/driver/driver_parser.mli
Ocamlc   src/util/json_lexer.ml
Ocamlc   src/util/rc.ml
Coqc     lib/coq/HighOrd.v
Coqc     lib/coq/WellFounded.v
Coqc     lib/coq/int/Int.v
Coqc     lib/coq/bool/Bool.v
Coqc     lib/coq/real/Real.v
Coqc     lib/coq/list/List.v
Coqc     lib/coq/option/Option.v
Ocamlopt src/util/bigInt.ml
Ocamlopt src/util/wstdlib.ml
Ocamlopt src/util/json_lexer.ml
Ocamlopt src/util/loc.ml
Ocamlopt src/util/plugin.ml
Ocamlopt src/util/number.ml
Ocamlopt src/core/ident.ml
Ocamlc   src/core/term.mli
Ocamlopt src/session/xml.ml
Ocamlc   src/core/ty.ml
Ocamlc   src/core/term.ml
Ocamlc   src/driver/driver_parser.ml
Ocamlc   src/parser/glob.ml
Coqc     lib/coq/list/Mem.v
Coqc     lib/coq/list/HdTl.v
Coqc     lib/coq/list/HdTlNoOpt.v
Coqc     lib/coq/list/Combine.v
Ocamlopt src/util/lexlib.ml
Ocamlopt src/util/rc.ml
Ocamlopt src/util/constant.ml
Ocamlopt src/core/ty.ml
Ocamlc   src/core/pattern.mli
Ocamlc   src/core/decl.mli
Ocamlc   src/core/coercion.mli
Ocamlopt src/core/parser_tokens.ml
Ocamlc   src/mlw/ity.mli
File "./lib/coq/real/Real.v", line 208, 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 208, 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 208, 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 208, 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 208, 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]
Ocamlc   src/core/dterm.mli
Ocamlopt src/driver/driver_parser.ml
Ocamlopt src/driver/smtv2_model_defs.ml
Ocamlopt src/parser/glob.ml
Ocamlc   src/transform/close_epsilon.mli
Ocamlc   src/printer/cntexmp_printer.mli
Ocamlc   src/core/pattern.ml
Ocamlc   src/core/decl.ml
Ocamlc   src/core/coercion.ml
Ocamlc   src/printer/cntexmp_printer.ml
Coqc     lib/coq/int/Exponentiation.v
Coqc     lib/coq/int/MinMax.v
Coqc     lib/coq/int/Abs.v
Coqc     lib/coq/int/NumOf.v
Coqc     lib/coq/real/Abs.v
Coqc     lib/coq/real/ExpLog.v
Coqc     lib/coq/real/FromInt.v
Coqc     lib/coq/real/MinMax.v
Coqc     lib/coq/real/RealInfix.v
Coqc     lib/coq/real/Square.v
Coqc     lib/coq/map/Map.v
Coqc     lib/coq/map/MapExt.v
Coqc     lib/coq/list/Length.v
Coqc     lib/coq/list/Nth.v
Coqc     lib/coq/list/NthNoOpt.v
Coqc     lib/coq/bv/Pow2int.v
Ocamlopt src/core/term.ml
Ocamlc   src/core/theory.mli
Ocamlc   src/mlw/expr.mli
Ocamlc   src/core/env.mli
Ocamlc   src/core/task.mli
Ocamlc   src/transform/detect_polymorphism.mli
Ocamlc   src/transform/eliminate_literal.mli
Ocamlc   src/session/termcode.mli
Ocamlc   src/core/theory.ml
Ocamlc   src/core/task.ml
Ocamlc   src/core/env.ml
Coqc     lib/coq/int/ComputerDivision.v
Coqc     lib/coq/int/EuclideanDivision.v
Coqc     lib/coq/int/Power.v
Coqc     lib/coq/real/PowerInt.v
Coqc     lib/coq/real/Trigonometry.v
Coqc     lib/coq/list/NthHdTl.v
Coqc     lib/coq/list/Append.v
File "./lib/coq/int/EuclideanDivision.v", line 25, 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 25, 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/list/Append.v", line 64, 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 64, 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 64, 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]
Ocamlopt src/core/pattern.ml
Ocamlopt src/core/coercion.ml
Ocamlc   src/parser/ptree.ml
Ocamlc   src/mlw/pdecl.mli
Ocamlc   src/core/pretty.mli
Ocamlc   src/core/trans.mli
Ocamlc   src/driver/whyconf.mli
Ocamlc   src/parser/ptree_helpers.mli
Ocamlc   src/parser/mlw_printer.mli
Ocamlc   src/transform/reduction_engine.mli
Ocamlc   src/transform/compute.mli
Ocamlc   src/transform/eliminate_definition.mli
Ocamlc   src/transform/eliminate_inductive.mli
Ocamlc   src/transform/eliminate_let.mli
Ocamlc   src/transform/eliminate_if.mli
Ocamlc   src/transform/libencoding.mli
Ocamlc   src/transform/eliminate_algebraic.mli
Ocamlc   src/transform/encoding.mli
Ocamlc   src/transform/abstraction.mli
Ocamlc   src/transform/eliminate_epsilon.mli
Ocamlc   src/transform/smoke_detector.mli
Ocamlc   src/transform/generic_arg_trans_utils.mli
Ocamlc   src/transform/apply.mli
Ocamlc   src/transform/subst.mli
Ocamlc   src/transform/introduction.mli
Ocamlc   src/transform/destruct.mli
Ocamlc   src/transform/cut.mli
Ocamlc   src/transform/reflection.mli
Ocamlc   src/session/strategy.mli
Ocamlc   src/core/dterm.ml
Ocamlc   src/parser/mlw_printer.ml
Ocamlc   src/mlw/expr.ml
Ocamlc   src/mlw/pdecl.ml
Ocamlc   src/mlw/ity.ml
Ocamlc   src/driver/whyconf.ml
Ocamlc   src/core/trans.ml
Ocamlc   src/transform/reduction_engine.ml
Ocamlc   src/transform/remove_unused.ml
Ocamlc   src/transform/detect_polymorphism.ml
Ocamlc   src/transform/extensional.ml
Ocamlc   src/transform/abstract_quantifiers.ml
Ocamlc   src/transform/eliminate_symbol.ml
Ocamlc   src/transform/eliminate_let.ml
Ocamlc   src/transform/eliminate_if.ml
Ocamlc   src/transform/libencoding.ml
Ocamlc   src/transform/encoding.ml
Ocamlc   src/transform/simplify_array.ml
Ocamlc   src/transform/abstraction.ml
Ocamlc   src/transform/close_epsilon.ml
Ocamlc   src/transform/lift_epsilon.ml
Ocamlc   src/transform/eliminate_epsilon.ml
Ocamlc   src/transform/instantiate_predicate.ml
Ocamlc   src/transform/eliminate_literal.ml
Ocamlc   src/transform/prop_curry.ml
Ocamlc   src/transform/smoke_detector.ml
Ocamlc   src/transform/generic_arg_trans_utils.ml
Ocamlc   src/transform/congruence.ml
Ocamlc   src/transform/keep_only_arithmetic.ml
Ocamlc   src/session/termcode.ml
Ocamlc   src/session/strategy.ml
Coqc     lib/coq/int/Div2.v
Coqc     lib/coq/real/PowerReal.v
Coqc     lib/coq/number/Parity.v
Coqc     lib/coq/map/Const.v
Coqc     lib/coq/map/Occ.v
Coqc     lib/coq/list/NthLength.v
Coqc     lib/coq/list/Reverse.v
Coqc     lib/coq/list/Distinct.v
Coqc     lib/coq/bv/BV_Gen.v
Coqc     lib/coq/for_drivers/ComputerOfEuclideanDivision.v
File "./lib/coq/list/Reverse.v", line 99, characters 12-27:
Warning: Notation List.rev_length is deprecated since 8.20.
Use 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 99, characters 12-27:
Warning: Notation List.rev_length is deprecated since 8.20.
Use 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 99, characters 12-27:
Warning: Notation List.rev_length is deprecated since 8.20.
Use length_rev instead.
[deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
Ocamlopt src/core/decl.ml
Ocamlc   src/mlw/pmodule.mli
Ocamlc   src/core/printer.mli
File "./lib/coq/map/Occ.v", line 248, 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 248, 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 248, 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]
Ocamlc   src/driver/driver_lexer.mli
Ocamlc   src/driver/autodetection.mli
Ocamlc   src/mlw/eval_match.mli
Ocamlc   src/mlw/typeinv.mli
Ocamlc   src/mlw/vc.mli
Ocamlc   src/mlw/dexpr.mli
Ocamlc   src/mlw/pinterp_core.mli
Ocamlc   src/extract/mltree.mli
Ocamlc   src/extract/mlinterp.mli
Ocamlc   src/parser/typing.mli
Ocamlc   src/parser/lexer.mli
Ocamlc   src/parser/sexp_parser.mli
Ocamlc   src/transform/simplify_formula.mli
Ocamlc   src/transform/inlining.mli
Ocamlc   src/transform/split_goal.mli
Ocamlc   src/transform/args_wrapper.mli
Ocamlc   src/transform/discriminate.mli
Ocamlc   src/session/strategy_parser.mli
Ocamlc   src/core/printer.ml
Ocamlc   src/driver/driver_lexer.ml
Ocamlc   src/driver/autodetection.ml
Ocamlc   src/mlw/eval_match.ml
Ocamlc   src/mlw/typeinv.ml
Ocamlc   src/mlw/vc.ml
Ocamlc   src/mlw/pmodule.ml
Ocamlc   src/mlw/dexpr.ml
Ocamlc   src/mlw/pinterp_core.ml
Ocamlc   src/extract/mltree.ml
Ocamlc   src/parser/ptree_helpers.ml
Ocamlc   src/parser/typing.ml
Ocamlc   src/parser/sexp_parser.ml
Ocamlc   src/transform/simplify_formula.ml
File "./lib/coq/bv/BV_Gen.v", line 49, characters 0-28:
Warning: Library File Coq.Bool.Bvector is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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/bv/BV_Gen.v", line 53, 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 53, 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]
Ocamlc   src/transform/split_goal.ml
Ocamlc   src/transform/args_wrapper.ml
Ocamlc   src/transform/compute.ml
Ocamlc   src/transform/eliminate_unknown_types.ml
Ocamlc   src/transform/eliminate_unknown_lsymbols.ml
Ocamlc   src/transform/eliminate_inductive.ml
Ocamlc   src/transform/eliminate_algebraic.ml
Ocamlc   src/transform/discriminate.ml
Ocamlc   src/transform/encoding_select.ml
Ocamlc   src/transform/encoding_guards_full.ml
Ocamlc   src/transform/encoding_tags_full.ml
Ocamlc   src/transform/encoding_guards.ml
Ocamlc   src/transform/encoding_tags.ml
Ocamlc   src/transform/encoding_twin.ml
Ocamlc   src/transform/encoding_sort.ml
Ocamlc   src/transform/filter_trigger.ml
Ocamlc   src/transform/case.ml
Ocamlc   src/transform/apply.ml
Ocamlc   src/transform/subst.ml
File "./lib/coq/bv/BV_Gen.v", line 339, characters 20-33:
Warning: Reference BshiftRl_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 339, characters 20-33:
Warning: Reference BshiftRl_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 345, characters 12-25:
Warning: Reference BshiftRl_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 8-21:
Warning: Reference BshiftRl_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 351, characters 9-17:
Warning: Reference BshiftRl is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 351, characters 19-24:
Warning: Reference Bhigh is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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]
Ocamlc   src/transform/introduction.ml
File "./lib/coq/bv/BV_Gen.v", line 390, characters 20-33:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 390, characters 20-33:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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]
Ocamlc   src/transform/destruct.ml
File "./lib/coq/bv/BV_Gen.v", line 448, characters 12-25:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 8-21:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 454, characters 9-17:
Warning: Reference BshiftRa is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 454, characters 19-24:
Warning: Reference Bhigh is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
[deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
File "./lib/coq/bv/BV_Gen.v", line 477, characters 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]
Ocamlc   src/transform/cut.ml
File "./lib/coq/bv/BV_Gen.v", line 477, characters 74-87:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 480, characters 16-24:
Warning: Reference BshiftRa is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 480, characters 26-31:
Warning: Reference Bhigh is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 487, characters 43-56:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 490, characters 8-21:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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]
Ocamlc   src/transform/reflection.ml
File "./lib/coq/bv/BV_Gen.v", line 495, characters 8-21:
Warning: Reference BshiftRa_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 496, characters 9-17:
Warning: Reference BshiftRa is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 496, characters 19-24:
Warning: Reference Bhigh is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 530, characters 20-32:
Warning: Reference BshiftL_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 530, characters 20-32:
Warning: Reference BshiftL_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 533, characters 134-146:
Warning: Reference BshiftL_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 567, characters 62-74:
Warning: Reference BshiftL_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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]
Ocamlc   src/printer/smtv1.ml
File "./lib/coq/bv/BV_Gen.v", line 602, 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 613, 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 616, characters 13-18:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 616, characters 13-18:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 624, 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 625, 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 626, characters 11-15:
Warning: Reference Bnil is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 628, characters 6-11:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 635, characters 9-14:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.
[deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default]
File "./lib/coq/bv/BV_Gen.v", line 639, characters 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 641, 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]
Ocamlc   src/printer/coq.ml
Ocamlc   src/printer/pvs.ml
File "./lib/coq/bv/BV_Gen.v", line 737, characters 42-47:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 751, characters 42-47:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 758, 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 767, characters 12-17:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 24-29:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 12-17:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 24-29:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 44-49:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 769, characters 15-20:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 782, characters 15-20:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 799, characters 13-18:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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]
Ocamlc   src/printer/isabelle.ml
Ocamlc   src/printer/simplify.ml
Ocamlc   src/printer/gappa.ml
File "./lib/coq/bv/BV_Gen.v", line 868, characters 22-27:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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]
Ocamlc   src/printer/cvc3.ml
File "./lib/coq/bv/BV_Gen.v", line 998, 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]
Ocamlc   src/printer/yices.ml
Ocamlc   src/printer/mathematica.ml
Ocamlc   src/session/strategy_parser.ml
File "./lib/coq/bv/BV_Gen.v", line 1217, characters 21-26:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1217, characters 21-26:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1251, characters 12-17:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1251, characters 12-17:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1253, characters 15-20:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1260, characters 12-17:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1260, characters 12-17:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1262, characters 15-20:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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/Divisibility.v
Coqc     lib/coq/map/MapPermut.v
Coqc     lib/coq/set/Set.v
File "./lib/coq/bv/BV_Gen.v", line 1345, characters 8-21:
Warning: Reference BshiftRl_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1346, characters 9-17:
Warning: Reference BshiftRl is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1346, characters 19-24:
Warning: Reference Bhigh is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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
File "./lib/coq/bv/BV_Gen.v", line 1393, characters 9-16:
Warning: Reference BshiftL is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1393, characters 18-23:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1394, characters 8-20:
Warning: Reference BshiftL_iter is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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/list/NthLengthAppend.v
Coqc     lib/coq/list/RevAppend.v
File "./lib/coq/bv/BV_Gen.v", line 1640, characters 9-14:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1688, characters 9-14:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1698, characters 24-29:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 1708, characters 37-42:
Warning: Reference Bsign is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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/list/NumOcc.v
File "./lib/coq/bv/BV_Gen.v", line 2347, characters 12-17:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 2347, characters 12-17:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 2355, characters 12-17:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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 2355, characters 12-17:
Warning: Reference Bcons is deprecated since 8.20.
Consider [list bool] instead. See <https://github.com/coq/coq/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]
Ocamlopt src/core/theory.ml
File "./lib/coq/set/Set.v", line 45, 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/number/Divisibility.v", line 207, 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 207, 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/set/Set.v", line 142, 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]
Ocamlc   src/parser/parser.mli
Ocamlopt src/core/task.ml
Ocamlopt src/core/env.ml
Ocamlc   src/core/model_parser.mli
Ocamlc   src/extract/compile.mli
Ocamlc   src/extract/pdriver.mli
Ocamlc   src/parser/report.mli
File "./lib/coq/set/Set.v", line 336, 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 336, 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 349, 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 349, 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]
Ocamlopt src/transform/reduction_engine.ml
Ocamlc   src/transform/ind_itp.mli
Ocamlc   src/core/model_parser.ml
Ocamlc   src/driver/smtv2_model_parser.ml
Ocamlc   src/extract/compile.ml
Ocamlc   src/extract/mlinterp.ml
Ocamlc   src/extract/c.ml
Ocamlc   src/extract/java.ml
Ocamlc   src/parser/parser.ml
Ocamlc   src/parser/report.ml
Ocamlc   src/transform/ind_itp.ml
Ocamlc   src/transform/induction.ml
Ocamlc   src/transform/induction_pr.ml
Coqc     lib/coq/number/Gcd.v
Coqc     lib/coq/number/Prime.v
Coqc     lib/coq/set/Cardinal.v
Coqc     lib/coq/list/Permut.v
Ocamlc   src/core/keywords.mli
Ocamlopt src/driver/whyconf.ml
Ocamlc   src/driver/call_provers.mli
Ocamlopt src/driver/driver_lexer.ml
Ocamlc   src/driver/driver.mli
Ocamlopt src/driver/autodetection.ml
Ocamlc   src/mlw/rac.mli
Ocamlc   src/mlw/pinterp.mli
Ocamlc   src/extract/ml_printer.mli
Ocamlc   src/session/session_itp.mli
Ocamlc   src/core/keywords.ml
Ocamlc   src/driver/call_provers.ml
Ocamlc   src/core/pretty.ml
Ocamlc   src/driver/driver.ml
File "./lib/coq/number/Prime.v", line 37, 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 37, 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]
Ocamlc   src/mlw/rac.ml
Ocamlc   src/mlw/pinterp.ml
File "./lib/coq/number/Gcd.v", line 135, characters 6-24:
Warning: Notation Zis_gcd_for_euclid is deprecated since 8.17.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./lib/coq/number/Gcd.v", line 135, characters 6-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]
Ocamlc   src/extract/pdriver.ml
Ocamlc   src/extract/ml_printer.ml
Ocamlc   src/extract/ocaml.ml
Ocamlc   src/extract/cakeml.ml
Ocamlc   src/parser/lexer.ml
Ocamlc   src/transform/inlining.ml
Ocamlc   src/transform/eliminate_definition.ml
Ocamlc   src/transform/prepare_for_counterexmp.ml
Ocamlc   src/printer/alt_ergo.ml
Ocamlc   src/printer/why3printer.ml
Ocamlc   src/printer/smtv2.ml
Ocamlc   src/session/session_itp.ml
Coqc     lib/coq/number/Coprime.v
Ocamlopt src/core/keywords.ml
Ocamlc   src/mlw/check_ce.mli
Ocamlc   src/session/controller_itp.mli
Ocamlopt src/core/pretty.ml
Ocamlc   src/mlw/check_ce.ml
Ocamlc   src/session/itp_communication.mli
Ocamlc   src/session/controller_itp.ml
Ocamlc   src/session/server_utils.mli
Ocamlc   src/session/itp_server.mli
Ocamlc   src/session/json_util.mli
Ocamlc   src/session/server_utils.ml
Ocamlc   src/session/itp_communication.ml
Ocamlc   src/session/itp_server.ml
Ocamlc   src/session/json_util.ml
Ocamlopt src/core/trans.ml
Ocamlopt src/core/dterm.ml
Ocamlopt src/mlw/ity.ml
Linking  lib/why3/why3.cmo
Ocamlopt src/transform/simplify_formula.ml
Ocamlopt src/core/printer.ml
Ocamlopt src/transform/detect_polymorphism.ml
Ocamlopt src/transform/extensional.ml
Ocamlopt src/transform/abstract_quantifiers.ml
Ocamlopt src/transform/eliminate_symbol.ml
Ocamlopt src/transform/eliminate_inductive.ml
Ocamlopt src/transform/eliminate_let.ml
File "./lib/coq/set/Cardinal.v", line 169, 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 170, 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 171, 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]
Ocamlopt src/transform/eliminate_if.ml
File "./lib/coq/set/Cardinal.v", line 188, 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 193, 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]
Ocamlopt src/transform/libencoding.ml
Ocamlopt src/transform/simplify_array.ml
Ocamlopt src/transform/filter_trigger.ml
Ocamlopt src/transform/abstraction.ml
Ocamlopt src/transform/close_epsilon.ml
Ocamlopt src/transform/eliminate_epsilon.ml
Ocamlopt src/transform/instantiate_predicate.ml
File "./lib/coq/set/Cardinal.v", line 447, 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]
Ocamlopt src/transform/smoke_detector.ml
Ocamlopt src/transform/prop_curry.ml
File "./lib/coq/set/Cardinal.v", line 475, 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]
Ocamlopt src/transform/generic_arg_trans_utils.ml
Ocamlopt src/transform/congruence.ml
Ocamlopt src/transform/keep_only_arithmetic.ml
Ocamlopt src/printer/cntexmp_printer.ml
File "./lib/coq/set/Cardinal.v", line 604, characters 26-41:
Warning: Notation List.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/set/Cardinal.v", line 604, characters 26-41:
Warning: Notation List.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/set/Cardinal.v", line 604, characters 26-41:
Warning: Notation List.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/set/Cardinal.v", line 605, characters 23-38:
Warning: Notation List.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/set/Cardinal.v", line 605, characters 23-38:
Warning: Notation List.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/set/Cardinal.v", line 605, characters 23-38:
Warning: Notation List.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]
Ocamlopt src/printer/coq.ml
Ocamlopt src/printer/pvs.ml
Ocamlopt src/printer/isabelle.ml
Ocamlopt src/printer/mathematica.ml
Ocamlopt src/session/strategy.ml
Ocamlopt src/session/termcode.ml
Ocamlopt src/mlw/expr.ml
File "./lib/coq/set/Cardinal.v", line 623, characters 26-41:
Warning: Notation List.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/set/Cardinal.v", line 623, characters 26-41:
Warning: Notation List.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/set/Cardinal.v", line 623, characters 26-41:
Warning: Notation List.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/set/Cardinal.v", line 623, characters 65-80:
Warning: Notation List.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/set/Cardinal.v", line 623, characters 65-80:
Warning: Notation List.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/set/Cardinal.v", line 623, characters 65-80:
Warning: Notation List.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]
Ocamlopt src/transform/eliminate_unknown_types.ml
Ocamlopt src/transform/eliminate_unknown_lsymbols.ml
Ocamlopt src/transform/eliminate_algebraic.ml
File "./lib/coq/set/Cardinal.v", line 740, characters 8-23:
Warning: Notation List.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/set/Cardinal.v", line 740, characters 8-23:
Warning: Notation List.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/set/Cardinal.v", line 740, characters 8-23:
Warning: Notation List.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]
Ocamlopt src/transform/encoding.ml
File "./lib/coq/set/Cardinal.v", line 821, characters 12-27:
Warning: Notation List.map_length is deprecated since 8.20.
Use 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 821, characters 12-27:
Warning: Notation List.map_length is deprecated since 8.20.
Use 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 821, characters 12-27:
Warning: Notation List.map_length is deprecated since 8.20.
Use length_map instead.
[deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
Ocamlopt src/transform/lift_epsilon.ml
File "./lib/coq/set/Cardinal.v", line 846, characters 24-40:
Warning: Notation List.prod_length is deprecated since 8.20.
Use 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 846, characters 24-40:
Warning: Notation List.prod_length is deprecated since 8.20.
Use 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 846, characters 24-40:
Warning: Notation List.prod_length is deprecated since 8.20.
Use length_prod instead.
[deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
Ocamlopt src/transform/eliminate_literal.ml
Ocamlopt src/session/strategy_parser.ml
Ocamlc   plugins/tptp/tptp_ast.mli
Ocamlc   plugins/python/py_ast.mli
Ocamlc   plugins/microc/mc_ast.mli
Ocamlc   plugins/microc/mc_printer.mli
Ocamlc   plugins/coma/coma_logic.mli
Ocamlc   plugins/cfg/cfg_ast.mli
Ocamlc   plugins/cfg/subregion_analysis.mli
Ocamlc   src/ide/gconfig.mli
Ocamlc   src/why3session/why3session_lib.mli
Ocamlc   src/why3doc/doc_def.mli
Coqc     lib/coq/set/Fset.v
Ocamlopt src/core/model_parser.ml
Ocamlopt src/mlw/pdecl.ml
Ocamlopt src/parser/ptree.ml
Ocamlopt src/transform/encoding_guards_full.ml
Ocamlopt src/transform/encoding_tags_full.ml
Ocamlopt src/transform/encoding_guards.ml
Ocamlopt src/transform/encoding_tags.ml
Ocamlopt src/transform/encoding_twin.ml
Ocamlopt src/transform/encoding_sort.ml
Ocamlc   plugins/tptp/tptp_parser.mli
Ocamlc   plugins/tptp/tptp_typing.mli
Ocamlc   plugins/python/py_parser.mli
Ocamlc   plugins/tptp/tptp_lexer.mli
Ocamlc   plugins/microc/mc_parser.mli
Ocamlc   plugins/python/py_lexer.mli
Ocamlc   plugins/microc/mc_lexer.mli
Ocamlc   plugins/coma/coma_syntax.mli
Ocamlc   plugins/cfg/cfg_parser.mli
Ocamlc   plugins/cfg/cfg_lexer.mli
Ocamlc   plugins/cfg/cfg_paths.mli
Ocamlc   plugins/cfg/cfg_main.mli
Ocamlc   plugins/cfg/stackify.mli
Ocamlc   src/why3session/why3session_info.mli
Ocamlc   src/why3session/why3session_html.mli
Ocamlc   src/why3session/why3session_latex.mli
Ocamlc   src/why3session/why3session_update.mli
Ocamlc   src/why3session/why3session_create.mli
Ocamlc   src/why3session/why3session_output.mli
Ocamlopt src/driver/call_provers.ml
Ocamlopt src/driver/smtv2_model_parser.ml
Ocamlopt src/mlw/eval_match.ml
Ocamlopt src/transform/split_goal.ml
Ocamlopt src/transform/remove_unused.ml
Ocamlc   plugins/coma/coma_parser.mli
Ocamlc   plugins/coma/coma_lexer.mli
Ocamlc   plugins/coma/coma_typing.mli
Ocamlopt src/driver/driver.ml
Ocamlopt src/mlw/typeinv.ml
Ocamlopt src/transform/inlining.ml
Ocamlopt src/mlw/vc.ml
File "./lib/coq/set/Fset.v", line 106, 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 112, 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 121, 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 166, 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 166, 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]
Ocamlopt src/mlw/pmodule.ml
Coqc     lib/coq/set/FsetInt.v
Coqc     lib/coq/set/FsetSum.v
Coqc     lib/coq/set/SetApp.v
Coqc     lib/coq/set/FsetInduction.v
Coqc     lib/coq/set/SetImp.v
Ocamlopt src/mlw/pinterp_core.ml
Ocamlopt src/mlw/dexpr.ml
Ocamlopt src/parser/ptree_helpers.ml
Ocamlopt src/parser/mlw_printer.ml
File "./lib/coq/set/SetImp.v", line 57, 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]
Ocamlopt src/mlw/pinterp.ml
Ocamlopt src/mlw/rac.ml
Ocamlopt src/extract/mltree.ml
File "./lib/coq/set/FsetInt.v", line 131, 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]
Ocamlopt src/parser/typing.ml
File "./lib/coq/set/FsetInt.v", line 132, 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 187, 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 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 189, 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 189, 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 219, 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 219, 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 219, 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 234, 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 234, 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 234, 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 234, 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 234, 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 236, 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 236, 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 236, 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 269, 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 269, 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]
Coqc     lib/coq/set/SetAppInt.v
Coqc     lib/coq/set/SetImpInt.v
Ocamlopt src/extract/compile.ml
Ocamlopt src/extract/pdriver.ml
Ocamlopt src/extract/ml_printer.ml
Ocamlopt src/extract/java.ml
Ocamlopt src/mlw/check_ce.ml
Ocamlopt src/parser/parser.ml
Ocamlopt src/parser/sexp_parser.ml
Ocamlopt src/extract/ocaml.ml
Ocamlopt src/extract/cakeml.ml
Ocamlopt src/extract/mlinterp.ml
Ocamlopt src/extract/c.ml
File "./lib/coq/set/SetImpInt.v", line 52, 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 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]
File "./lib/coq/set/FsetSum.v", line 106, 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 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 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 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 120, 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 126, 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 126, 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 126, 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 129, 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 129, 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 129, 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 181, 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 181, 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 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 185, 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 214, 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 214, 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 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 218, 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 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/FsetSum.v", line 317, 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]
Ocamlopt src/parser/report.ml
Ocamlopt src/parser/lexer.ml
Ocamlopt src/transform/args_wrapper.ml
Ocamlopt src/transform/case.ml
Ocamlopt src/transform/compute.ml
Ocamlopt src/transform/subst.ml
Ocamlopt src/transform/ind_itp.ml
Ocamlopt src/transform/cut.ml
Ocamlopt src/transform/apply.ml
Ocamlopt src/transform/eliminate_definition.ml
Ocamlopt src/transform/discriminate.ml
Ocamlopt src/printer/gappa.ml
Ocamlopt src/transform/introduction.ml
Ocamlopt src/transform/destruct.ml
Ocamlopt src/transform/induction.ml
Ocamlopt src/transform/induction_pr.ml
Ocamlopt src/transform/reflection.ml
Ocamlopt src/transform/prepare_for_counterexmp.ml
Ocamlopt src/printer/alt_ergo.ml
Ocamlopt src/transform/encoding_select.ml
Ocamlopt src/printer/why3printer.ml
Ocamlopt src/printer/smtv1.ml
Ocamlopt src/printer/smtv2.ml
Ocamlopt src/printer/simplify.ml
Ocamlopt src/printer/cvc3.ml
Ocamlopt src/printer/yices.ml
Ocamlopt src/session/session_itp.ml
Ocamlopt src/session/controller_itp.ml
Ocamlopt src/session/itp_communication.ml
Ocamlopt src/session/server_utils.ml
Ocamlopt src/session/json_util.ml
Ocamlopt src/session/itp_server.ml
Linking  lib/why3/why3.cmx
Ocamlopt plugins/parser/genequlin.ml
Ocamlopt plugins/tptp/tptp_parser.ml
Ocamlopt plugins/python/py_parser.ml
Ocamlopt plugins/tptp/tptp_printer.ml
Ocamlopt plugins/tptp/tptp_typing.ml
Ocamlopt plugins/parser/dimacs.ml
Ocamlopt plugins/microc/mc_parser.ml
Ocamlopt plugins/microc/mc_printer.ml
Ocamlopt plugins/coma/coma_logic.ml
Ocamlopt plugins/cfg/cfg_parser.ml
Ocamlopt plugins/cfg/cfg_paths.ml
Ocamlopt plugins/cfg/subregion_analysis.ml
Ocamlopt plugins/cfg/stackify.ml
Ocamlopt plugins/strategies/forward_propagation.ml
Ocamlopt plugins/transform/hypothesis_selection.ml
Linking  lib/why3/why3.cmxa
Linking  lib/why3/why3.cmxs
Ocamlopt src/tools/main.ml
Ocamlopt src/tools/why3config.ml
Ocamlopt src/tools/why3execute.ml
Ocamlopt src/tools/why3extract.ml
Ocamlopt src/tools/why3prove.ml
Ocamlopt src/tools/why3realize.ml
Ocamlopt src/tools/why3replay.ml
Ocamlopt src/tools/why3show.ml
Ocamlopt src/tools/why3bench.ml
Ocamlopt src/tools/why3wc.ml
Ocamlopt src/ide/gconfig.ml
Ocamlopt src/ide/wserver.ml
Ocamlopt src/why3session/why3session_lib.ml
Ocamlopt src/tools/why3shell.ml
Ocamlopt src/isabelle-client/isabelle_client_main.ml
Ocamlopt src/tools/why3pp.ml
Ocamlopt src/why3doc/doc_html.ml
Ocamlopt src/why3doc/doc_def.ml
Linking  lib/plugins/genequlin.cmxs
Linking  lib/plugins/dimacs.cmxs
Ocamlopt plugins/tptp/tptp_lexer.ml
Ocamlopt plugins/python/py_lexer.ml
Ocamlopt plugins/microc/mc_lexer.ml
Ocamlopt plugins/coma/coma_syntax.ml
Linking  lib/plugins/forward_propagation.cmxs
Linking  lib/plugins/hypothesis_selection.cmxs
Linking  bin/why3.opt
Linking  bin/why3config.cmxs
Linking  bin/why3execute.cmxs
Linking  bin/why3extract.cmxs
Linking  bin/why3prove.cmxs
Linking  bin/why3realize.cmxs
Linking  bin/why3replay.cmxs
Linking  bin/why3show.cmxs
Linking  bin/why3wc.cmxs
Linking  bin/why3bench.cmxs
Ocamlopt src/ide/why3ide.ml
Ocamlopt src/ide/why3web.ml
Ocamlopt src/why3session/why3session_info.ml
Ocamlopt src/why3session/why3session_html.ml
Ocamlopt src/why3session/why3session_latex.ml
Ocamlopt src/why3session/why3session_update.ml
Ocamlopt src/why3session/why3session_output.ml
Ocamlopt src/why3session/why3session_create.ml
Linking  bin/why3shell.cmxs
Linking  bin/isabelle_client.opt
Linking  bin/why3pp.cmxs
Ocamlopt src/why3doc/doc_lexer.ml
Linking  lib/plugins/tptp.cmxs
Ocamlopt plugins/python/py_main.ml
Ocamlopt plugins/microc/mc_main.ml
Ocamlopt plugins/coma/coma_parser.ml
Ocamlopt plugins/coma/coma_typing.ml
Linking  bin/why3webserver.cmxs
Ocamlopt src/why3session/why3session_main.ml
Ocamlopt src/why3doc/doc_main.ml
Linking  lib/plugins/microc.cmxs
Linking  bin/why3session.cmxs
Linking  bin/why3doc.cmxs
Linking  lib/plugins/python.cmxs
Linking  bin/why3ide.cmxs
ld: warning: libfontconfig.so.2, needed by /pbulk/work/devel/why3/work/.buildlink/lib/libcairo.so, may conflict with libfontconfig.so.1
ld: warning: libfreetype.so.19, needed by /usr/X11R7/lib/libfontconfig.so.2, may conflict with libfreetype.so.6
Ocamlopt plugins/cfg/cfg_lexer.ml
Ocamlopt plugins/cfg/cfg_main.ml
Ocamlopt plugins/cfg/cfg_stackify.ml
Linking  lib/plugins/cfg.cmxs
Ocamlopt plugins/coma/coma_lexer.ml
Ocamlopt plugins/coma/coma_main.ml
Linking  lib/plugins/coma.cmxs