=> Bootstrap dependency digest>=20211023: found digest-20220214 ===> 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.2nb3 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 '/usr/pkgsrc/lang/coq/work/coq-8.12.2' OCAMLC clib/segmenttree.mli OCAMLOPT clib/segmenttree.ml OCAMLC clib/segmenttree.ml OCAMLC clib/unicodetable.ml OCAMLOPT clib/unicodetable.ml OCAMLC clib/unicode.mli OCAMLOPT clib/unicode.ml OCAMLC clib/unicode.ml OCAMLC clib/minisys.ml OCAMLOPT clib/minisys.ml OCAMLC tools/coqdep_lexer.mli OCAMLLEX tools/coqdep_lexer.mll 217 states, 2223 transitions, table size 10194 bytes OCAMLOPT tools/coqdep_lexer.ml OCAMLC tools/coqdep_common.mli OCAMLOPT tools/coqdep_common.ml OCAMLC tools/coqdep_boot.ml OCAMLOPT tools/coqdep_boot.ml OCAMLBEST -o bin/coqdep_boot COQDEP VFILES OCAMLC kernel/genOpcodeFiles.ml WRITE kernel/byterun/coq_instruct.h WRITE kernel/byterun/coq_jumptbl.h CCDEP kernel/byterun/coq_values.c CCDEP kernel/byterun/coq_memory.c CCDEP kernel/byterun/coq_interp.c CCDEP kernel/byterun/coq_fix_code.c OCAMLLEX tools/ocamllibdep.mll 14 states, 417 transitions, table size 1752 bytes OCAMLC tools/ocamllibdep.ml OCAMLOPT tools/ocamllibdep.ml OCAMLBEST -o bin/ocamllibdep OCAMLC coqpp/coqpp_ast.mli OCAMLYACC coqpp/coqpp_parse.mly gmake[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. OCAMLC coqpp/coqpp_parse.mli OCAMLC coqpp/coqpp_parse.ml OCAMLLEX coqpp/coqpp_lex.mll 240 states, 15992 transitions, table size 65408 bytes OCAMLC coqpp/coqpp_lex.ml OCAMLC -a bin/coqpp mkdir -p gramlib/.pack OCAMLLEX ide/config_lexer.mll 30 states, 1657 transitions, table size 6808 bytes 6052 additional bytes used for bindings OCAMLLEX ide/coq_lex.mll 124 states, 1808 transitions, table size 7976 bytes OCAMLLEX ide/protocol/xml_lexer.mll 80 states, 774 transitions, table size 3576 bytes OCAMLLEX ide/utf8_convert.mll 15 states, 827 transitions, table size 3398 bytes OCAMLLEX tools/coqdoc/cpretty.mll 2714 states, 8784 transitions, table size 51420 bytes 17613 additional bytes used for bindings OCAMLLEX tools/coqwc.mll 244 states, 858 transitions, table size 4896 bytes 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_auto.mlg COQPP plugins/ltac/g_class.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 printf '# 1 "%s"\n' gramlib/ploc.ml > gramlib/.pack/gramlib__Ploc.ml cat gramlib/ploc.ml >> gramlib/.pack/gramlib__Ploc.ml printf '# 1 "%s"\n' gramlib/plexing.ml > gramlib/.pack/gramlib__Plexing.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 cat 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 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 WRITE kernel/copcodes.ml rm -f kernel/uint63.ml && cp kernel/uint63_31.ml kernel/uint63.ml && chmod a-w kernel/uint63.ml printf '# 1 "%s"\n' gramlib/ploc.mli > gramlib/.pack/gramlib__Ploc.mli cat gramlib/ploc.mli >> gramlib/.pack/gramlib__Ploc.mli printf '# 1 "%s"\n' gramlib/plexing.mli > gramlib/.pack/gramlib__Plexing.mli cat gramlib/plexing.mli >> gramlib/.pack/gramlib__Plexing.mli printf '# 1 "%s"\n' gramlib/gramext.mli > gramlib/.pack/gramlib__Gramext.mli cat gramlib/gramext.mli >> gramlib/.pack/gramlib__Gramext.mli printf '# 1 "%s"\n' gramlib/grammar.mli > gramlib/.pack/gramlib__Grammar.mli cat gramlib/grammar.mli >> gramlib/.pack/gramlib__Grammar.mli 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 OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES OCAMLDEP checker/MLFILES checker/MLIFILES gmake[1]: Circular coqpp/coqpp_parse.cmi <- coqpp/coqpp_parse.cmo dependency dropped. OCAMLC config/coq_config.mli OCAMLOPT config/coq_config.ml OCAMLOPT -a -o config/config.cmxa OCAMLC clib/cObj.mli OCAMLOPT clib/cObj.ml OCAMLC clib/cEphemeron.mli OCAMLOPT clib/cEphemeron.ml OCAMLC clib/cSig.mli OCAMLC clib/cMap.mli OCAMLOPT clib/cMap.ml OCAMLC clib/int.mli OCAMLOPT clib/int.ml OCAMLC clib/hashset.mli OCAMLOPT clib/hashset.ml OCAMLC clib/hashcons.mli OCAMLOPT clib/hashcons.ml OCAMLC clib/orderedType.mli OCAMLOPT clib/orderedType.ml OCAMLC clib/cSet.mli OCAMLOPT clib/cSet.ml OCAMLC clib/cList.mli OCAMLOPT clib/cList.ml OCAMLC clib/cString.mli OCAMLOPT clib/cString.ml OCAMLC clib/range.mli OCAMLOPT clib/range.ml OCAMLC clib/hMap.mli OCAMLOPT clib/hMap.ml OCAMLC clib/bigint.mli OCAMLOPT clib/bigint.ml OCAMLC clib/cArray.mli OCAMLOPT clib/cArray.ml OCAMLC clib/option.mli OCAMLOPT clib/option.ml OCAMLC clib/cUnix.mli OCAMLOPT clib/cUnix.ml OCAMLC clib/cThread.mli OCAMLOPT clib/cThread.ml OCAMLC clib/trie.mli OCAMLOPT clib/trie.ml OCAMLC clib/predicate.mli OCAMLOPT clib/predicate.ml OCAMLC clib/heap.mli OCAMLOPT clib/heap.ml OCAMLC clib/unionfind.mli OCAMLOPT clib/unionfind.ml OCAMLC clib/dyn.mli OCAMLOPT clib/dyn.ml OCAMLC clib/store.mli OCAMLOPT clib/store.ml OCAMLC clib/exninfo.mli OCAMLOPT clib/exninfo.ml OCAMLC clib/iStream.mli OCAMLOPT clib/iStream.ml OCAMLC clib/terminal.mli OCAMLOPT clib/terminal.ml OCAMLC clib/monad.mli OCAMLOPT clib/monad.ml OCAMLC clib/diff2.mli OCAMLOPT clib/diff2.ml OCAMLOPT -a -o clib/clib.cmxa OCAMLC lib/hook.mli OCAMLOPT lib/hook.ml OCAMLC lib/flags.mli OCAMLOPT lib/flags.ml OCAMLC lib/control.mli OCAMLOPT lib/control.ml OCAMLC lib/util.mli OCAMLOPT lib/util.ml OCAMLC lib/pp.mli OCAMLOPT lib/pp.ml OCAMLC lib/pp_diff.mli OCAMLOPT lib/pp_diff.ml OCAMLC lib/loc.mli OCAMLOPT lib/loc.ml OCAMLC lib/stateid.mli OCAMLOPT lib/stateid.ml OCAMLC lib/xml_datatype.mli OCAMLC lib/feedback.mli OCAMLOPT lib/feedback.ml OCAMLC lib/cErrors.mli OCAMLOPT lib/cErrors.ml OCAMLC lib/cWarnings.mli OCAMLOPT lib/cWarnings.ml OCAMLC lib/acyclicGraph.mli OCAMLOPT lib/acyclicGraph.ml OCAMLC lib/rtree.mli OCAMLOPT lib/rtree.ml OCAMLC lib/system.mli OCAMLOPT lib/system.ml OCAMLC lib/objFile.mli OCAMLOPT lib/objFile.ml OCAMLC lib/explore.mli OCAMLOPT lib/explore.ml OCAMLC lib/cProfile.mli OCAMLOPT lib/cProfile.ml OCAMLC lib/future.mli OCAMLOPT lib/future.ml OCAMLC lib/spawn.mli OCAMLOPT lib/spawn.ml OCAMLC lib/cAst.mli OCAMLOPT lib/cAst.ml OCAMLC lib/dAst.mli OCAMLOPT lib/dAst.ml OCAMLC lib/genarg.mli OCAMLOPT lib/genarg.ml OCAMLC lib/remoteCounter.mli OCAMLOPT lib/remoteCounter.ml OCAMLC lib/aux_file.mli OCAMLOPT lib/aux_file.ml OCAMLC lib/envars.mli OCAMLOPT lib/envars.ml OCAMLC lib/coqProject_file.mli OCAMLOPT lib/coqProject_file.ml OCAMLOPT -a -o lib/lib.cmxa OCAMLC kernel/names.mli OCAMLOPT kernel/names.ml OCAMLC kernel/transparentState.mli OCAMLOPT kernel/transparentState.ml OCAMLC kernel/uint63.mli OCAMLOPT kernel/uint63.ml OCAMLC kernel/float64.mli OCAMLOPT kernel/float64.ml OCAMLC kernel/cPrimitives.mli OCAMLOPT kernel/cPrimitives.ml OCAMLC kernel/univ.mli OCAMLOPT kernel/univ.ml OCAMLC kernel/uGraph.mli OCAMLOPT kernel/uGraph.ml OCAMLC kernel/esubst.mli OCAMLOPT kernel/esubst.ml OCAMLC kernel/sorts.mli OCAMLOPT kernel/sorts.ml OCAMLC kernel/evar.mli OCAMLOPT kernel/evar.ml OCAMLC kernel/context.mli OCAMLOPT kernel/context.ml OCAMLC kernel/constr.mli OCAMLOPT kernel/constr.ml OCAMLC kernel/vars.mli OCAMLOPT kernel/vars.ml OCAMLC kernel/term.mli OCAMLOPT kernel/term.ml OCAMLC kernel/retroknowledge.mli OCAMLOPT kernel/retroknowledge.ml OCAMLC kernel/mod_subst.mli OCAMLOPT kernel/mod_subst.ml OCAMLC kernel/vmvalues.mli OCAMLOPT kernel/vmvalues.ml OCAMLC kernel/cbytecodes.mli OCAMLOPT kernel/cbytecodes.ml OCAMLC kernel/copcodes.ml OCAMLOPT kernel/copcodes.ml OCAMLC kernel/cemitcodes.mli OCAMLOPT kernel/cemitcodes.ml OCAMLC kernel/opaqueproof.mli OCAMLOPT kernel/opaqueproof.ml OCAMLC kernel/conv_oracle.mli OCAMLOPT kernel/conv_oracle.ml OCAMLC kernel/declarations.ml OCAMLOPT kernel/declarations.ml OCAMLC kernel/entries.ml OCAMLOPT kernel/entries.ml OCAMLC kernel/nativevalues.mli OCAMLOPT kernel/nativevalues.ml OCAMLC kernel/declareops.mli OCAMLOPT kernel/declareops.ml OCAMLC kernel/environ.mli OCAMLOPT kernel/environ.ml OCAMLC kernel/primred.mli OCAMLOPT kernel/primred.ml OCAMLC kernel/cClosure.mli OCAMLOPT kernel/cClosure.ml OCAMLC kernel/relevanceops.mli OCAMLOPT kernel/relevanceops.ml OCAMLC kernel/reduction.mli OCAMLOPT kernel/reduction.ml OCAMLC kernel/clambda.mli OCAMLOPT kernel/clambda.ml OCAMLC kernel/nativelambda.mli OCAMLOPT kernel/nativelambda.ml OCAMLC kernel/cbytegen.mli OCAMLOPT kernel/cbytegen.ml OCAMLC kernel/nativecode.mli OCAMLOPT kernel/nativecode.ml OCAMLC kernel/nativelib.mli OCAMLOPT kernel/nativelib.ml OCAMLC kernel/csymtable.mli OCAMLOPT kernel/csymtable.ml OCAMLC kernel/vm.mli OCAMLOPT kernel/vm.ml OCAMLC kernel/vconv.mli OCAMLOPT kernel/vconv.ml OCAMLC kernel/nativeconv.mli OCAMLOPT kernel/nativeconv.ml OCAMLC kernel/type_errors.mli OCAMLOPT kernel/type_errors.ml OCAMLC kernel/modops.mli OCAMLOPT kernel/modops.ml OCAMLC kernel/inductive.mli OCAMLOPT kernel/inductive.ml OCAMLC kernel/typeops.mli OCAMLOPT kernel/typeops.ml OCAMLC kernel/inferCumulativity.mli OCAMLOPT kernel/inferCumulativity.ml OCAMLC kernel/indTyping.mli OCAMLOPT kernel/indTyping.ml OCAMLC kernel/indtypes.mli OCAMLOPT kernel/indtypes.ml OCAMLC kernel/cooking.mli OCAMLOPT kernel/cooking.ml OCAMLC kernel/term_typing.mli OCAMLOPT kernel/term_typing.ml OCAMLC kernel/subtyping.mli OCAMLOPT kernel/subtyping.ml OCAMLC kernel/mod_typing.mli OCAMLOPT kernel/mod_typing.ml OCAMLC kernel/nativelibrary.mli OCAMLOPT kernel/nativelibrary.ml OCAMLC kernel/section.mli OCAMLOPT kernel/section.ml OCAMLC kernel/safe_typing.mli OCAMLOPT kernel/safe_typing.ml OCAMLOPT -a -o kernel/kernel.cmxa OCAMLC library/libnames.mli OCAMLOPT library/libnames.ml OCAMLC library/globnames.mli OCAMLOPT library/globnames.ml OCAMLC library/libobject.mli OCAMLOPT library/libobject.ml OCAMLC library/summary.mli OCAMLOPT library/summary.ml OCAMLC library/nametab.mli OCAMLOPT library/nametab.ml OCAMLC library/global.mli OCAMLOPT library/global.ml OCAMLC library/lib.mli OCAMLOPT library/lib.ml OCAMLC library/states.mli OCAMLOPT library/states.ml OCAMLC library/goptions.mli OCAMLOPT library/goptions.ml OCAMLC library/coqlib.mli OCAMLOPT library/coqlib.ml OCAMLOPT -a -o library/library.cmxa OCAMLC engine/univNames.mli OCAMLOPT engine/univNames.ml OCAMLC engine/univGen.mli OCAMLOPT engine/univGen.ml OCAMLC engine/univSubst.mli OCAMLOPT engine/univSubst.ml OCAMLC engine/univProblem.mli OCAMLOPT engine/univProblem.ml OCAMLC engine/univMinim.mli OCAMLOPT engine/univMinim.ml OCAMLC engine/uState.mli OCAMLOPT engine/uState.ml OCAMLC engine/univops.mli OCAMLOPT engine/univops.ml OCAMLC engine/nameops.mli OCAMLOPT engine/nameops.ml OCAMLC engine/evar_kinds.mli OCAMLOPT engine/evar_kinds.ml OCAMLC engine/evd.mli OCAMLOPT engine/evd.ml OCAMLC engine/eConstr.mli OCAMLOPT engine/eConstr.ml OCAMLC engine/namegen.mli OCAMLOPT engine/namegen.ml OCAMLC engine/termops.mli OCAMLOPT engine/termops.ml OCAMLC engine/evarutil.mli OCAMLOPT engine/evarutil.ml OCAMLC engine/logic_monad.mli OCAMLOPT engine/logic_monad.ml OCAMLC engine/proofview_monad.mli OCAMLOPT engine/proofview_monad.ml OCAMLC engine/proofview.mli OCAMLOPT engine/proofview.ml OCAMLC engine/ftactic.mli OCAMLOPT engine/ftactic.ml OCAMLOPT -a -o engine/engine.cmxa OCAMLC pretyping/geninterp.mli OCAMLOPT pretyping/geninterp.ml OCAMLC pretyping/locus.ml OCAMLOPT pretyping/locus.ml OCAMLC pretyping/locusops.mli OCAMLOPT pretyping/locusops.ml OCAMLC pretyping/pretype_errors.mli OCAMLOPT pretyping/pretype_errors.ml OCAMLC pretyping/reductionops.mli OCAMLOPT pretyping/reductionops.ml OCAMLC pretyping/inductiveops.mli OCAMLOPT pretyping/inductiveops.ml OCAMLC pretyping/arguments_renaming.mli OCAMLOPT pretyping/arguments_renaming.ml OCAMLC pretyping/retyping.mli OCAMLOPT pretyping/retyping.ml OCAMLC pretyping/vnorm.mli OCAMLOPT pretyping/vnorm.ml OCAMLC pretyping/nativenorm.mli OCAMLOPT pretyping/nativenorm.ml OCAMLC pretyping/cbv.mli OCAMLOPT pretyping/cbv.ml OCAMLC pretyping/find_subterm.mli OCAMLOPT pretyping/find_subterm.ml OCAMLC pretyping/evardefine.mli OCAMLOPT pretyping/evardefine.ml OCAMLC pretyping/evarsolve.mli OCAMLOPT pretyping/evarsolve.ml OCAMLC pretyping/recordops.mli OCAMLOPT pretyping/recordops.ml OCAMLC pretyping/heads.mli OCAMLOPT pretyping/heads.ml OCAMLC pretyping/evarconv.mli OCAMLOPT pretyping/evarconv.ml OCAMLC pretyping/typing.mli OCAMLOPT pretyping/typing.ml OCAMLC pretyping/glob_term.ml OCAMLOPT pretyping/glob_term.ml OCAMLC pretyping/ltac_pretype.ml OCAMLOPT pretyping/ltac_pretype.ml OCAMLC pretyping/glob_ops.mli OCAMLOPT pretyping/glob_ops.ml OCAMLC pretyping/pattern.ml OCAMLOPT pretyping/pattern.ml OCAMLC pretyping/patternops.mli OCAMLOPT pretyping/patternops.ml OCAMLC pretyping/constr_matching.mli OCAMLOPT pretyping/constr_matching.ml OCAMLC pretyping/tacred.mli OCAMLOPT pretyping/tacred.ml OCAMLC pretyping/typeclasses_errors.mli OCAMLOPT pretyping/typeclasses_errors.ml OCAMLC pretyping/typeclasses.mli OCAMLOPT pretyping/typeclasses.ml OCAMLC pretyping/coercionops.mli OCAMLOPT pretyping/coercionops.ml OCAMLC pretyping/program.mli OCAMLOPT pretyping/program.ml OCAMLC pretyping/coercion.mli OCAMLOPT pretyping/coercion.ml OCAMLC pretyping/detyping.mli OCAMLOPT pretyping/detyping.ml OCAMLC pretyping/indrec.mli OCAMLOPT pretyping/indrec.ml OCAMLC pretyping/globEnv.mli OCAMLOPT pretyping/globEnv.ml OCAMLC pretyping/cases.mli OCAMLOPT pretyping/cases.ml OCAMLC pretyping/pretyping.mli OCAMLOPT pretyping/pretyping.ml OCAMLC pretyping/keys.mli OCAMLOPT pretyping/keys.ml OCAMLC pretyping/unification.mli OCAMLOPT pretyping/unification.ml OCAMLOPT -a -o pretyping/pretyping.cmxa OCAMLC interp/deprecation.mli OCAMLOPT interp/deprecation.ml OCAMLC interp/numTok.mli OCAMLOPT interp/numTok.ml OCAMLC interp/constrexpr.ml OCAMLOPT interp/constrexpr.ml OCAMLC proofs/tactypes.ml OCAMLOPT proofs/tactypes.ml OCAMLC interp/notation_term.ml OCAMLC interp/genintern.mli OCAMLC interp/stdarg.mli OCAMLOPT interp/stdarg.ml OCAMLOPT interp/notation_term.ml OCAMLOPT interp/genintern.ml OCAMLC interp/notation_ops.mli OCAMLOPT interp/notation_ops.ml OCAMLC interp/notation.mli OCAMLOPT interp/notation.ml OCAMLC interp/syntax_def.mli OCAMLOPT interp/syntax_def.ml OCAMLC interp/smartlocate.mli OCAMLOPT interp/smartlocate.ml OCAMLC interp/constrexpr_ops.mli OCAMLOPT interp/constrexpr_ops.ml OCAMLC interp/decls.mli OCAMLOPT interp/decls.ml OCAMLC interp/dumpglob.mli OCAMLOPT interp/dumpglob.ml OCAMLC interp/reserve.mli OCAMLOPT interp/reserve.ml OCAMLC interp/impargs.mli OCAMLOPT interp/impargs.ml OCAMLC interp/implicit_quantifiers.mli OCAMLOPT interp/implicit_quantifiers.ml OCAMLC interp/constrintern.mli OCAMLOPT interp/constrintern.ml OCAMLC interp/modintern.mli OCAMLOPT interp/modintern.ml OCAMLC interp/constrextern.mli OCAMLOPT interp/constrextern.ml OCAMLOPT -a -o interp/interp.cmxa OCAMLC proofs/miscprint.mli OCAMLOPT proofs/miscprint.ml OCAMLC proofs/goal.mli OCAMLOPT proofs/goal.ml OCAMLC proofs/evar_refiner.mli OCAMLOPT proofs/evar_refiner.ml OCAMLC proofs/refine.mli OCAMLOPT proofs/refine.ml OCAMLC proofs/goal_select.mli OCAMLOPT proofs/goal_select.ml OCAMLC proofs/proof.mli OCAMLOPT proofs/proof.ml OCAMLC proofs/logic.mli OCAMLOPT proofs/logic.ml OCAMLC proofs/proof_bullet.mli OCAMLOPT proofs/proof_bullet.ml OCAMLC proofs/refiner.mli OCAMLOPT proofs/refiner.ml OCAMLC proofs/tacmach.mli OCAMLOPT proofs/tacmach.ml OCAMLC proofs/clenv.mli OCAMLOPT proofs/clenv.ml OCAMLC proofs/clenvtac.mli OCAMLOPT proofs/clenvtac.ml OCAMLOPT -a -o proofs/proofs.cmxa OCAMLC gramlib/.pack/gramlib.ml OCAMLOPT gramlib/.pack/gramlib.ml OCAMLC gramlib/.pack/gramlib__Ploc.mli OCAMLOPT gramlib/.pack/gramlib__Ploc.ml OCAMLC gramlib/.pack/gramlib__Plexing.mli OCAMLOPT gramlib/.pack/gramlib__Plexing.ml OCAMLC gramlib/.pack/gramlib__Gramext.mli OCAMLOPT gramlib/.pack/gramlib__Gramext.ml OCAMLC gramlib/.pack/gramlib__Grammar.mli OCAMLOPT gramlib/.pack/gramlib__Grammar.ml OCAMLOPT -a -o gramlib/.pack/gramlib.cmxa OCAMLC parsing/tok.mli OCAMLOPT parsing/tok.ml OCAMLC parsing/cLexer.mli OCAMLOPT parsing/cLexer.ml OCAMLC parsing/extend.ml OCAMLOPT parsing/extend.ml OCAMLC parsing/notation_gram.ml OCAMLOPT parsing/notation_gram.ml OCAMLC parsing/notgram_ops.mli OCAMLOPT parsing/notgram_ops.ml OCAMLC parsing/ppextend.mli OCAMLOPT parsing/ppextend.ml OCAMLC parsing/pcoq.mli OCAMLOPT parsing/pcoq.ml OCAMLC parsing/g_constr.ml OCAMLOPT parsing/g_constr.ml OCAMLC parsing/g_prim.ml OCAMLOPT parsing/g_prim.ml OCAMLOPT -a -o parsing/parsing.cmxa OCAMLC printing/genprint.mli OCAMLOPT printing/genprint.ml OCAMLC printing/pputils.mli OCAMLOPT printing/pputils.ml OCAMLC printing/ppconstr.mli OCAMLOPT printing/ppconstr.ml OCAMLC printing/proof_diffs.mli OCAMLOPT printing/proof_diffs.ml OCAMLC printing/printer.mli OCAMLOPT printing/printer.ml OCAMLC printing/printmod.mli OCAMLOPT printing/printmod.ml OCAMLOPT -a -o printing/printing.cmxa OCAMLC tactics/declareScheme.mli OCAMLOPT tactics/declareScheme.ml OCAMLC tactics/dnet.mli OCAMLOPT tactics/dnet.ml OCAMLC tactics/dn.mli OCAMLOPT tactics/dn.ml OCAMLC tactics/btermdn.mli OCAMLOPT tactics/btermdn.ml OCAMLC tactics/tacticals.mli OCAMLOPT tactics/tacticals.ml OCAMLC tactics/hipattern.mli OCAMLOPT tactics/hipattern.ml OCAMLC tactics/ind_tables.mli OCAMLOPT tactics/ind_tables.ml OCAMLC tactics/eqschemes.mli OCAMLOPT tactics/eqschemes.ml OCAMLC tactics/elimschemes.mli OCAMLOPT tactics/elimschemes.ml OCAMLC tactics/genredexpr.ml OCAMLOPT tactics/genredexpr.ml OCAMLC tactics/redops.mli OCAMLOPT tactics/redops.ml OCAMLC tactics/redexpr.mli OCAMLOPT tactics/redexpr.ml OCAMLC tactics/ppred.mli OCAMLOPT tactics/ppred.ml OCAMLC tactics/tactics.mli OCAMLOPT tactics/tactics.ml OCAMLC tactics/abstract.mli OCAMLOPT tactics/abstract.ml OCAMLC tactics/elim.mli OCAMLOPT tactics/elim.ml OCAMLC tactics/equality.mli OCAMLOPT tactics/equality.ml OCAMLC tactics/contradiction.mli OCAMLOPT tactics/contradiction.ml OCAMLC tactics/inv.mli OCAMLOPT tactics/inv.ml OCAMLC tactics/declareUctx.mli OCAMLOPT tactics/declareUctx.ml OCAMLC tactics/hints.mli OCAMLOPT tactics/hints.ml OCAMLC tactics/auto.mli OCAMLOPT tactics/auto.ml OCAMLC tactics/eauto.mli OCAMLOPT tactics/eauto.ml OCAMLC tactics/class_tactics.mli OCAMLOPT tactics/class_tactics.ml OCAMLC tactics/term_dnet.mli OCAMLOPT tactics/term_dnet.ml OCAMLC tactics/eqdecide.mli OCAMLOPT tactics/eqdecide.ml OCAMLC tactics/autorewrite.mli OCAMLOPT tactics/autorewrite.ml OCAMLOPT -a -o tactics/tactics.cmxa OCAMLC vernac/declaremods.mli OCAMLOPT vernac/declaremods.ml OCAMLC vernac/attributes.mli OCAMLOPT vernac/attributes.ml OCAMLC vernac/vernacexpr.ml OCAMLOPT vernac/vernacexpr.ml OCAMLC vernac/pvernac.mli OCAMLOPT vernac/pvernac.ml OCAMLC vernac/g_vernac.ml OCAMLOPT vernac/g_vernac.ml OCAMLC vernac/retrieveObl.mli OCAMLOPT vernac/retrieveObl.ml OCAMLC vernac/egramml.mli OCAMLOPT vernac/egramml.ml OCAMLC vernac/ppvernac.mli OCAMLOPT vernac/ppvernac.ml OCAMLC vernac/proof_using.mli OCAMLOPT vernac/proof_using.ml OCAMLC vernac/egramcoq.mli OCAMLOPT vernac/egramcoq.ml OCAMLC vernac/metasyntax.mli OCAMLOPT vernac/metasyntax.ml OCAMLC vernac/himsg.mli OCAMLOPT vernac/himsg.ml OCAMLC vernac/declareUniv.mli OCAMLOPT vernac/declareUniv.ml OCAMLC vernac/declare.mli OCAMLOPT vernac/declare.ml OCAMLC vernac/g_proofs.ml OCAMLOPT vernac/g_proofs.ml OCAMLC vernac/vernacprop.mli OCAMLOPT vernac/vernacprop.ml OCAMLC vernac/locality.mli OCAMLOPT vernac/locality.ml OCAMLC vernac/declareObl.mli OCAMLOPT vernac/declareObl.ml OCAMLC vernac/lemmas.mli OCAMLOPT vernac/lemmas.ml OCAMLC vernac/vernacextend.mli OCAMLOPT vernac/vernacextend.ml OCAMLC vernac/comHints.mli OCAMLOPT vernac/comHints.ml OCAMLC vernac/canonical.mli OCAMLOPT vernac/canonical.ml OCAMLC vernac/recLemmas.mli OCAMLOPT vernac/recLemmas.ml OCAMLC vernac/library.mli OCAMLOPT vernac/library.ml OCAMLC vernac/comCoercion.mli OCAMLOPT vernac/comCoercion.ml OCAMLC vernac/auto_ind_decl.mli OCAMLOPT vernac/auto_ind_decl.ml OCAMLC vernac/indschemes.mli OCAMLOPT vernac/indschemes.ml OCAMLC vernac/obligations.mli OCAMLOPT vernac/obligations.ml OCAMLC vernac/comDefinition.mli OCAMLOPT vernac/comDefinition.ml OCAMLC vernac/classes.mli OCAMLOPT vernac/classes.ml OCAMLC vernac/comPrimitive.mli OCAMLOPT vernac/comPrimitive.ml OCAMLC vernac/comAssumption.mli OCAMLOPT vernac/comAssumption.ml OCAMLC vernac/declareInd.mli OCAMLOPT vernac/declareInd.ml OCAMLC vernac/search.mli OCAMLOPT vernac/search.ml OCAMLC vernac/comSearch.mli OCAMLOPT vernac/comSearch.ml OCAMLC vernac/prettyp.mli OCAMLOPT vernac/prettyp.ml OCAMLC vernac/comInductive.mli OCAMLOPT vernac/comInductive.ml OCAMLC vernac/comFixpoint.mli OCAMLOPT vernac/comFixpoint.ml OCAMLC vernac/comProgramFixpoint.mli OCAMLOPT vernac/comProgramFixpoint.ml OCAMLC vernac/record.mli OCAMLOPT vernac/record.ml OCAMLC vernac/assumptions.mli OCAMLOPT vernac/assumptions.ml OCAMLC vernac/mltop.mli OCAMLOPT vernac/mltop.ml OCAMLC vernac/topfmt.mli OCAMLOPT vernac/topfmt.ml OCAMLC vernac/loadpath.mli OCAMLOPT vernac/loadpath.ml OCAMLC vernac/comArguments.mli OCAMLOPT vernac/comArguments.ml OCAMLC vernac/vernacentries.mli OCAMLOPT vernac/vernacentries.ml OCAMLC vernac/vernacstate.mli OCAMLOPT vernac/vernacstate.ml OCAMLC vernac/vernacinterp.mli OCAMLOPT vernac/vernacinterp.ml OCAMLC vernac/proof_global.ml OCAMLOPT vernac/proof_global.ml OCAMLC vernac/pfedit.ml OCAMLOPT vernac/pfedit.ml OCAMLC vernac/declareDef.ml OCAMLOPT vernac/declareDef.ml OCAMLOPT -a -o vernac/vernac.cmxa OCAMLC stm/spawned.mli OCAMLOPT stm/spawned.ml OCAMLC stm/dag.mli OCAMLOPT stm/dag.ml OCAMLC stm/vcs.mli OCAMLOPT stm/vcs.ml OCAMLC stm/tQueue.mli OCAMLOPT stm/tQueue.ml OCAMLC stm/coqworkmgrApi.mli OCAMLOPT stm/coqworkmgrApi.ml OCAMLC stm/workerPool.mli OCAMLOPT stm/workerPool.ml OCAMLC stm/vernac_classifier.mli OCAMLOPT stm/vernac_classifier.ml OCAMLC stm/asyncTaskQueue.mli OCAMLOPT stm/asyncTaskQueue.ml OCAMLC stm/stm.mli OCAMLOPT stm/stm.ml OCAMLC stm/proofBlockDelimiter.mli OCAMLOPT stm/proofBlockDelimiter.ml OCAMLC stm/vio_checking.mli OCAMLOPT stm/vio_checking.ml OCAMLOPT -a -o stm/stm.cmxa OCAMLC toplevel/vernac.mli OCAMLOPT toplevel/vernac.ml OCAMLC toplevel/usage.mli OCAMLOPT toplevel/usage.ml OCAMLC toplevel/coqinit.mli OCAMLOPT toplevel/coqinit.ml OCAMLC toplevel/coqargs.mli OCAMLOPT toplevel/coqargs.ml OCAMLC toplevel/coqcargs.mli OCAMLOPT toplevel/coqcargs.ml OCAMLC toplevel/g_toplevel.ml OCAMLOPT toplevel/g_toplevel.ml OCAMLC toplevel/coqloop.mli OCAMLOPT toplevel/coqloop.ml OCAMLC toplevel/ccompile.mli OCAMLOPT toplevel/ccompile.ml OCAMLC toplevel/coqtop.mli OCAMLOPT toplevel/coqtop.ml OCAMLC toplevel/workerLoop.mli OCAMLOPT toplevel/workerLoop.ml OCAMLC toplevel/coqc.mli OCAMLOPT toplevel/coqc.ml OCAMLOPT -a -o toplevel/toplevel.cmxa 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) ^~~~~~~~~~~~~ cd kernel/byterun/ && \ "/usr/pkg/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o COQMKTOP -o bin/coqc.opt rm -f bin/coqc && cp bin/coqc.opt bin/coqc COQC -noinit theories/Init/Notations.v OCAMLC plugins/ltac/tacexpr.mli OCAMLOPT plugins/ltac/tacexpr.ml OCAMLC plugins/ltac/tacarg.mli OCAMLOPT plugins/ltac/tacarg.ml OCAMLC plugins/ltac/tacsubst.mli OCAMLOPT plugins/ltac/tacsubst.ml OCAMLC plugins/ltac/tacenv.mli OCAMLOPT plugins/ltac/tacenv.ml OCAMLC plugins/ltac/pptactic.mli OCAMLOPT plugins/ltac/pptactic.ml OCAMLC plugins/ltac/pltac.mli OCAMLOPT plugins/ltac/pltac.ml OCAMLC plugins/ltac/taccoerce.mli OCAMLOPT plugins/ltac/taccoerce.ml OCAMLC plugins/ltac/tactic_debug.mli OCAMLOPT plugins/ltac/tactic_debug.ml OCAMLC plugins/ltac/tacintern.mli OCAMLOPT plugins/ltac/tacintern.ml OCAMLC plugins/ltac/profile_ltac.mli OCAMLOPT plugins/ltac/profile_ltac.ml OCAMLC plugins/ltac/tactic_matching.mli OCAMLOPT plugins/ltac/tactic_matching.ml OCAMLC plugins/ltac/leminv.mli OCAMLOPT plugins/ltac/leminv.ml OCAMLC plugins/ltac/tacinterp.mli OCAMLOPT plugins/ltac/tacinterp.ml OCAMLC plugins/ltac/tacentries.mli OCAMLOPT plugins/ltac/tacentries.ml OCAMLC plugins/ltac/evar_tactics.mli OCAMLOPT plugins/ltac/evar_tactics.ml OCAMLC plugins/ltac/tactic_option.mli OCAMLOPT plugins/ltac/tactic_option.ml OCAMLC plugins/ltac/extraargs.mli OCAMLOPT plugins/ltac/extraargs.ml OCAMLC plugins/ltac/g_obligations.ml OCAMLOPT plugins/ltac/g_obligations.ml OCAMLC plugins/ltac/coretactics.ml OCAMLOPT plugins/ltac/coretactics.ml OCAMLC plugins/ltac/extratactics.mli OCAMLOPT plugins/ltac/extratactics.ml OCAMLC plugins/ltac/profile_ltac_tactics.ml OCAMLOPT plugins/ltac/profile_ltac_tactics.ml OCAMLC plugins/ltac/g_auto.ml OCAMLOPT plugins/ltac/g_auto.ml OCAMLC plugins/ltac/g_class.ml OCAMLOPT plugins/ltac/g_class.ml OCAMLC plugins/ltac/rewrite.mli OCAMLOPT plugins/ltac/rewrite.ml OCAMLC plugins/ltac/g_rewrite.ml OCAMLOPT plugins/ltac/g_rewrite.ml OCAMLC plugins/ltac/g_eqdecide.ml OCAMLOPT plugins/ltac/g_eqdecide.ml OCAMLC plugins/ltac/g_tactic.ml OCAMLOPT plugins/ltac/g_tactic.ml OCAMLC plugins/ltac/g_ltac.ml OCAMLOPT plugins/ltac/g_ltac.ml OCAMLOPT -pack -o plugins/ltac/ltac_plugin.cmx OCAMLOPT -shared -o plugins/ltac/ltac_plugin.cmxs COQC -noinit theories/Init/Ltac.v /usr/pkgsrc/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(\"/usr/pkgsrc/lang/coq/work/coq-8.12.2/plugins/ltac/ltac_plugin.cmxs: Unsupported relocation type 6 in non-PLT relocations\")") gmake[1]: *** [Makefile.build:869: theories/Init/Ltac.vo] Error 1 gmake[1]: Leaving directory '/usr/pkgsrc/lang/coq/work/coq-8.12.2' gmake: *** [Makefile.make:178: submake] Error 2 *** Error code 2 Stop. make[1]: stopped in /usr/pkgsrc/lang/coq *** Error code 1 Stop. make: stopped in /usr/pkgsrc/lang/coq