=> 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 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings Ocamllex src/util/json_lexer.mll 52 states, 495 transitions, table size 2292 bytes Ocamllex src/parser/lexer.mll Menhir src/parser/parser_common.mly Menhir src/parser/parser_common.mly src/parser/parser.mly 174 states, 4831 transitions, table size 20368 bytes 9859 additional bytes used for bindings Menhir src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 34 states, 1366 transitions, table size 5668 bytes Ocamllex src/driver/sexp.mll 33 states, 370 transitions, table size 1678 bytes Ocamllex src/session/xml.mll Ocamllex src/session/strategy_parser.mll 59 states, 799 transitions, table size 3550 bytes 2611 additional bytes used for bindings 117 states, 1396 transitions, table size 6286 bytes 3556 additional bytes used for bindings cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml Ocamllex plugins/tptp/tptp_lexer.mll Menhir plugins/tptp/tptp_parser.mly 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings Ocamllex plugins/coma/coma_lexer.mll Menhir src/parser/parser_common.mly plugins/coma/coma_parser.mly 251 states, 6731 transitions, table size 28430 bytes 16559 additional bytes used for bindings Read 3 sample input sentences and 3 error messages. menhir --explain --strict src/parser/parser_common.mly src/parser/parser.mly --base src/parser/parser --compile-errors \ src/parser/handcrafted.messages > src/parser/parser_messages.ml Ocamllex plugins/python/py_lexer.mll 69 states, 1256 transitions, table size 5438 bytes 1453 additional bytes used for bindings Menhir plugins/python/py_parser.mly Ocamllex plugins/microc/mc_lexer.mll 77 states, 473 transitions, table size 2354 bytes 1504 additional bytes used for bindings Menhir plugins/microc/mc_parser.mly Read 3 sample input sentences and 3 error messages. Ocamllex plugins/cfg/cfg_lexer.mll Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly 173 states, 4796 transitions, table size 20222 bytes 9853 additional bytes used for bindings Ocamllex plugins/parser/dimacs.mll 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings Ocamllex src/tools/why3wc.mll 307 states, 15627 transitions, table size 64350 bytes Ocamldep src/ide/gconfig.ml Ocamldep src/ide/ide_utils.ml Ocamldep src/ide/why3ide.ml Ocamldep src/ide/wserver.ml Ocamldep src/ide/why3web.ml Ocamldep src/why3session/why3session_lib.ml Ocamldep src/why3session/why3session_info.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 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/Fset.v Coqdep lib/coq/set/Cardinal.v Coqdep lib/coq/set/FsetInduction.v Coqdep lib/coq/set/FsetInt.v Coqdep lib/coq/set/FsetSum.v Coqdep lib/coq/set/SetAppInt.v Coqdep lib/coq/set/SetApp.v Coqdep lib/coq/set/SetImp.v Coqdep lib/coq/map/Map.v Coqdep lib/coq/set/SetImpInt.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/NthLengthAppend.v Coqdep lib/coq/list/Append.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/Distinct.v Coqdep lib/coq/list/Combine.v Coqdep lib/coq/list/NumOcc.v Coqdep lib/coq/list/Permut.v Coqdep lib/coq/option/Option.v Coqdep lib/coq/bv/BV_Gen.v Coqdep lib/coq/bv/Pow2int.v Coqdep lib/coq/for_drivers/ComputerOfEuclideanDivision.v Ocamldep src/isabelle-client/isabelle_client_main.ml Ocamldep src/tools/why3pp.ml cp src/util/json_base.ml src/trywhy3/json_base.ml cp src/util/json_base.mli src/trywhy3/json_base.mli Ocamllex src/why3doc/doc_lexer.mll 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 120 states, 706 transitions, table size 3544 bytes 1763 additional bytes used for bindings Ocamldep src/util/exn_printer.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/mysexplib.ml Ocamldep src/util/config.ml Ocamldep src/util/mlmpfr_wrapper.ml Ocamldep src/util/util.ml Ocamldep src/util/lists.ml Ocamldep src/util/opt.ml Ocamldep src/util/strings.ml Ocamldep src/util/pp.ml Ocamldep src/util/extset.ml Ocamldep src/util/extmap.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/hcpt.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/diffmap.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/getopt.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/json_base.ml Ocamldep src/util/debug.ml Ocamldep src/util/loc.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/rc.ml Ocamldep src/util/plugin.ml Ocamldep src/util/number.ml Ocamldep src/util/constant.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/vector.ml Ocamldep src/util/re.ml Ocamldep src/core/ident.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/theory.ml Ocamldep src/core/parser_tokens.ml Ocamldep src/core/keywords.ml Ocamldep src/core/task.ml Ocamldep src/core/pretty.ml Ocamldep src/core/env.ml Ocamldep src/core/dterm.ml Ocamldep src/core/trans.ml Ocamldep src/core/printer.ml Ocamldep src/core/model_parser.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/smtv2_model_defs.ml Ocamldep src/driver/sexp.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/pmodule.ml Ocamldep src/mlw/vc.ml Ocamldep src/mlw/dexpr.ml Ocamldep src/mlw/big_real.ml Ocamldep src/mlw/pinterp_core.ml Ocamldep src/mlw/rac.ml Ocamldep src/mlw/pinterp.ml Ocamldep src/mlw/check_ce.ml Ocamldep src/extract/mltree.ml Ocamldep src/extract/compile.ml Ocamldep src/extract/pdriver.ml Ocamldep src/extract/mlinterp.ml Ocamldep src/extract/ml_printer.ml Ocamldep src/extract/c.ml Ocamldep src/extract/ocaml.ml Ocamldep src/extract/java.ml Ocamldep src/extract/cakeml.ml Ocamldep src/parser/ptree.ml Ocamldep src/parser/ptree_helpers.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/parser/report.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/sexp_parser.ml Ocamldep src/parser/mlw_printer.ml Ocamldep src/parser/lexer.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/args_wrapper.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/abstract_quantifiers.ml Ocamldep src/transform/extensional.ml Ocamldep src/transform/eliminate_unknown_types.ml Ocamldep src/transform/eliminate_unknown_lsymbols.ml Ocamldep src/transform/eliminate_symbol.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/eliminate_let.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/libencoding.ml Ocamldep src/transform/discriminate.ml Ocamldep src/transform/encoding.ml Ocamldep src/transform/encoding_select.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_sort.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/close_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/cut.ml Ocamldep src/transform/congruence.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/smtv2.ml Ocamldep src/printer/coq.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/controller_itp.ml Ocamldep src/session/server_utils.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/json_util.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/driver/driver_ast.mli Ocamldep plugins/parser/genequlin.ml Ocamldep plugins/parser/dimacs.ml Ocamldep plugins/transform/hypothesis_selection.ml Ocamldep plugins/strategies/forward_propagation.ml Ocamldep plugins/tptp/tptp_parser.ml Ocamldep plugins/tptp/tptp_typing.ml Ocamldep plugins/tptp/tptp_lexer.ml Ocamldep plugins/tptp/tptp_printer.ml Ocamldep plugins/coma/coma_logic.ml Ocamldep plugins/coma/coma_syntax.ml Ocamldep plugins/coma/coma_parser.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/why3config.ml Ocamldep src/tools/main.ml Ocamldep src/tools/why3execute.ml Ocamldep src/tools/why3extract.ml Ocamldep src/tools/why3prove.ml Ocamldep src/tools/why3realize.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_html.ml Ocamldep src/why3doc/doc_main.ml Ocamldep src/why3doc/doc_def.ml Ocamldep src/why3doc/doc_lexer.ml Ocamldep src/trywhy3/json_base.ml Ocamldep src/trywhy3/json_parser.ml Ocamldep src/trywhy3/json_lexer.ml Ocamldep src/trywhy3/bindings.ml Ocamldep src/trywhy3/shortener.ml Ocamldep src/trywhy3/trywhy3.ml Ocamldep src/trywhy3/why3_worker.ml Ocamldep src/trywhy3/worker_proto.ml mkdir lib/plugins Ocamlc src/util/exn_printer.mli Ocamlc src/util/bigInt.mli Ocamlc src/util/config.mli Ocamlc src/util/mlmpfr_wrapper.mli Ocamlc src/util/util.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/getopt.mli Ocamlc src/util/json_base.mli Ocamlc src/util/hashcons.mli Ocamlc src/util/print_tree.mli Ocamlc src/util/cmdline.mli Ocamlc src/util/sysutil.mli Ocamlc src/util/lexlib.mli Ocamlc src/util/number.mli Ocamlc src/util/vector.mli Ocamlc src/util/pqueue.mli Ocamlc src/util/re.ml Ocamlc src/driver/prove_client.mli Ocamlc src/driver/smtv2_model_defs.mli File "src/util/re.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/driver/sexp.mli Ocamlc src/driver/smtv2_model_parser.mli Ocamlc src/mlw/big_real.mli Linking src/util/ppx_debug_optim findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/pkg/lib/ocaml, /usr/pkg/lib/ocaml/compiler-libs Ocamlc src/extract/c.mli Ocamlc src/extract/ocaml.mli Ocamlc src/extract/cakeml.mli Ocamlc src/extract/java.mli Ocamlc src/parser/parser_messages.mli Ocamlc src/transform/remove_unused.mli Ocamlc src/transform/eliminate_unknown_types.mli Ocamlc src/transform/extensional.mli Ocamlc src/transform/abstract_quantifiers.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_guards.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/simplify_array.mli Ocamlc src/transform/filter_trigger.mli Ocamlc src/transform/lift_epsilon.mli Ocamlc src/transform/instantiate_predicate.mli Ocamlc src/transform/prop_curry.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/transform/keep_only_arithmetic.mli Ocamlc src/printer/alt_ergo.mli Ocamlc src/printer/why3printer.mli Ocamlc src/printer/smtv1.mli Ocamlc src/printer/smtv2.mli Ocamlc src/printer/coq.mli Ocamlc src/printer/pvs.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/config.ml Ocamlc src/util/mlmpfr_wrapper.ml Ocamlc src/util/util.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 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/prove_client.ml Ocamlc src/driver/smtv2_model_defs.ml Ocamlc src/driver/sexp.ml Ocamlc src/mlw/big_real.ml Ocamlc src/parser/parser_messages.ml 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/cfg/cfg_stackify.mli Ocamlc plugins/strategies/forward_propagation.mli Ocamlc plugins/coma/coma_main.mli Ocamlc plugins/transform/hypothesis_selection.mli Ocamlc src/tools/why3execute.mli Ocamlc src/tools/main.mli Ocamlc src/tools/why3config.mli Ocamlc src/tools/why3extract.mli Ocamlc src/tools/why3prove.mli Ocamlc src/tools/why3replay.mli Ocamlc src/tools/why3realize.mli Ocamlc src/tools/why3show.mli Ocamlc src/tools/why3wc.mli Ocamlc src/tools/why3bench.mli Ocamlc src/ide/ide_utils.mli Ocamlc src/ide/why3ide.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/tools/why3pp.mli Ocamlc src/why3doc/doc_html.mli Ocamlc src/why3doc/doc_lexer.mli gcc -Wall -O -g -o src/server/logging.o -c src/server/logging.c gcc -Wall -O -g -o src/server/arraylist.o -c src/server/arraylist.c Ocamlc src/why3doc/doc_main.mli 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 Ocamlc src/util/mysexplib.ml Ocamlopt src/util/config.ml Ocamlopt src/util/mlmpfr_wrapper.ml Ocamlopt src/util/util.ml Ocamlopt src/util/opt.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 Ocamlopt src/util/print_tree.ml Ocamlc src/util/loc.mli Ocamlopt src/util/cmdline.ml Ocamlopt src/util/sysutil.ml Ocamlc src/util/rc.mli 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 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/core/parser_tokens.mli Ocamlopt src/driver/prove_client.ml Ocamlc src/driver/driver_ast.mli Ocamlopt src/mlw/big_real.ml Ocamlopt src/driver/sexp.ml Ocamlc src/parser/glob.mli Ocamlopt src/parser/parser_messages.ml Ocamlopt src/session/compress.ml Ocamlopt src/session/unix_scheduler.ml Ocamlc src/util/bigInt.ml Ocamlc src/util/extset.ml Ocamlc src/util/wstdlib.ml Ocamlc src/util/diffmap.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/rc.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/parser/glob.ml Ocamlc src/session/xml.ml Ocamlopt src/ide/ide_utils.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 Coqc lib/coq/WellFounded.v Coqc lib/coq/HighOrd.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/mysexplib.ml Ocamlopt src/util/extset.ml Ocamlopt src/util/diffmap.ml Ocamlopt src/util/wstdlib.ml Ocamlopt src/util/json_parser.ml Ocamlc src/util/json_lexer.mli Ocamlopt src/util/debug.ml Ocamlopt src/util/pqueue.ml 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/ty.mli Ocamlc src/driver/driver_parser.mli Ocamlopt src/session/xml.ml Ocamlc src/util/json_lexer.ml Ocamlc src/driver/driver_parser.ml Coqc lib/coq/int/Exponentiation.v Coqc lib/coq/int/Abs.v Coqc lib/coq/int/MinMax.v Coqc lib/coq/int/NumOf.v Coqc lib/coq/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/Mem.v Coqc lib/coq/list/Nth.v Coqc lib/coq/list/HdTl.v Coqc lib/coq/list/HdTlNoOpt.v Coqc lib/coq/list/NthNoOpt.v Coqc lib/coq/list/Combine.v Coqc lib/coq/bv/Pow2int.v Ocamlopt src/util/bigInt.ml Ocamlopt src/util/json_lexer.ml Ocamlopt src/util/loc.ml Ocamlopt src/util/plugin.ml Ocamlopt src/util/number.ml Ocamlc src/core/term.mli Ocamlc src/core/ty.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 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] Coqc lib/coq/real/Trigonometry.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/NthHdTl.v Coqc lib/coq/list/Append.v Coqc lib/coq/bv/BV_Gen.v 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] 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] Coqc lib/coq/for_drivers/ComputerOfEuclideanDivision.v Ocamlopt src/util/lexlib.ml Ocamlopt src/util/rc.ml Ocamlopt src/util/constant.ml Ocamlopt src/core/ident.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 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/core/pattern.mli Ocamlc src/core/decl.mli Ocamlc src/core/coercion.mli Ocamlopt src/core/parser_tokens.ml Ocamlc src/mlw/ity.mli Ocamlc src/core/dterm.mli Ocamlopt src/driver/driver_parser.ml Ocamlopt src/driver/smtv2_model_defs.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 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 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 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 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 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 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 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 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 448, characters 12-25: Warning: Reference BshiftRa_iter is deprecated since 8.20. Consider [list bool] instead. See 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 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 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 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] 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 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 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 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 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 for details. Please open an issue if you would like to keep using Bvector. [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default] File "./lib/coq/bv/BV_Gen.v", line 495, characters 8-21: Warning: Reference BshiftRa_iter is deprecated since 8.20. Consider [list bool] instead. See 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 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 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 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 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 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/parser/glob.ml Ocamlc src/transform/close_epsilon.mli Ocamlc src/printer/cntexmp_printer.mli 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 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/core/term.ml Ocamlc src/core/pattern.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 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 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 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 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 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/core/decl.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 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 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 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 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 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 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 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 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 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/core/coercion.ml 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 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/cntexmp_printer.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 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/int/Div2.v Coqc lib/coq/real/PowerReal.v Coqc lib/coq/number/Divisibility.v 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] 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 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 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 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 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 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 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 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 for details. Please open an issue if you would like to keep using Bvector. [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default] File "./lib/coq/bv/BV_Gen.v", line 1345, characters 8-21: Warning: Reference BshiftRl_iter is deprecated since 8.20. Consider [list bool] instead. See 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 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 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 9-16: Warning: Reference BshiftL is deprecated since 8.20. Consider [list bool] instead. See 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 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 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 1640, characters 9-14: Warning: Reference Bsign is deprecated since 8.20. Consider [list bool] instead. See 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/set/Set.v 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 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 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 for details. Please open an issue if you would like to keep using Bvector. [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default] File "./lib/coq/number/Divisibility.v", line 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] Coqc lib/coq/map/MapPermut.v Coqc lib/coq/map/MapInjection.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 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 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 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 for details. Please open an issue if you would like to keep using Bvector. [deprecated-reference-since-8.20,deprecated-since-8.20,deprecated-reference,deprecated,default] File "./lib/coq/set/Set.v", line 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/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] Coqc lib/coq/list/NthLengthAppend.v Coqc lib/coq/list/Reverse.v 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] Coqc lib/coq/list/Distinct.v 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/core/ty.ml Ocamlc src/core/theory.mli 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] Ocamlc src/mlw/expr.mli Ocamlc src/core/env.mli Ocamlc src/core/task.mli Ocamlc src/driver/whyconf.mli Ocamlc src/transform/reduction_engine.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 Ocamlc src/driver/whyconf.ml Ocamlc src/transform/reduction_engine.ml Coqc lib/coq/set/Cardinal.v Coqc lib/coq/number/Prime.v Coqc lib/coq/number/Gcd.v 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] 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] Coqc lib/coq/list/RevAppend.v Coqc lib/coq/list/NumOcc.v Ocamlopt src/core/term.ml Ocamlc src/parser/ptree.ml Ocamlc src/mlw/pdecl.mli Ocamlc src/core/pretty.mli Ocamlc src/core/trans.mli 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/parser/ptree_helpers.mli Ocamlc src/transform/simplify_formula.mli Ocamlc src/parser/mlw_printer.mli Ocamlc src/transform/split_goal.mli Ocamlc src/transform/inlining.mli Ocamlc src/transform/args_wrapper.mli Ocamlc src/transform/compute.mli Ocamlc src/transform/eliminate_inductive.mli Ocamlc src/transform/eliminate_definition.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 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] Ocamlc src/transform/introduction.mli Ocamlc src/transform/ind_itp.mli Ocamlc src/transform/destruct.mli Ocamlc src/transform/cut.mli Ocamlc src/transform/reflection.mli Ocamlc src/session/strategy.mli 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] Ocamlc src/core/trans.ml Ocamlc src/core/dterm.ml Ocamlc src/driver/driver_lexer.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] Ocamlc src/driver/autodetection.ml 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] Ocamlc src/mlw/ity.ml Ocamlc src/mlw/expr.ml Ocamlc src/mlw/pdecl.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] 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] Ocamlc src/mlw/eval_match.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] Ocamlc src/mlw/typeinv.ml 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] Ocamlc src/mlw/vc.ml Ocamlc src/parser/mlw_printer.ml Ocamlc src/transform/simplify_formula.ml Ocamlc src/transform/compute.ml Ocamlc src/transform/split_goal.ml Ocamlc src/transform/remove_unused.ml Ocamlc src/transform/detect_polymorphism.ml Ocamlc src/transform/extensional.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] Ocamlc src/transform/abstract_quantifiers.ml Ocamlc src/transform/eliminate_symbol.ml Ocamlc src/transform/eliminate_inductive.ml Ocamlc src/transform/eliminate_let.ml Ocamlc src/transform/eliminate_if.ml Ocamlc src/transform/encoding.ml Ocamlc src/transform/libencoding.ml Ocamlc src/transform/simplify_array.ml Ocamlc src/transform/abstraction.ml Ocamlc src/transform/close_epsilon.ml Ocamlc src/transform/eliminate_epsilon.ml Ocamlc src/transform/lift_epsilon.ml Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.ml Ocamlc src/transform/prop_curry.ml Ocamlc src/transform/eliminate_literal.ml Ocamlc src/transform/generic_arg_trans_utils.ml Ocamlc src/transform/case.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] Ocamlc src/transform/apply.ml Ocamlc src/transform/subst.ml Ocamlc src/transform/introduction.ml Ocamlc src/transform/ind_itp.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] 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] Ocamlc src/transform/destruct.ml Ocamlc src/transform/cut.ml Ocamlc src/transform/congruence.ml Ocamlc src/transform/induction.ml Ocamlc src/transform/induction_pr.ml Ocamlc src/transform/keep_only_arithmetic.ml Ocamlc src/session/termcode.ml Ocamlc src/session/strategy.ml Coqc lib/coq/number/Coprime.v Coqc lib/coq/set/Fset.v Coqc lib/coq/list/Permut.v Ocamlopt src/core/pattern.ml Ocamlopt src/core/coercion.ml Ocamlc src/mlw/pmodule.mli Ocamlc src/core/printer.mli Ocamlc src/mlw/dexpr.mli Ocamlc src/mlw/pinterp_core.mli 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] Ocamlc src/extract/mltree.mli Ocamlc src/extract/mlinterp.mli 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] Ocamlc src/parser/typing.mli Ocamlc src/parser/lexer.mli Ocamlc src/parser/sexp_parser.mli Ocamlc src/transform/discriminate.mli Ocamlc src/session/strategy_parser.mli Ocamlc src/core/printer.ml Ocamlc src/mlw/pmodule.ml 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] 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/args_wrapper.ml Ocamlc src/transform/eliminate_unknown_types.ml Ocamlc src/transform/eliminate_unknown_lsymbols.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/reflection.ml Ocamlc src/printer/smtv1.ml Ocamlc src/printer/coq.ml Ocamlc src/printer/pvs.ml Ocamlc src/printer/isabelle.ml Ocamlc src/printer/simplify.ml Ocamlc src/printer/gappa.ml Ocamlc src/printer/cvc3.ml Ocamlc src/printer/yices.ml Ocamlc src/printer/mathematica.ml Ocamlc src/session/strategy_parser.ml Coqc lib/coq/set/FsetInduction.v Coqc lib/coq/set/FsetSum.v Coqc lib/coq/set/FsetInt.v Coqc lib/coq/set/SetApp.v Coqc lib/coq/set/SetImp.v 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/core/decl.ml Ocamlc src/parser/parser.mli 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/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] 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] Ocamlc src/core/model_parser.ml 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/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/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] Ocamlc src/driver/smtv2_model_parser.ml 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] Ocamlc src/extract/compile.ml Ocamlc src/extract/mlinterp.ml 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] Ocamlc src/extract/c.ml Ocamlc src/extract/java.ml 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] Ocamlc src/parser/parser.ml 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] Ocamlc src/parser/report.ml Coqc lib/coq/set/SetAppInt.v 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] Coqc lib/coq/set/SetImpInt.v Ocamlopt src/core/theory.ml Ocamlc src/core/keywords.mli Ocamlc src/driver/call_provers.mli Ocamlc src/extract/ml_printer.mli Ocamlc src/core/keywords.ml Ocamlc src/core/pretty.ml Ocamlc src/driver/call_provers.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] Ocamlc src/extract/ml_printer.ml Ocamlc src/extract/ocaml.ml Ocamlc src/extract/cakeml.ml Ocamlc src/parser/lexer.ml Ocamlc src/printer/why3printer.ml Ocamlopt src/core/keywords.ml Ocamlopt src/core/task.ml Ocamlopt src/core/env.ml Ocamlc src/driver/driver.mli Ocamlc src/mlw/pinterp.mli Ocamlc src/session/session_itp.mli Ocamlc src/driver/driver.ml Ocamlc src/mlw/pinterp.ml Ocamlc src/extract/pdriver.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/smtv2.ml Ocamlc src/session/session_itp.ml Ocamlopt src/core/pretty.ml Ocamlopt src/driver/whyconf.ml Ocamlc src/mlw/rac.mli Ocamlc src/mlw/check_ce.mli Ocamlopt src/transform/reduction_engine.ml Ocamlc src/session/controller_itp.mli Ocamlc src/mlw/rac.ml Ocamlc src/mlw/check_ce.ml Ocamlc src/session/controller_itp.ml Ocamlopt src/core/dterm.ml Ocamlopt src/core/trans.ml Ocamlopt src/mlw/ity.ml Ocamlopt src/driver/driver_lexer.ml Ocamlopt src/driver/autodetection.ml Ocamlopt src/transform/simplify_formula.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 Ocamlopt src/transform/eliminate_if.ml Ocamlopt src/transform/libencoding.ml Ocamlopt src/transform/simplify_array.ml Ocamlopt src/transform/abstraction.ml Ocamlopt src/transform/close_epsilon.ml Ocamlopt src/transform/eliminate_epsilon.ml Ocamlopt src/transform/instantiate_predicate.ml Ocamlopt src/transform/smoke_detector.ml Ocamlopt src/transform/prop_curry.ml Ocamlopt src/transform/eliminate_literal.ml 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 Ocamlopt src/session/termcode.ml Ocamlopt src/session/strategy.ml Ocamlc src/session/itp_communication.mli Ocamlopt src/core/printer.ml Ocamlopt src/mlw/expr.ml Ocamlopt src/transform/encoding.ml Ocamlopt src/transform/lift_epsilon.ml Ocamlopt src/session/strategy_parser.ml Ocamlc src/session/itp_server.mli Ocamlc src/session/server_utils.mli Ocamlc src/session/json_util.mli Ocamlc src/session/itp_communication.ml Ocamlc src/session/itp_server.ml Ocamlc src/session/json_util.ml Ocamlopt src/transform/eliminate_unknown_types.ml Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlopt src/transform/eliminate_algebraic.ml Ocamlopt src/transform/encoding_guards_full.ml Ocamlopt src/transform/encoding_tags_full.ml Ocamlopt src/transform/encoding_twin.ml Ocamlopt src/transform/filter_trigger.ml Ocamlopt src/printer/coq.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml Ocamlopt src/printer/mathematica.ml Ocamlc src/session/server_utils.ml Ocamlopt src/core/model_parser.ml Ocamlopt src/mlw/pdecl.ml Ocamlopt src/parser/ptree.ml Ocamlopt src/transform/encoding_guards.ml Ocamlopt src/transform/encoding_tags.ml Ocamlopt src/transform/encoding_sort.ml Linking lib/why3/why3.cmo 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 Ocamlopt src/driver/driver.ml Ocamlopt src/mlw/typeinv.ml Ocamlopt src/transform/inlining.ml Ocamlopt src/mlw/vc.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 src/why3session/why3session_lib.mli Ocamlc plugins/cfg/subregion_analysis.mli Ocamlc src/ide/gconfig.mli Ocamlc src/why3doc/doc_def.mli Ocamlc plugins/tptp/tptp_parser.mli Ocamlc plugins/tptp/tptp_typing.mli Ocamlc plugins/tptp/tptp_lexer.mli Ocamlc plugins/python/py_parser.mli Ocamlc plugins/python/py_lexer.mli Ocamlc plugins/microc/mc_parser.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_output.mli Ocamlc plugins/coma/coma_parser.mli Ocamlc src/why3session/why3session_create.mli Ocamlc plugins/coma/coma_lexer.mli Ocamlc plugins/coma/coma_typing.mli Ocamlopt src/mlw/pmodule.ml Ocamlopt src/parser/ptree_helpers.ml Ocamlopt src/mlw/pinterp_core.ml Ocamlopt src/mlw/dexpr.ml Ocamlopt src/parser/mlw_printer.ml Ocamlopt src/mlw/rac.ml Ocamlopt src/mlw/pinterp.ml Ocamlopt src/extract/mltree.ml Ocamlopt src/parser/typing.ml Ocamlopt src/extract/compile.ml Ocamlopt src/extract/pdriver.ml Ocamlopt src/mlw/check_ce.ml Ocamlopt src/extract/ml_printer.ml Ocamlopt src/extract/java.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 Ocamlopt src/parser/report.ml Ocamlopt src/parser/lexer.ml Ocamlopt src/transform/args_wrapper.ml Ocamlopt src/transform/compute.ml Ocamlopt src/transform/subst.ml Ocamlopt src/transform/apply.ml Ocamlopt src/transform/case.ml Ocamlopt src/transform/ind_itp.ml Ocamlopt src/transform/cut.ml Ocamlopt src/printer/gappa.ml Ocamlopt src/transform/eliminate_definition.ml Ocamlopt src/transform/discriminate.ml Ocamlopt src/transform/introduction.ml Ocamlopt src/transform/destruct.ml Ocamlopt src/transform/induction.ml Ocamlopt src/transform/induction_pr.ml Ocamlopt src/printer/alt_ergo.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/transform/encoding_select.ml Ocamlopt src/transform/prepare_for_counterexmp.ml Ocamlopt src/transform/reflection.ml Ocamlopt src/session/session_itp.ml Ocamlopt src/session/controller_itp.ml Ocamlopt src/session/itp_communication.ml Ocamlopt src/session/json_util.ml Ocamlopt src/session/server_utils.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/tptp/tptp_typing.ml Ocamlopt plugins/parser/dimacs.ml Ocamlopt plugins/tptp/tptp_printer.ml Ocamlopt plugins/python/py_parser.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/why3prove.ml Ocamlopt src/tools/why3extract.ml Ocamlopt src/tools/why3realize.ml Ocamlopt src/tools/why3replay.ml Ocamlopt src/tools/why3show.ml Ocamlopt src/tools/why3wc.ml Ocamlopt src/tools/why3bench.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/why3wc.cmxs Linking bin/why3show.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/python.cmxs Linking lib/plugins/microc.cmxs Linking bin/why3ide.cmxs Linking bin/why3session.cmxs Linking bin/why3doc.cmxs ld: warning: libfontconfig.so.2, needed by /tmp/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