=> Bootstrap dependency digest>=20010302: found digest-20190127 ===> Skipping vulnerability checks. WARNING: No /var/db/pkg/pkg-vulnerabilities file found. WARNING: To fix run: `/usr/sbin/pkg_admin -K /var/db/pkg fetch-pkg-vulnerabilities'. ===> Building for coq-8.12.2nb1 rm -f cp -a ".merlin.in" ".merlin" cp -a "ide/.merlin.in" "ide/.merlin" cp -a "kernel/.merlin.in" "kernel/.merlin" cp -a "plugins/.merlin.in" "plugins/.merlin" cp -a "test-suite/unit-tests/.merlin.in" "test-suite/unit-tests/.merlin" cp -a "META.coq.in" "META.coq" mkdir bin /usr/pkg/bin/gmake --warn-undefined-variable --no-builtin-rules -f Makefile.build world gmake[1]: Entering directory '/scratch/work/lang/coq/work/coq-8.12.2' OCAMLC clib/segmenttree.mli OCAMLC clib/unicode.mli OCAMLC tools/coqdep_lexer.mli OCAMLLEX tools/coqdep_lexer.mll 217 states, 2223 transitions, table size 10194 bytes OCAMLC tools/coqdep_common.mli OCAMLC kernel/genOpcodeFiles.ml OCAMLLEX tools/ocamllibdep.mll OCAMLC coqpp/coqpp_ast.mli 14 states, 417 transitions, table size 1752 bytes gmake[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. OCAMLYACC coqpp/coqpp_parse.mly OCAMLLEX coqpp/coqpp_lex.mll mkdir -p gramlib/.pack OCAMLLEX ide/config_lexer.mll 240 states, 15992 transitions, table size 65408 bytes OCAMLLEX ide/coq_lex.mll 30 states, 1657 transitions, table size 6808 bytes 6052 additional bytes used for bindings OCAMLLEX ide/protocol/xml_lexer.mll OCAMLLEX ide/utf8_convert.mll 124 states, 1808 transitions, table size 7976 bytes 80 states, 774 transitions, table size 3576 bytes 15 states, 827 transitions, table size 3398 bytes printf '# 1 "%s"\n' gramlib/ploc.ml > gramlib/.pack/gramlib__Ploc.ml OCAMLLEX tools/coqdoc/cpretty.mll printf '# 1 "%s"\n' gramlib/plexing.ml > gramlib/.pack/gramlib__Plexing.ml OCAMLLEX tools/coqwc.mll cat gramlib/ploc.ml >> gramlib/.pack/gramlib__Ploc.ml cat gramlib/plexing.ml >> gramlib/.pack/gramlib__Plexing.ml printf '# 1 "%s"\n' gramlib/gramext.ml > gramlib/.pack/gramlib__Gramext.ml cat gramlib/gramext.ml >> gramlib/.pack/gramlib__Gramext.ml printf '# 1 "%s"\n' gramlib/grammar.ml > gramlib/.pack/gramlib__Grammar.ml echo " \ module Ploc = Gramlib__Ploc \ module Plexing = Gramlib__Plexing \ module Gramext = Gramlib__Gramext \ module Grammar = Gramlib__Grammar" > gramlib/.pack/gramlib.ml cat gramlib/grammar.ml >> gramlib/.pack/gramlib__Grammar.ml rm -f ide/coqide_os_specific.ml && cp ide/coqide_X11.ml.in ide/coqide_os_specific.ml && chmod a-w ide/coqide_os_specific.ml 244 states, 858 transitions, table size 4896 bytes rm -f kernel/uint63.ml && cp kernel/uint63_31.ml kernel/uint63.ml && chmod a-w kernel/uint63.ml WRITE kernel/copcodes.ml printf '# 1 "%s"\n' gramlib/ploc.mli > gramlib/.pack/gramlib__Ploc.mli printf '# 1 "%s"\n' gramlib/plexing.mli > gramlib/.pack/gramlib__Plexing.mli cat gramlib/ploc.mli >> gramlib/.pack/gramlib__Ploc.mli cat gramlib/plexing.mli >> gramlib/.pack/gramlib__Plexing.mli printf '# 1 "%s"\n' gramlib/gramext.mli > gramlib/.pack/gramlib__Gramext.mli printf '# 1 "%s"\n' gramlib/grammar.mli > gramlib/.pack/gramlib__Grammar.mli cat gramlib/gramext.mli >> gramlib/.pack/gramlib__Gramext.mli cat gramlib/grammar.mli >> gramlib/.pack/gramlib__Grammar.mli WRITE kernel/byterun/coq_instruct.h WRITE kernel/byterun/coq_jumptbl.h OCAMLDEP checker/MLFILES checker/MLIFILES OCAMLOPT clib/segmenttree.ml OCAMLC clib/segmenttree.ml OCAMLC tools/coqdep_boot.ml CCDEP kernel/byterun/coq_values.c CCDEP kernel/byterun/coq_memory.c 2714 states, 8784 transitions, table size 51420 bytes 17613 additional bytes used for bindings CCDEP kernel/byterun/coq_interp.c CCDEP kernel/byterun/coq_fix_code.c OCAMLC tools/ocamllibdep.ml OCAMLC coqpp/coqpp_parse.mli OCAMLC clib/unicodetable.ml OCAMLOPT tools/ocamllibdep.ml OCAMLC coqpp/coqpp_parse.ml OCAMLOPT clib/unicodetable.ml OCAMLBEST -o bin/ocamllibdep OCAMLC clib/unicode.ml OCAMLC coqpp/coqpp_lex.ml OCAMLC -a bin/coqpp OCAMLC clib/minisys.ml OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES COQPP parsing/g_constr.mlg COQPP parsing/g_prim.mlg COQPP plugins/btauto/g_btauto.mlg COQPP plugins/cc/g_congruence.mlg COQPP plugins/derive/g_derive.mlg COQPP plugins/extraction/g_extraction.mlg COQPP plugins/firstorder/g_ground.mlg COQPP plugins/funind/g_indfun.mlg COQPP plugins/ltac/coretactics.mlg COQPP plugins/ltac/extraargs.mlg COQPP plugins/ltac/extratactics.mlg COQPP plugins/ltac/g_class.mlg COQPP plugins/ltac/g_auto.mlg COQPP plugins/ltac/g_eqdecide.mlg COQPP plugins/ltac/g_ltac.mlg COQPP plugins/ltac/g_obligations.mlg COQPP plugins/ltac/g_rewrite.mlg COQPP plugins/ltac/g_tactic.mlg COQPP plugins/ltac/profile_ltac_tactics.mlg COQPP plugins/micromega/g_micromega.mlg COQPP plugins/micromega/g_zify.mlg COQPP plugins/nsatz/g_nsatz.mlg COQPP plugins/omega/g_omega.mlg COQPP plugins/rtauto/g_rtauto.mlg COQPP plugins/setoid_ring/g_newring.mlg COQPP plugins/ssr/ssrparser.mlg COQPP plugins/ssr/ssrvernac.mlg COQPP plugins/ssrmatching/g_ssrmatching.mlg COQPP plugins/ssrsearch/g_search.mlg COQPP plugins/syntax/g_numeral.mlg COQPP plugins/syntax/g_string.mlg COQPP toplevel/g_toplevel.mlg COQPP vernac/g_proofs.mlg COQPP vernac/g_vernac.mlg COQPP user-contrib/Ltac2/g_ltac2.mlg OCAMLLIBDEP user-contrib/MLLIBFILES user-contrib/MLPACKFILES OCAMLDEP user-contrib/MLFILES user-contrib/MLIFILES OCAMLLIBDEP plugins/MLLIBFILES plugins/MLPACKFILES OCAMLDEP plugins/MLFILES plugins/MLIFILES OCAMLLIBDEP MLLIBFILES MLPACKFILES OCAMLDEP MLFILES MLIFILES OCAMLOPT clib/unicode.ml OCAMLOPT clib/minisys.ml OCAMLOPT tools/coqdep_lexer.ml OCAMLOPT tools/coqdep_common.ml OCAMLOPT tools/coqdep_boot.ml OCAMLBEST -o bin/coqdep_boot COQDEP VFILES gmake[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. OCAMLC config/coq_config.mli OCAMLC clib/cObj.mli OCAMLC clib/cEphemeron.mli OCAMLC clib/cSig.mli OCAMLC clib/orderedType.mli OCAMLC clib/hashset.mli OCAMLC clib/range.mli OCAMLC clib/bigint.mli OCAMLC clib/cArray.mli OCAMLC clib/option.mli OCAMLC clib/cUnix.mli OCAMLC clib/cThread.mli OCAMLC clib/predicate.mli OCAMLC clib/trie.mli OCAMLC clib/heap.mli OCAMLC clib/unionfind.mli OCAMLC clib/store.mli OCAMLC clib/dyn.mli OCAMLC clib/exninfo.mli OCAMLC clib/iStream.mli OCAMLC clib/terminal.mli OCAMLC clib/monad.mli OCAMLC clib/diff2.mli OCAMLC lib/hook.mli OCAMLC lib/flags.mli OCAMLC lib/control.mli OCAMLC lib/pp.mli OCAMLC lib/loc.mli OCAMLC lib/xml_datatype.mli OCAMLC lib/cProfile.mli OCAMLC lib/spawn.mli OCAMLC lib/cAst.mli OCAMLC lib/genarg.mli OCAMLC lib/remoteCounter.mli OCAMLC lib/aux_file.mli OCAMLC lib/envars.mli OCAMLC lib/coqProject_file.mli OCAMLC kernel/uint63.mli OCAMLC kernel/copcodes.ml OCAMLC kernel/cPrimitives.mli OCAMLC library/summary.mli OCAMLC engine/logic_monad.mli OCAMLC interp/numTok.mli OCAMLC interp/deprecation.mli OCAMLC gramlib/.pack/gramlib.ml OCAMLC tactics/dnet.mli OCAMLC tactics/dn.mli OCAMLC stm/spawned.mli OCAMLC stm/dag.mli OCAMLC stm/tQueue.mli OCAMLC stm/coqworkmgrApi.mli OCAMLC stm/vio_checking.mli OCAMLC toplevel/usage.mli OCAMLC toplevel/workerLoop.mli OCAMLC toplevel/coqc.mli OCAMLC kernel/byterun/coq_fix_code.c OCAMLC kernel/byterun/coq_memory.c OCAMLC kernel/byterun/coq_values.c OCAMLC kernel/byterun/coq_interp.c In file included from coq_interp.c:53:0: coq_uint63_emul.h: In function 'uint63_one': coq_uint63_emul.h:25:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:99:1: note: in expansion of macro 'DECLARE_NULLOP' DECLARE_NULLOP(one) ^~~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_add_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:100:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(add) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_addcarry_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:102:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(addcarry) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_addmuldiv_ml': coq_uint63_emul.h:84:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:104:1: note: in expansion of macro 'DECLARE_TEROP' DECLARE_TEROP(addmuldiv) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_div_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:106:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(div) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_eq_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:108:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(eq) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_eq0_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:110:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(eq0) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_head0_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:112:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(head0) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_land_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:114:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(land) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_leq_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:116:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(leq) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_lor_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:118:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(lor) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_lsl_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:120:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(lsl) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_lsl1_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:122:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(lsl1) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_lsr_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:124:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(lsr) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_lsr1_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:126:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(lsr1) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_lt_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:128:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(lt) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_lxor_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:130:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(lxor) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_mod_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:132:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(mod) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_mul_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:134:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(mul) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_sub_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:136:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(sub) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_subcarry_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:138:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(subcarry) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_tail0_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:140:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(tail0) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_div21_ml_ml': coq_uint63_emul.h:84:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:143:1: note: in expansion of macro 'DECLARE_TEROP' DECLARE_TEROP(div21_ml) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_mulc_ml_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:157:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(mulc_ml) ^~~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_to_float_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:170:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(to_float) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_of_float_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:173:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(of_float) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_of_int_ml': coq_uint63_emul.h:33:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:179:1: note: in expansion of macro 'DECLARE_UNOP' DECLARE_UNOP(of_int) ^~~~~~~~~~~~ coq_uint63_emul.h: In function 'uint63_to_int_min_ml': coq_uint63_emul.h:58:15: warning: assignment discards 'const' qualifier from pointer target type [-Wdiscarded-qualifiers] if (!cb) cb = caml_named_value("uint63 " #name); \ ^ coq_uint63_emul.h:182:1: note: in expansion of macro 'DECLARE_BINOP' DECLARE_BINOP(to_int_min) ^~~~~~~~~~~~~ OCAMLC plugins/ltac/tauto.mli OCAMLC plugins/micromega/micromega.mli OCAMLC plugins/micromega/numCompat.mli OCAMLC plugins/micromega/persistent_cache.mli OCAMLC plugins/micromega/g_micromega.mli OCAMLC plugins/syntax/r_syntax.mli OCAMLC plugins/ssr/ssrvernac.mli OCAMLC plugins/nsatz/utile.mli OCAMLC plugins/nsatz/polynom.mli OCAMLC plugins/rtauto/proof_search.mli OCAMLC user-contrib/Ltac2/tac2dyn.mli OCAMLC user-contrib/Ltac2/tac2stdlib.mli OCAMLC checker/analyze.mli OCAMLC checker/values.mli OCAMLC checker/checker.mli OCAMLC plugins/micromega/sos_lib.mli OCAMLC plugins/micromega/csdpcert.mli OCAMLC ide/protocol/xml_lexer.mli OCAMLC ide/protocol/xml_parser.mli OCAMLC ide/protocol/xml_printer.mli OCAMLC ide/protocol/serialize.mli OCAMLC ide/protocol/richpp.mli OCAMLC tools/coq_tex.ml OCAMLC tools/coqwc.ml OCAMLC tools/coqdoc/cdglobals.mli OCAMLC tools/coqdoc/alpha.mli OCAMLC tools/coqworkmgr.ml OCAMLC checker/votour.mli OCAMLC -a bin/doc_grammar "/usr/pkg/bin/ocamlfind" ocamlc -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67 -safe-string -strict-sequence ide/default_bindings_src.ml -o ide/default_bindings_src.exe OCAMLC ide/minilib.mli OCAMLC ide/configwin_messages.ml OCAMLC ide/configwin_types.ml OCAMLC ide/configwin.mli OCAMLC ide/tags.mli OCAMLC ide/wg_Notebook.mli OCAMLC ide/utf8_convert.mli OCAMLC ide/unicode_bindings.mli OCAMLC ide/coq_lex.mli OCAMLC ide/sentence.mli OCAMLC ide/gtk_parsing.mli OCAMLC ide/wg_Segment.mli OCAMLC ide/wg_Detachable.mli OCAMLC ide/wg_Find.mli OCAMLC ide/coq_commands.mli OCAMLC ide/coqide_ui.mli OCAMLC ide/coqide.mli OCAMLC ide/coqide_os_specific.mli CHECK revision OCAMLOPT config/coq_config.ml OCAMLOPT clib/cObj.ml OCAMLOPT clib/cEphemeron.ml OCAMLC clib/cMap.mli OCAMLC clib/hashcons.mli OCAMLC clib/cList.mli OCAMLOPT clib/option.ml OCAMLOPT clib/cThread.ml OCAMLOPT clib/trie.ml OCAMLOPT clib/predicate.ml OCAMLOPT clib/heap.ml OCAMLOPT clib/unionfind.ml OCAMLOPT clib/iStream.ml OCAMLOPT clib/terminal.ml OCAMLOPT clib/monad.ml OCAMLOPT clib/diff2.ml OCAMLOPT lib/hook.ml OCAMLC lib/pp_diff.mli OCAMLC lib/stateid.mli OCAMLC lib/cErrors.mli OCAMLC lib/cWarnings.mli OCAMLC lib/rtree.mli OCAMLC lib/system.mli OCAMLC lib/explore.mli OCAMLC lib/future.mli OCAMLC lib/dAst.mli OCAMLC kernel/float64.mli OCAMLC kernel/evar.mli OCAMLOPT kernel/copcodes.ml OCAMLOPT gramlib/.pack/gramlib.ml OCAMLC gramlib/.pack/gramlib__Ploc.mli OCAMLC gramlib/.pack/gramlib__Gramext.mli OCAMLOPT tactics/dnet.ml OCAMLC stm/vcs.mli OCAMLOPT stm/coqworkmgrApi.ml OCAMLC stm/workerPool.mli OCAMLOPT toplevel/usage.ml OCAMLOPT plugins/micromega/micromega.ml OCAMLOPT plugins/micromega/numCompat.ml OCAMLC plugins/micromega/mutils.mli OCAMLC plugins/micromega/itv.mli OCAMLC plugins/micromega/sos_types.mli OCAMLC plugins/nsatz/ideal.mli OCAMLOPT checker/analyze.ml OCAMLOPT checker/values.ml OCAMLC checker/validate.mli OCAMLOPT plugins/micromega/sos_lib.ml OCAMLC plugins/micromega/sos.mli OCAMLOPT ide/protocol/xml_lexer.ml OCAMLOPT ide/protocol/xml_printer.ml OCAMLC ide/document.mli OCAMLC tools/coqdep.ml OCAMLOPT tools/coq_tex.ml OCAMLOPT tools/coqwc.ml OCAMLOPT tools/coqdoc/cdglobals.ml OCAMLC tools/coqdoc/index.mli OCAMLC tools/coqdoc/cpretty.mli OCAMLOPT tools/coqworkmgr.ml OCAMLOPT checker/votour.ml ide/default_bindings_src.exe ide/default.bindings OCAMLOPT ide/configwin_messages.ml OCAMLOPT ide/configwin_types.ml OCAMLC ide/configwin_ihm.mli OCAMLOPT ide/tags.ml OCAMLOPT ide/utf8_convert.ml OCAMLOPT ide/gtk_parsing.ml OCAMLOPT ide/wg_Detachable.ml OCAMLOPT ide/coqide_os_specific.ml OCAMLOPT ide/coq_commands.ml OCAMLOPT -a -o config/config.cmxa OCAMLOPT clib/cMap.ml OCAMLC clib/int.mli OCAMLC clib/cSet.mli OCAMLC clib/cString.mli OCAMLC clib/hMap.mli OCAMLC lib/feedback.mli OCAMLC lib/acyclicGraph.mli OCAMLC lib/objFile.mli OCAMLOPT gramlib/.pack/gramlib__Gramext.ml cd kernel/byterun/ && \ "/usr/pkg/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o OCAMLC stm/asyncTaskQueue.mli OCAMLOPT plugins/micromega/itv.ml OCAMLC plugins/micromega/vect.mli OCAMLOPT plugins/micromega/sos_types.ml OCAMLC plugins/micromega/certificate.mli OCAMLOPT checker/validate.ml OCAMLOPT ide/protocol/xml_parser.ml OCAMLC tools/coq_makefile.ml OCAMLBEST -o bin/coq-tex OCAMLBEST -o bin/coqwc OCAMLOPT tools/coqdoc/alpha.ml OCAMLC tools/coqdoc/tokens.mli OCAMLC tools/coqdoc/output.mli OCAMLBEST -o bin/votour OCAMLC ide/ideutils.mli OCAMLOPT ide/coq_lex.ml OCAMLOPT clib/int.ml OCAMLC lib/util.mli OCAMLC plugins/micromega/polynomial.mli OCAMLOPT plugins/micromega/sos.ml OCAMLOPT tools/coqdoc/index.ml OCAMLC tools/coqdoc/main.ml OCAMLC ide/config_lexer.mli OCAMLC ide/preferences.mli OCAMLOPT ide/sentence.ml OCAMLC ide/wg_MessageView.mli OCAMLC ide/fileOps.mli OCAMLOPT clib/hashset.ml OCAMLOPT clib/orderedType.ml OCAMLOPT clib/cList.ml OCAMLOPT clib/range.ml OCAMLOPT clib/hMap.ml OCAMLOPT clib/bigint.ml OCAMLOPT clib/dyn.ml OCAMLC kernel/names.mli OCAMLOPT kernel/uint63.ml OCAMLC kernel/esubst.mli OCAMLC gramlib/.pack/gramlib__Plexing.mli OCAMLC parsing/tok.mli OCAMLOPT stm/dag.ml OCAMLOPT plugins/micromega/mutils.ml OCAMLC plugins/micromega/mfourier.mli OCAMLC plugins/micromega/simplex.mli OCAMLC plugins/omega/omega.ml OCAMLC plugins/extraction/miniml.mli OCAMLOPT user-contrib/Ltac2/tac2dyn.ml OCAMLC ide/protocol/interface.ml OCAMLOPT tools/coqdoc/tokens.ml OCAMLC ide/wg_RoutedMessageViews.mli OCAMLOPT clib/hashcons.ml OCAMLOPT clib/cArray.ml OCAMLOPT clib/store.ml OCAMLC kernel/transparentState.mli OCAMLOPT kernel/float64.ml OCAMLC kernel/univ.mli OCAMLC kernel/retroknowledge.mli OCAMLC kernel/conv_oracle.mli OCAMLC library/libnames.mli OCAMLC engine/evar_kinds.mli OCAMLC pretyping/locus.ml OCAMLC proofs/goal_select.mli OCAMLC gramlib/.pack/gramlib__Grammar.mli OCAMLC parsing/cLexer.mli OCAMLC tactics/declareScheme.mli OCAMLC tactics/declareUctx.mli OCAMLC vernac/canonical.mli OCAMLC vernac/loadpath.mli OCAMLOPT plugins/micromega/vect.ml OCAMLC plugins/extraction/modutil.mli OCAMLC plugins/extraction/common.mli OCAMLC plugins/extraction/ocaml.mli OCAMLC plugins/extraction/haskell.mli OCAMLC plugins/extraction/scheme.mli OCAMLC plugins/extraction/json.mli OCAMLC user-contrib/Ltac2/tac2expr.mli OCAMLOPT plugins/micromega/csdpcert.ml OCAMLC ide/protocol/xmlprotocol.mli OCAMLOPT tools/coqdoc/output.ml OCAMLC ide/coq.mli OCAMLC ide/wg_ProofView.mli OCAMLOPT clib/cSet.ml OCAMLOPT clib/cString.ml OCAMLOPT clib/exninfo.ml OCAMLOPT lib/pp.ml OCAMLC kernel/uGraph.mli OCAMLC kernel/sorts.mli OCAMLC library/coqlib.mli OCAMLC engine/univNames.mli OCAMLC pretyping/locusops.mli OCAMLC interp/decls.mli OCAMLOPT plugins/micromega/polynomial.ml OCAMLC ide/fake_ide.ml OCAMLC ide/wg_Completion.mli OCAMLC ide/wg_ScriptView.mli OCAMLOPT clib/cUnix.ml OCAMLOPT lib/flags.ml OCAMLOPT lib/control.ml OCAMLOPT lib/util.ml OCAMLOPT lib/pp_diff.ml OCAMLOPT lib/loc.ml OCAMLOPT lib/coqProject_file.ml OCAMLOPT kernel/evar.ml OCAMLC kernel/context.mli OCAMLOPT interp/numTok.ml OCAMLOPT gramlib/.pack/gramlib__Ploc.ml OCAMLOPT gramlib/.pack/gramlib__Plexing.ml OCAMLOPT tactics/dn.ml OCAMLOPT plugins/micromega/simplex.ml OCAMLOPT plugins/omega/omega.ml OCAMLOPT ide/protocol/serialize.ml OCAMLOPT ide/protocol/richpp.ml OCAMLOPT tools/coqdoc/cpretty.ml OCAMLOPT ide/wg_Notebook.ml OCAMLOPT ide/config_lexer.ml OCAMLC ide/coqOps.mli OCAMLOPT -a -o clib/clib.cmxa OCAMLOPT lib/stateid.ml OCAMLOPT lib/cErrors.ml OCAMLOPT lib/rtree.ml OCAMLOPT lib/cAst.ml OCAMLOPT lib/envars.ml OCAMLOPT kernel/cPrimitives.ml OCAMLOPT kernel/esubst.ml OCAMLC kernel/constr.mli OCAMLOPT parsing/tok.ml OCAMLOPT stm/vcs.ml OCAMLOPT stm/tQueue.ml OCAMLOPT stm/workerPool.ml OCAMLOPT plugins/micromega/mfourier.ml OCAMLOPT plugins/micromega/persistent_cache.ml OCAMLC plugins/funind/functional_principles_types.mli OCAMLBEST -o plugins/micromega/csdpcert OCAMLOPT ide/document.ml OCAMLOPT tools/coqdoc/main.ml OCAMLOPT ide/minilib.ml OCAMLC ide/wg_Command.mli OCAMLOPT lib/feedback.ml OCAMLOPT lib/acyclicGraph.ml OCAMLOPT lib/cProfile.ml OCAMLOPT lib/future.ml OCAMLOPT lib/spawn.ml OCAMLOPT lib/dAst.ml OCAMLOPT lib/genarg.ml OCAMLOPT lib/remoteCounter.ml OCAMLOPT lib/aux_file.ml OCAMLOPT kernel/names.ml OCAMLC kernel/vars.mli OCAMLC kernel/term.mli OCAMLC kernel/vmvalues.mli OCAMLC kernel/mod_subst.mli OCAMLC kernel/nativevalues.mli OCAMLC engine/univSubst.mli OCAMLC engine/univProblem.mli OCAMLC engine/univops.mli OCAMLC engine/nameops.mli OCAMLOPT engine/logic_monad.ml OCAMLC pretyping/pattern.ml OCAMLC pretyping/keys.mli OCAMLOPT gramlib/.pack/gramlib__Grammar.ml OCAMLC tactics/term_dnet.mli OCAMLOPT stm/spawned.ml OCAMLOPT plugins/nsatz/utile.ml OCAMLOPT ide/protocol/interface.ml OCAMLOPT tools/coq_makefile.ml OCAMLOPT ide/configwin_ihm.ml OCAMLC ide/session.mli OCAMLOPT lib/cWarnings.ml OCAMLOPT lib/explore.ml OCAMLOPT kernel/transparentState.ml OCAMLOPT kernel/univ.ml OCAMLOPT kernel/retroknowledge.ml OCAMLC kernel/cbytecodes.mli OCAMLC kernel/opaqueproof.mli OCAMLOPT kernel/conv_oracle.ml OCAMLC kernel/vm.mli OCAMLOPT library/libnames.ml OCAMLC library/globnames.mli OCAMLOPT library/summary.ml OCAMLC engine/univMinim.mli OCAMLOPT engine/evar_kinds.ml OCAMLOPT pretyping/locus.ml OCAMLOPT interp/deprecation.ml OCAMLOPT -a -o gramlib/.pack/gramlib.cmxa OCAMLOPT parsing/cLexer.ml OCAMLC vernac/library.mli OCAMLOPT plugins/extraction/miniml.ml OCAMLOPT plugins/nsatz/polynom.ml OCAMLOPT ide/protocol/xmlprotocol.ml OCAMLOPT ide/configwin.ml OCAMLC ide/microPG.mli OCAMLOPT lib/system.ml OCAMLOPT kernel/uGraph.ml OCAMLOPT kernel/sorts.ml OCAMLC kernel/cemitcodes.mli OCAMLC library/libobject.mli OCAMLC library/nametab.mli OCAMLOPT pretyping/locusops.ml OCAMLOPT plugins/nsatz/ideal.ml OCAMLOPT -a -o ide/protocol/ideprotocol.cmxa OCAMLOPT ide/fake_ide.ml OCAMLOPT -a -o ide/ide_common.cmxa OCAMLOPT tools/coqdep.ml OCAMLOPT ide/preferences.ml OCAMLOPT lib/objFile.ml OCAMLOPT kernel/context.ml OCAMLC kernel/declarations.ml OCAMLC kernel/entries.ml OCAMLC kernel/environ.mli OCAMLC kernel/cooking.mli OCAMLOPT -a -o lib/lib.cmxa OCAMLC kernel/declareops.mli OCAMLC kernel/primred.mli OCAMLC kernel/cClosure.mli OCAMLC kernel/reduction.mli OCAMLC kernel/clambda.mli OCAMLC kernel/nativelambda.mli OCAMLC kernel/cbytegen.mli OCAMLC kernel/csymtable.mli OCAMLC kernel/vconv.mli OCAMLC kernel/nativeconv.mli OCAMLC kernel/type_errors.mli OCAMLC kernel/modops.mli OCAMLC kernel/inductive.mli OCAMLC kernel/typeops.mli OCAMLC kernel/inferCumulativity.mli OCAMLC kernel/indTyping.mli OCAMLC kernel/indtypes.mli OCAMLC kernel/term_typing.mli OCAMLC kernel/subtyping.mli OCAMLC kernel/mod_typing.mli OCAMLC kernel/section.mli OCAMLC library/goptions.mli OCAMLC engine/univGen.mli OCAMLOPT engine/nameops.ml OCAMLC pretyping/arguments_renaming.mli OCAMLC pretyping/heads.mli OCAMLC printing/printmod.mli OCAMLC vernac/attributes.mli OCAMLC plugins/extraction/table.mli OCAMLC checker/checkFlags.mli OCAMLC checker/checkInductive.mli OCAMLC checker/mod_checking.mli OCAMLC checker/checkTypes.mli OCAMLC checker/check_stat.mli OCAMLBEST -o bin/coqdep OCAMLBEST -o bin/coq_makefile OCAMLBEST -o bin/coqdoc OCAMLBEST -o bin/coqworkmgr OCAMLOPT ide/ideutils.ml OCAMLOPT ide/wg_Segment.ml OCAMLOPT ide/coqide_ui.ml OCAMLOPT kernel/constr.ml OCAMLC kernel/relevanceops.mli OCAMLC kernel/nativecode.mli OCAMLC library/lib.mli OCAMLC plugins/extraction/mlutil.mli OCAMLC kernel/nativelib.mli OCAMLC kernel/nativelibrary.mli OCAMLC kernel/safe_typing.mli OCAMLC library/states.mli OCAMLOPT ide/unicode_bindings.ml OCAMLOPT ide/coq.ml OCAMLOPT ide/wg_MessageView.ml OCAMLOPT ide/wg_Find.ml OCAMLOPT ide/fileOps.ml OCAMLOPT kernel/vars.ml OCAMLOPT kernel/vmvalues.ml OCAMLOPT kernel/nativevalues.ml OCAMLC library/global.mli OCAMLOPT engine/univSubst.ml OCAMLC engine/uState.mli OCAMLOPT pretyping/pattern.ml OCAMLC checker/safe_checking.mli OCAMLC checker/check.mli OCAMLOPT ide/wg_ProofView.ml OCAMLOPT ide/wg_RoutedMessageViews.ml OCAMLOPT ide/wg_Completion.ml OCAMLOPT ide/wg_Command.ml OCAMLOPT kernel/term.ml OCAMLOPT kernel/mod_subst.ml OCAMLOPT kernel/cbytecodes.ml OCAMLOPT engine/univProblem.ml OCAMLC engine/evd.mli OCAMLOPT ide/wg_ScriptView.ml OCAMLOPT kernel/cemitcodes.ml OCAMLOPT kernel/opaqueproof.ml OCAMLOPT library/globnames.ml OCAMLC engine/eConstr.mli OCAMLC engine/proofview_monad.mli OCAMLC pretyping/indrec.mli OCAMLOPT kernel/declarations.ml OCAMLOPT library/libobject.ml OCAMLOPT library/nametab.ml OCAMLC engine/namegen.mli OCAMLC engine/termops.mli OCAMLC engine/proofview.mli OCAMLC pretyping/pretype_errors.mli OCAMLC pretyping/reductionops.mli OCAMLC pretyping/inductiveops.mli OCAMLC pretyping/retyping.mli OCAMLC pretyping/vnorm.mli OCAMLC pretyping/nativenorm.mli OCAMLC pretyping/cbv.mli OCAMLC pretyping/find_subterm.mli OCAMLC pretyping/evardefine.mli OCAMLC pretyping/evarsolve.mli OCAMLC pretyping/recordops.mli OCAMLC pretyping/typing.mli OCAMLC pretyping/glob_term.ml OCAMLC pretyping/typeclasses_errors.mli OCAMLC pretyping/typeclasses.mli OCAMLC pretyping/coercionops.mli OCAMLC pretyping/program.mli OCAMLC interp/constrexpr.ml OCAMLC proofs/tactypes.ml OCAMLC proofs/goal.mli OCAMLC proofs/refine.mli OCAMLC proofs/logic.mli OCAMLC parsing/pcoq.mli OCAMLC printing/pputils.mli OCAMLC printing/ppconstr.mli OCAMLC tactics/btermdn.mli OCAMLC tactics/tacticals.mli OCAMLC tactics/hipattern.mli OCAMLC tactics/ind_tables.mli OCAMLC tactics/abstract.mli OCAMLC tactics/contradiction.mli OCAMLC tactics/inv.mli OCAMLC tactics/eqdecide.mli OCAMLC vernac/declaremods.mli OCAMLC vernac/retrieveObl.mli OCAMLC vernac/himsg.mli OCAMLC vernac/declareUniv.mli OCAMLC vernac/recLemmas.mli OCAMLC vernac/auto_ind_decl.mli OCAMLC vernac/comPrimitive.mli OCAMLC vernac/prettyp.mli OCAMLC plugins/ltac/leminv.mli OCAMLC plugins/ltac/extratactics.mli OCAMLC plugins/cc/ccalgo.mli OCAMLC plugins/firstorder/formula.mli OCAMLC plugins/firstorder/unify.mli OCAMLC plugins/micromega/coq_micromega.mli OCAMLC plugins/omega/coq_omega.mli OCAMLC plugins/extraction/extraction.mli OCAMLC plugins/funind/glob_term_to_relation.mli OCAMLC plugins/funind/invfun.mli OCAMLC plugins/btauto/refl_btauto.mli OCAMLC plugins/nsatz/nsatz.mli OCAMLC plugins/rtauto/refl_tauto.mli OCAMLC user-contrib/Ltac2/tac2qexpr.mli OCAMLC user-contrib/Ltac2/tac2core.mli OCAMLOPT ide/coqOps.ml OCAMLOPT kernel/entries.ml OCAMLOPT kernel/cooking.ml OCAMLOPT engine/univNames.ml OCAMLC engine/evarutil.mli OCAMLC engine/ftactic.mli OCAMLC pretyping/evarconv.mli OCAMLC interp/notation_term.ml OCAMLC interp/smartlocate.mli OCAMLC interp/constrexpr_ops.mli OCAMLC interp/impargs.mli OCAMLC interp/modintern.mli OCAMLC proofs/miscprint.mli OCAMLC proofs/proof.mli OCAMLC proofs/refiner.mli OCAMLC proofs/tacmach.mli OCAMLC parsing/extend.ml OCAMLC parsing/g_constr.ml OCAMLC parsing/g_prim.ml OCAMLC printing/proof_diffs.mli OCAMLC tactics/eqschemes.mli OCAMLC tactics/elimschemes.mli OCAMLC vernac/declareInd.mli OCAMLC plugins/cc/ccproof.mli OCAMLC plugins/funind/indfun_common.mli OCAMLOPT ide/session.ml OCAMLOPT kernel/declareops.ml OCAMLC pretyping/geninterp.mli OCAMLC pretyping/coercion.mli OCAMLC interp/genintern.mli OCAMLC interp/notation_ops.mli OCAMLC interp/notation.mli OCAMLC interp/syntax_def.mli OCAMLC interp/reserve.mli OCAMLC interp/implicit_quantifiers.mli OCAMLC proofs/proof_bullet.mli OCAMLC parsing/notation_gram.ml OCAMLC parsing/ppextend.mli OCAMLC printing/genprint.mli OCAMLC tactics/genredexpr.ml OCAMLC vernac/egramcoq.mli OCAMLC plugins/cc/cctac.mli OCAMLC plugins/funind/functional_principles_proofs.mli OCAMLC plugins/ssrmatching/ssrmatching.mli OCAMLC user-contrib/Ltac2/tac2intern.mli OCAMLOPT kernel/environ.ml OCAMLC pretyping/ltac_pretype.ml OCAMLC interp/dumpglob.mli OCAMLC parsing/notgram_ops.mli OCAMLC tactics/redops.mli OCAMLC tactics/redexpr.mli OCAMLC tactics/ppred.mli OCAMLC toplevel/coqcargs.mli OCAMLC plugins/ssrmatching/g_ssrmatching.mli OCAMLC user-contrib/Ltac2/tac2ffi.mli OCAMLC user-contrib/Ltac2/tac2match.mli OCAMLOPT ide/microPG.ml OCAMLC pretyping/glob_ops.mli OCAMLC pretyping/patternops.mli OCAMLC pretyping/constr_matching.mli OCAMLC pretyping/tacred.mli OCAMLC pretyping/detyping.mli OCAMLC pretyping/globEnv.mli OCAMLC interp/stdarg.mli OCAMLC interp/constrextern.mli OCAMLC proofs/evar_refiner.mli OCAMLC printing/printer.mli OCAMLC user-contrib/Ltac2/tac2env.mli OCAMLC user-contrib/Ltac2/tac2print.mli OCAMLOPT checker/checkFlags.ml OCAMLOPT checker/check_stat.ml OCAMLOPT kernel/primred.ml OCAMLOPT kernel/section.ml OCAMLC pretyping/cases.mli OCAMLC pretyping/pretyping.mli OCAMLC vernac/assumptions.mli OCAMLC user-contrib/Ltac2/tac2interp.mli OCAMLOPT ide/coqide.ml OCAMLOPT kernel/cClosure.ml OCAMLC pretyping/unification.mli OCAMLC interp/constrintern.mli OCAMLC plugins/funind/glob_termops.mli OCAMLC proofs/clenv.mli OCAMLC proofs/clenvtac.mli OCAMLC tactics/tactics.mli OCAMLC tactics/hints.mli OCAMLC tactics/elim.mli OCAMLC tactics/equality.mli OCAMLC tactics/auto.mli OCAMLC tactics/eauto.mli OCAMLC tactics/class_tactics.mli OCAMLC tactics/autorewrite.mli OCAMLC vernac/vernacexpr.ml OCAMLC plugins/ltac/tacexpr.mli OCAMLC plugins/firstorder/sequent.mli OCAMLC user-contrib/Ltac2/tac2types.mli OCAMLOPT kernel/relevanceops.ml OCAMLC vernac/pvernac.mli OCAMLC vernac/egramml.mli OCAMLC vernac/ppvernac.mli OCAMLC vernac/proof_using.mli OCAMLC vernac/metasyntax.mli OCAMLC vernac/declare.mli OCAMLC vernac/vernacprop.mli OCAMLC vernac/comHints.mli OCAMLC vernac/indschemes.mli OCAMLC vernac/comDefinition.mli OCAMLC vernac/comAssumption.mli OCAMLC vernac/search.mli OCAMLC vernac/comSearch.mli OCAMLC vernac/comInductive.mli OCAMLC vernac/comProgramFixpoint.mli OCAMLC vernac/record.mli OCAMLC vernac/mltop.mli OCAMLC vernac/topfmt.mli OCAMLC vernac/comArguments.mli OCAMLC vernac/proof_global.ml OCAMLC vernac/pfedit.ml OCAMLC vernac/declareDef.ml OCAMLC toplevel/g_toplevel.ml OCAMLC plugins/ltac/tacarg.mli OCAMLC plugins/ltac/tacsubst.mli OCAMLC plugins/ltac/tacenv.mli OCAMLC plugins/ltac/pptactic.mli OCAMLC plugins/ltac/pltac.mli OCAMLC plugins/ltac/taccoerce.mli OCAMLC plugins/ltac/tactic_debug.mli OCAMLC plugins/ltac/tacintern.mli OCAMLC plugins/ltac/profile_ltac.mli OCAMLC plugins/ltac/tactic_matching.mli OCAMLC plugins/ltac/tactic_option.mli OCAMLC plugins/syntax/string_notation.mli OCAMLC plugins/ltac/tacexpr.ml OCAMLC plugins/ltac/tacarg.ml OCAMLC plugins/ltac/tacsubst.ml OCAMLC plugins/ltac/tacenv.ml OCAMLC plugins/ltac/pptactic.ml OCAMLC plugins/ltac/pltac.ml OCAMLC plugins/ltac/taccoerce.ml OCAMLC plugins/ltac/tactic_debug.ml OCAMLC plugins/ltac/tacintern.ml OCAMLC plugins/ltac/tactic_matching.ml OCAMLC plugins/ltac/leminv.ml OCAMLC plugins/firstorder/rules.mli OCAMLC plugins/firstorder/ground.mli OCAMLC plugins/syntax/numeral.mli OCAMLC plugins/extraction/extract_env.mli OCAMLC plugins/syntax/int63_syntax.ml OCAMLC plugins/syntax/float_syntax.ml OCAMLC user-contrib/Ltac2/tac2entries.mli OCAMLC user-contrib/Ltac2/tac2extffi.mli OCAMLC user-contrib/Ltac2/tac2tactics.mli OCAMLOPT -a -o ide/ide.cmxa OCAMLOPT kernel/reduction.ml OCAMLC vernac/g_vernac.ml OCAMLC vernac/locality.mli OCAMLC vernac/declareObl.mli OCAMLC vernac/comCoercion.mli OCAMLC plugins/ltac/tacinterp.mli OCAMLC plugins/firstorder/instances.mli OCAMLOPT -o bin/coqide OCAMLC vernac/lemmas.mli OCAMLC plugins/ltac/evar_tactics.mli OCAMLC plugins/ltac/extraargs.mli OCAMLC plugins/ltac/rewrite.mli OCAMLC plugins/ltac/evar_tactics.ml OCAMLC plugins/ltac/tactic_option.ml OCAMLC plugins/funind/recdef.mli OCAMLC plugins/funind/gen_principle.mli OCAMLC plugins/derive/derive.mli OCAMLOPT checker/checkTypes.ml OCAMLOPT kernel/clambda.ml OCAMLOPT kernel/nativelambda.ml OCAMLOPT kernel/type_errors.ml OCAMLOPT kernel/inferCumulativity.ml OCAMLOPT pretyping/heads.ml OCAMLC vernac/g_proofs.ml OCAMLC vernac/vernacextend.mli OCAMLC vernac/obligations.mli OCAMLC vernac/classes.mli OCAMLC vernac/comFixpoint.mli OCAMLC vernac/vernacentries.mli OCAMLC vernac/vernacstate.mli OCAMLC stm/vernac_classifier.mli OCAMLC plugins/ltac/tacentries.mli OCAMLC plugins/ltac/g_obligations.ml OCAMLC plugins/ltac/g_tactic.ml OCAMLC plugins/syntax/g_string.ml OCAMLC plugins/ltac/tacinterp.ml OCAMLC plugins/ltac/tacentries.ml OCAMLC plugins/ltac/extraargs.ml OCAMLC plugins/ltac/extratactics.ml OCAMLC plugins/ltac/rewrite.ml OCAMLC plugins/syntax/g_numeral.ml OCAMLC plugins/derive/g_derive.ml OCAMLOPT kernel/cbytegen.ml OCAMLOPT kernel/nativecode.ml OCAMLOPT kernel/inductive.ml OCAMLC vernac/vernacinterp.mli OCAMLC stm/stm.mli OCAMLC plugins/ltac/coretactics.ml OCAMLC plugins/ltac/profile_ltac_tactics.ml OCAMLC plugins/ltac/g_auto.ml OCAMLC plugins/ltac/g_class.ml OCAMLC plugins/ltac/g_rewrite.ml OCAMLC plugins/ltac/g_eqdecide.ml OCAMLC plugins/ltac/g_ltac.ml OCAMLC plugins/ltac/profile_ltac.ml OCAMLOPT kernel/nativelib.ml OCAMLOPT kernel/csymtable.ml OCAMLOPT kernel/modops.ml OCAMLC stm/proofBlockDelimiter.mli OCAMLC toplevel/vernac.mli OCAMLC toplevel/coqargs.mli OCAMLOPT kernel/vm.ml OCAMLC toplevel/coqinit.mli OCAMLC toplevel/coqloop.mli OCAMLC toplevel/ccompile.mli OCAMLC toplevel/coqtop.mli OCAMLC -pack -o plugins/ltac/ltac_plugin.cmo OCAMLOPT kernel/vconv.ml OCAMLOPT kernel/subtyping.ml OCAMLOPT kernel/nativelibrary.ml OCAMLOPT kernel/nativeconv.ml OCAMLC plugins/cc/g_congruence.ml OCAMLC plugins/firstorder/g_ground.ml OCAMLC plugins/setoid_ring/newring_ast.mli OCAMLC plugins/micromega/zify.mli OCAMLC plugins/omega/g_omega.ml OCAMLC plugins/extraction/g_extraction.ml OCAMLC plugins/funind/indfun.mli OCAMLC plugins/btauto/g_btauto.ml OCAMLC plugins/ssrmatching/ssrmatching.ml OCAMLC plugins/ssrmatching/g_ssrmatching.ml OCAMLC plugins/nsatz/g_nsatz.ml OCAMLC plugins/rtauto/g_rtauto.ml OCAMLC user-contrib/Ltac2/tac2quote.mli OCAMLOPT kernel/typeops.ml OCAMLC plugins/setoid_ring/newring.mli OCAMLC plugins/micromega/g_zify.ml OCAMLC plugins/funind/g_indfun.ml OCAMLC user-contrib/Ltac2/g_ltac2.ml OCAMLC plugins/setoid_ring/g_newring.ml OCAMLOPT kernel/indTyping.ml OCAMLOPT kernel/term_typing.ml OCAMLOPT kernel/mod_typing.ml OCAMLC -pack -o plugins/ssrmatching/ssrmatching_plugin.cmo OCAMLOPT kernel/indtypes.ml OCAMLC plugins/ssr/ssrast.mli OCAMLC plugins/ssr/ssrprinters.mli OCAMLC plugins/ssr/ssrcommon.mli OCAMLC plugins/ssr/ssrtacticals.mli OCAMLC plugins/ssr/ssrelim.mli OCAMLC plugins/ssr/ssrview.mli OCAMLC plugins/ssr/ssrbwd.mli OCAMLC plugins/ssr/ssrequality.mli OCAMLC plugins/ssr/ssripats.mli OCAMLC plugins/ssr/ssrprinters.ml OCAMLC plugins/ssr/ssrcommon.ml OCAMLC plugins/ssr/ssrtacticals.ml OCAMLC plugins/ssr/ssrelim.ml OCAMLC plugins/ssr/ssrview.ml OCAMLC plugins/ssr/ssrbwd.ml OCAMLC plugins/ssr/ssrequality.ml OCAMLC plugins/ssr/ssripats.ml OCAMLC plugins/ssr/ssrvernac.ml OCAMLOPT checker/checkInductive.ml OCAMLOPT kernel/safe_typing.ml OCAMLC plugins/ssr/ssrfwd.mli OCAMLC plugins/ssr/ssrparser.mli OCAMLOPT checker/mod_checking.ml OCAMLC plugins/ssr/ssrfwd.ml OCAMLC plugins/ssr/ssrparser.ml OCAMLOPT -a -o kernel/kernel.cmxa OCAMLOPT library/global.ml OCAMLOPT checker/safe_checking.ml OCAMLOPT checker/check.ml OCAMLOPT library/lib.ml OCAMLOPT engine/univGen.ml OCAMLOPT tactics/declareUctx.ml OCAMLOPT stm/asyncTaskQueue.ml OCAMLOPT checker/checker.ml OCAMLOPT library/states.ml OCAMLOPT library/goptions.ml OCAMLOPT library/coqlib.ml OCAMLOPT pretyping/keys.ml OCAMLOPT interp/decls.ml OCAMLOPT tactics/declareScheme.ml OCAMLOPT -a -o checker/check.cmxa OCAMLOPT -a -o library/library.cmxa OCAMLOPT engine/univMinim.ml OCAMLOPT proofs/goal_select.ml OCAMLOPT vernac/attributes.ml OCAMLOPT plugins/micromega/certificate.ml OCAMLOPT plugins/rtauto/proof_search.ml OCAMLC -pack -o plugins/ssr/ssreflect_plugin.cmo OCAMLOPT -o bin/coqchk OCAMLOPT engine/uState.ml OCAMLC plugins/ssrsearch/g_search.ml OCAMLOPT engine/univops.ml OCAMLOPT engine/evd.ml OCAMLOPT engine/eConstr.ml OCAMLOPT engine/proofview_monad.ml OCAMLOPT engine/namegen.ml OCAMLOPT pretyping/pretype_errors.ml OCAMLOPT pretyping/typeclasses_errors.ml OCAMLOPT engine/termops.ml OCAMLOPT pretyping/glob_term.ml OCAMLOPT proofs/tactypes.ml OCAMLOPT proofs/miscprint.ml OCAMLOPT interp/constrexpr.ml OCAMLOPT interp/notation_term.ml OCAMLOPT parsing/extend.ml OCAMLOPT engine/evarutil.ml OCAMLOPT pretyping/find_subterm.ml OCAMLOPT tactics/term_dnet.ml OCAMLOPT engine/proofview.ml OCAMLOPT pretyping/reductionops.ml OCAMLOPT pretyping/program.ml OCAMLOPT engine/ftactic.ml OCAMLOPT proofs/goal.ml OCAMLOPT tactics/ind_tables.ml OCAMLOPT vernac/retrieveObl.ml OCAMLOPT -a -o engine/engine.cmxa OCAMLOPT pretyping/geninterp.ml OCAMLOPT pretyping/inductiveops.ml OCAMLOPT pretyping/cbv.ml OCAMLOPT pretyping/evardefine.ml OCAMLOPT pretyping/recordops.ml OCAMLOPT pretyping/ltac_pretype.ml OCAMLOPT interp/stdarg.ml OCAMLOPT printing/genprint.ml OCAMLOPT vernac/canonical.ml OCAMLOPT vernac/recLemmas.ml OCAMLOPT plugins/firstorder/unify.ml OCAMLOPT user-contrib/Ltac2/tac2ffi.ml OCAMLOPT pretyping/arguments_renaming.ml OCAMLOPT pretyping/nativenorm.ml OCAMLOPT pretyping/glob_ops.ml OCAMLOPT parsing/pcoq.ml OCAMLOPT printing/pputils.ml OCAMLOPT user-contrib/Ltac2/tac2extffi.ml OCAMLOPT pretyping/retyping.ml OCAMLOPT interp/impargs.ml OCAMLOPT parsing/g_prim.ml OCAMLOPT pretyping/evarsolve.ml OCAMLOPT pretyping/vnorm.ml OCAMLOPT pretyping/patternops.ml OCAMLOPT pretyping/typeclasses.ml OCAMLOPT pretyping/indrec.ml OCAMLOPT pretyping/globEnv.ml OCAMLOPT interp/dumpglob.ml OCAMLOPT tactics/btermdn.ml OCAMLOPT pretyping/constr_matching.ml OCAMLOPT pretyping/evarconv.ml OCAMLOPT tactics/eqschemes.ml OCAMLOPT tactics/elimschemes.ml OCAMLOPT pretyping/detyping.ml OCAMLOPT tactics/hipattern.ml OCAMLOPT user-contrib/Ltac2/tac2match.ml OCAMLOPT plugins/firstorder/formula.ml OCAMLOPT pretyping/typing.ml OCAMLOPT interp/genintern.ml OCAMLOPT interp/notation_ops.ml OCAMLOPT user-contrib/Ltac2/tac2env.ml OCAMLOPT tactics/genredexpr.ml OCAMLOPT tactics/redops.ml OCAMLOPT tactics/ppred.ml OCAMLOPT pretyping/tacred.ml OCAMLOPT proofs/refine.ml OCAMLOPT user-contrib/Ltac2/tac2interp.ml OCAMLOPT pretyping/coercionops.ml OCAMLOPT tactics/redexpr.ml OCAMLOPT interp/reserve.ml OCAMLOPT pretyping/coercion.ml OCAMLOPT interp/notation.ml OCAMLOPT pretyping/cases.ml OCAMLOPT interp/syntax_def.ml OCAMLOPT parsing/notation_gram.ml OCAMLOPT parsing/notgram_ops.ml OCAMLOPT parsing/ppextend.ml OCAMLOPT vernac/egramcoq.ml OCAMLOPT interp/smartlocate.ml OCAMLOPT pretyping/pretyping.ml OCAMLOPT pretyping/unification.ml OCAMLOPT interp/constrexpr_ops.ml OCAMLOPT proofs/evar_refiner.ml OCAMLOPT vernac/declareUniv.ml OCAMLOPT proofs/proof.ml OCAMLOPT proofs/logic.ml OCAMLOPT proofs/proof_bullet.ml OCAMLOPT interp/implicit_quantifiers.ml OCAMLOPT parsing/g_constr.ml OCAMLOPT user-contrib/Ltac2/tac2quote.ml OCAMLOPT interp/constrintern.ml OCAMLOPT proofs/refiner.ml OCAMLOPT -a -o pretyping/pretyping.cmxa OCAMLOPT proofs/tacmach.ml OCAMLOPT proofs/clenv.ml OCAMLOPT proofs/clenvtac.ml OCAMLOPT -a -o proofs/proofs.cmxa OCAMLOPT interp/modintern.ml OCAMLOPT interp/constrextern.ml OCAMLOPT plugins/syntax/string_notation.ml OCAMLOPT plugins/syntax/numeral.ml OCAMLOPT -a -o parsing/parsing.cmxa OCAMLOPT -a -o interp/interp.cmxa OCAMLOPT printing/ppconstr.ml OCAMLOPT printing/proof_diffs.ml OCAMLOPT printing/printer.ml OCAMLOPT printing/printmod.ml OCAMLOPT tactics/tacticals.ml OCAMLOPT vernac/himsg.ml OCAMLOPT tactics/hints.ml OCAMLOPT plugins/cc/ccalgo.ml OCAMLOPT user-contrib/Ltac2/tac2print.ml OCAMLOPT -a -o printing/printing.cmxa OCAMLOPT tactics/tactics.ml OCAMLOPT vernac/declaremods.ml OCAMLOPT plugins/cc/ccproof.ml OCAMLOPT plugins/firstorder/sequent.ml OCAMLOPT vernac/vernacexpr.ml OCAMLOPT vernac/library.ml OCAMLOPT vernac/pvernac.ml OCAMLOPT vernac/vernacprop.ml OCAMLOPT vernac/mltop.ml OCAMLOPT vernac/comArguments.ml OCAMLOPT toplevel/g_toplevel.ml OCAMLOPT plugins/extraction/table.ml OCAMLOPT vernac/g_vernac.ml OCAMLOPT vernac/egramml.ml OCAMLOPT vernac/assumptions.ml OCAMLOPT vernac/loadpath.ml OCAMLOPT plugins/extraction/mlutil.ml OCAMLOPT plugins/syntax/int63_syntax.ml OCAMLOPT plugins/syntax/float_syntax.ml OCAMLOPT plugins/syntax/r_syntax.ml OCAMLOPT tactics/abstract.ml OCAMLOPT tactics/elim.ml OCAMLOPT tactics/equality.ml OCAMLOPT tactics/contradiction.ml OCAMLOPT tactics/auto.ml OCAMLOPT vernac/ppvernac.ml OCAMLOPT plugins/firstorder/rules.ml OCAMLOPT plugins/micromega/coq_micromega.ml OCAMLOPT plugins/extraction/modutil.ml OCAMLOPT plugins/extraction/extraction.ml OCAMLOPT plugins/extraction/common.ml OCAMLOPT -pack -o plugins/syntax/int63_syntax_plugin.cmx OCAMLOPT -pack -o plugins/syntax/float_syntax_plugin.cmx OCAMLOPT -pack -o plugins/syntax/r_syntax_plugin.cmx OCAMLOPT plugins/btauto/refl_btauto.ml OCAMLOPT plugins/nsatz/nsatz.ml OCAMLOPT tactics/inv.ml OCAMLOPT tactics/eauto.ml OCAMLOPT tactics/eqdecide.ml OCAMLOPT tactics/autorewrite.ml OCAMLOPT vernac/metasyntax.ml OCAMLOPT vernac/topfmt.ml OCAMLOPT plugins/ltac/tacexpr.ml OCAMLOPT plugins/cc/cctac.ml OCAMLOPT plugins/firstorder/instances.ml OCAMLOPT plugins/omega/coq_omega.ml OCAMLOPT plugins/extraction/ocaml.ml OCAMLOPT plugins/extraction/haskell.ml OCAMLOPT plugins/extraction/scheme.ml OCAMLOPT plugins/extraction/json.ml OCAMLOPT -shared -o plugins/syntax/int63_syntax_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/float_syntax_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/r_syntax_plugin.cmxs OCAMLOPT tactics/class_tactics.ml OCAMLOPT toplevel/coqcargs.ml OCAMLOPT plugins/ltac/tacarg.ml OCAMLOPT plugins/ltac/tactic_matching.ml OCAMLOPT plugins/ltac/tacsubst.ml OCAMLOPT plugins/ltac/pltac.ml OCAMLOPT plugins/ltac/tacenv.ml OCAMLOPT -a -o tactics/tactics.cmxa OCAMLOPT plugins/ltac/pptactic.ml OCAMLOPT plugins/ltac/taccoerce.ml OCAMLOPT plugins/ltac/tactic_debug.ml OCAMLOPT plugins/ltac/tacintern.ml OCAMLOPT vernac/proof_using.ml OCAMLOPT vernac/declare.ml OCAMLOPT vernac/g_proofs.ml OCAMLOPT vernac/locality.ml OCAMLOPT vernac/comHints.ml OCAMLOPT vernac/comCoercion.ml OCAMLOPT vernac/auto_ind_decl.ml OCAMLOPT vernac/comPrimitive.ml OCAMLOPT vernac/proof_global.ml OCAMLOPT vernac/pfedit.ml OCAMLOPT vernac/declareDef.ml OCAMLOPT plugins/ltac/leminv.ml OCAMLOPT plugins/extraction/extract_env.ml OCAMLOPT vernac/declareObl.ml OCAMLOPT vernac/indschemes.ml OCAMLOPT vernac/lemmas.ml OCAMLOPT vernac/declareInd.ml OCAMLOPT vernac/vernacextend.ml OCAMLOPT vernac/obligations.ml OCAMLOPT vernac/comFixpoint.ml OCAMLOPT vernac/vernacstate.ml OCAMLOPT plugins/derive/derive.ml OCAMLOPT vernac/search.ml OCAMLOPT vernac/prettyp.ml OCAMLOPT vernac/comInductive.ml OCAMLOPT vernac/comProgramFixpoint.ml OCAMLOPT plugins/syntax/g_string.ml OCAMLOPT plugins/syntax/g_numeral.ml OCAMLOPT plugins/funind/indfun_common.ml OCAMLOPT plugins/derive/g_derive.ml OCAMLOPT vernac/comDefinition.ml OCAMLOPT vernac/classes.ml OCAMLOPT vernac/comSearch.ml OCAMLOPT -pack -o plugins/syntax/string_notation_plugin.cmx OCAMLOPT -pack -o plugins/syntax/numeral_notation_plugin.cmx OCAMLOPT plugins/funind/glob_termops.ml OCAMLOPT plugins/funind/functional_principles_types.ml OCAMLOPT plugins/funind/invfun.ml OCAMLOPT plugins/funind/indfun.ml OCAMLOPT -pack -o plugins/derive/derive_plugin.cmx OCAMLOPT vernac/comAssumption.ml OCAMLOPT vernac/record.ml OCAMLOPT -shared -o plugins/syntax/string_notation_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/numeral_notation_plugin.cmxs OCAMLOPT plugins/funind/glob_term_to_relation.ml OCAMLOPT -shared -o plugins/derive/derive_plugin.cmxs OCAMLOPT vernac/vernacentries.ml OCAMLOPT vernac/vernacinterp.ml OCAMLOPT -a -o vernac/vernac.cmxa OCAMLOPT stm/vernac_classifier.ml OCAMLOPT stm/stm.ml OCAMLOPT stm/proofBlockDelimiter.ml OCAMLOPT stm/vio_checking.ml OCAMLOPT toplevel/vernac.ml OCAMLOPT plugins/ltac/profile_ltac.ml OCAMLOPT toplevel/coqinit.ml OCAMLOPT -a -o stm/stm.cmxa OCAMLOPT toplevel/coqargs.ml OCAMLOPT plugins/ltac/tacinterp.ml OCAMLOPT toplevel/coqloop.ml OCAMLOPT toplevel/ccompile.ml OCAMLOPT toplevel/coqtop.ml OCAMLOPT toplevel/workerLoop.ml OCAMLOPT toplevel/coqc.ml OCAMLOPT -a -o toplevel/toplevel.cmxa OCAMLOPT plugins/ltac/tacentries.ml OCAMLOPT plugins/ltac/evar_tactics.ml OCAMLOPT plugins/ltac/tactic_option.ml OCAMLOPT plugins/ltac/rewrite.ml COQMKTOP -o bin/coqtop.opt COQMKTOP -o bin/coqproofworker.opt COQMKTOP -o bin/coqtacticworker.opt COQMKTOP -o bin/coqqueryworker.opt COQMKTOP -o bin/coqidetop.opt COQMKTOP -o bin/coqc.opt OCAMLOPT plugins/ltac/extraargs.ml OCAMLOPT plugins/ltac/profile_ltac_tactics.ml OCAMLOPT plugins/ltac/g_auto.ml OCAMLOPT plugins/ltac/g_class.ml OCAMLOPT plugins/ltac/g_rewrite.ml OCAMLOPT plugins/ltac/g_eqdecide.ml OCAMLOPT plugins/ltac/g_tactic.ml OCAMLOPT plugins/ltac/g_ltac.ml rm -f bin/coqtop && cp bin/coqtop.opt bin/coqtop rm -f bin/coqc && cp bin/coqc.opt bin/coqc OCAMLOPT plugins/ltac/g_obligations.ml OCAMLOPT plugins/ltac/coretactics.ml OCAMLOPT plugins/ltac/extratactics.ml rm -f bin/coqidetop && cp bin/coqidetop.opt bin/coqidetop COQC -noinit theories/Init/Notations.v OCAMLBEST -o bin/fake_ide OCAMLOPT -pack -o plugins/ltac/ltac_plugin.cmx OCAMLOPT -shared -o plugins/ltac/ltac_plugin.cmxs OCAMLOPT plugins/ltac/tauto.ml OCAMLOPT plugins/cc/g_congruence.ml OCAMLOPT plugins/firstorder/ground.ml OCAMLOPT plugins/setoid_ring/newring_ast.ml OCAMLOPT plugins/micromega/zify.ml OCAMLOPT plugins/micromega/g_micromega.ml OCAMLOPT plugins/extraction/g_extraction.ml OCAMLOPT plugins/omega/g_omega.ml OCAMLOPT plugins/btauto/g_btauto.ml OCAMLOPT plugins/ssrmatching/ssrmatching.ml OCAMLOPT plugins/nsatz/g_nsatz.ml OCAMLOPT plugins/rtauto/refl_tauto.ml OCAMLOPT user-contrib/Ltac2/tac2intern.ml COQC -noinit theories/Init/Ltac.v OCAMLOPT -pack -o plugins/ltac/tauto_plugin.cmx /scratch/work/lang/coq/work/coq-8.12.2/plugins/ltac/ltac_plugin.cmxs: text relocations File "./theories/Init/Ltac.v", line 11, characters 0-32: Error: Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/scratch/work/lang/coq/work/coq-8.12.2/plugins/ltac/ltac_plugin.cmxs: Cannot write-enable text segment: Permission denied\")") gmake[1]: *** [Makefile.build:869: theories/Init/Ltac.vo] Error 1 gmake[1]: *** Waiting for unfinished jobs.... gmake[1]: Leaving directory '/scratch/work/lang/coq/work/coq-8.12.2' gmake: *** [Makefile.make:178: submake] Error 2 *** Error code 2 Stop. make[1]: stopped in /tree/pkgsrc/lang/coq *** Error code 1 Stop. make: stopped in /tree/pkgsrc/lang/coq