=> Bootstrap dependency digest>=20010302: found digest-20160304 ===> 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.7.2nb3 /usr/pkg/bin/gmake --warn-undefined-variable --no-builtin-rules -f Makefile.build world gmake[1]: Entering directory '/data/scratch/lang/coq/work/coq-8.7.2' OCAMLC lib/unicode.mli OCAMLC tools/coqdep_lexer.mli OCAMLLEX tools/coqdep_lexer.mll OCAMLC tools/coqdep_common.mli OCAMLC lib/segmenttree.mli sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ -e '/^}/q' kernel/byterun/coq_instruct.h > "kernel/byterun/coq_jumptbl.h" || (RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV}) tr -d "\r" < kernel/byterun/coq_instruct.h | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | \ awk -f kernel/make-opcodes > "kernel/copcodes.ml" || (RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV}) OCAMLLEX tools/ocamllibdep.mll OCAMLLEX ide/config_lexer.mll OCAMLLEX ide/coq_lex.mll OCAMLLEX ide/xml_lexer.mll OCAMLLEX tools/gallina_lexer.mll OCAMLLEX tools/coqdoc/cpretty.mll OCAMLLEX tools/coqwc.mll ECHO... > tools/tolink.ml OCAMLLEX ide/utf8_convert.mll 314 states, 4454 transitions, table size 19700 bytes 2927 additional bytes used for bindings OCAMLDEP checker/univ.mli 80 states, 774 transitions, table size 3576 bytes 15 states, 827 transitions, table size 3398 bytes 14 states, 417 transitions, table size 1752 bytes 30 states, 1657 transitions, table size 6808 bytes 6052 additional bytes used for bindings OCAMLDEP checker/typeops.mli OCAMLDEP checker/type_errors.mli 85 states, 821 transitions, table size 3794 bytes 189 states, 503 transitions, table size 3146 bytes OCAMLDEP checker/term.mli OCAMLDEP checker/subtyping.mli 244 states, 858 transitions, table size 4896 bytes OCAMLDEP checker/safe_typing.mli OCAMLDEP checker/reduction.mli OCAMLDEP checker/modops.mli OCAMLDEP checker/names.mli OCAMLDEP checker/mod_checking.mli OCAMLDEP checker/inductive.mli OCAMLDEP checker/indtypes.mli OCAMLDEP checker/esubst.mli OCAMLDEP checker/environ.mli OCAMLDEP checker/declarations.mli OCAMLDEP checker/closure.mli OCAMLDEP checker/cic.mli OCAMLDEP checker/check_stat.mli OCAMLDEP checker/analyze.mli OCAMLC -c grammar/q_util.mli CAMLP4O ide/coqide_main.ml4 OCAMLDEP checker/names.ml OCAMLDEP checker/esubst.ml OCAMLDEP checker/votour.ml OCAMLDEP checker/values.ml OCAMLDEP checker/validate.ml OCAMLDEP checker/univ.ml 2654 states, 8247 transitions, table size 48912 bytes OCAMLDEP checker/typeops.ml OCAMLDEP checker/term.ml OCAMLDEP checker/subtyping.ml OCAMLDEP checker/print.ml OCAMLDEP checker/reduction.ml OCAMLDEP checker/modops.ml OCAMLDEP checker/type_errors.ml OCAMLDEP checker/safe_typing.ml OCAMLDEP checker/mod_checking.ml OCAMLDEP checker/main.ml OCAMLDEP checker/inductive.ml OCAMLDEP checker/indtypes.ml OCAMLDEP checker/environ.ml OCAMLDEP checker/declarations.ml OCAMLDEP checker/closure.ml OCAMLDEP checker/checker.ml OCAMLDEP checker/check_stat.ml OCAMLDEP checker/check.ml OCAMLDEP checker/analyze.ml OCAMLC lib/segmenttree.ml OCAMLOPT lib/segmenttree.ml OCAMLC tools/coqdep_boot.ml 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 OCAMLC tools/ocamllibdep.ml OCAMLDEP vernac/vernacprop.mli OCAMLDEP vernac/vernacinterp.mli OCAMLDEP vernac/vernacentries.mli OCAMLDEP vernac/obligations.mli OCAMLDEP vernac/topfmt.mli OCAMLDEP vernac/record.mli OCAMLDEP vernac/search.mli OCAMLDEP vernac/mltop.mli OCAMLDEP vernac/metasyntax.mli OCAMLDEP vernac/locality.mli OCAMLDEP vernac/lemmas.mli OCAMLDEP vernac/indschemes.mli OCAMLDEP vernac/himsg.mli OCAMLDEP vernac/explainErr.mli OCAMLDEP vernac/discharge.mli OCAMLDEP vernac/declareDef.mli OCAMLDEP vernac/command.mli OCAMLDEP vernac/classes.mli OCAMLDEP vernac/class.mli OCAMLDEP vernac/auto_ind_decl.mli OCAMLDEP toplevel/vernac.mli OCAMLDEP vernac/assumptions.mli OCAMLDEP toplevel/usage.mli OCAMLDEP toplevel/coqtop.mli OCAMLDEP toplevel/coqloop.mli OCAMLDEP toplevel/coqinit.mli OCAMLDEP tools/coqdoc/tokens.mli OCAMLDEP tools/coqdoc/output.mli OCAMLDEP tools/coqdoc/index.mli OCAMLDEP tools/coqdoc/cpretty.mli OCAMLDEP tools/coqdoc/cdglobals.mli OCAMLDEP tools/coqdoc/alpha.mli OCAMLDEP tools/coqdep_lexer.mli OCAMLDEP tools/coqdep_common.mli OCAMLDEP tactics/term_dnet.mli OCAMLDEP tactics/tactics.mli OCAMLDEP tactics/tacticals.mli OCAMLDEP tactics/leminv.mli OCAMLDEP tactics/inv.mli OCAMLDEP tactics/ind_tables.mli OCAMLDEP tactics/hipattern.mli OCAMLDEP tactics/hints.mli OCAMLDEP tactics/equality.mli OCAMLDEP tactics/eqschemes.mli OCAMLDEP tactics/eqdecide.mli OCAMLDEP tactics/elim.mli OCAMLDEP tactics/elimschemes.mli OCAMLDEP tactics/eauto.mli OCAMLDEP tactics/dnet.mli OCAMLDEP tactics/dn.mli OCAMLDEP tactics/contradiction.mli OCAMLDEP tactics/class_tactics.mli OCAMLDEP tactics/autorewrite.mli OCAMLDEP stm/workerPool.mli OCAMLDEP tactics/auto.mli OCAMLDEP tactics/btermdn.mli OCAMLDEP stm/vio_checking.mli OCAMLDEP stm/workerLoop.mli OCAMLDEP stm/vernac_classifier.mli OCAMLDEP stm/tQueue.mli OCAMLDEP stm/vcs.mli OCAMLDEP stm/spawned.mli OCAMLDEP stm/stm.mli OCAMLDEP stm/proofBlockDelimiter.mli OCAMLDEP stm/dag.mli OCAMLDEP stm/coqworkmgrApi.mli OCAMLDEP stm/asyncTaskQueue.mli OCAMLDEP proofs/tacmach.mli OCAMLDEP proofs/refiner.mli OCAMLDEP proofs/refine.mli OCAMLDEP proofs/redexpr.mli OCAMLDEP proofs/proof_using.mli OCAMLDEP proofs/proof_type.mli OCAMLDEP proofs/proof_global.mli OCAMLDEP proofs/proof.mli OCAMLDEP proofs/miscprint.mli OCAMLDEP proofs/pfedit.mli OCAMLDEP proofs/logic.mli OCAMLDEP proofs/goal.mli OCAMLDEP proofs/evar_refiner.mli OCAMLDEP proofs/clenvtac.mli OCAMLDEP proofs/clenv.mli OCAMLDEP printing/printmod.mli OCAMLDEP printing/printer.mli OCAMLDEP printing/prettyp.mli OCAMLDEP printing/ppvernac.mli OCAMLDEP printing/pputils.mli OCAMLDEP printing/ppconstr.mli OCAMLDEP printing/genprint.mli OCAMLDEP pretyping/vnorm.mli OCAMLDEP pretyping/unification.mli OCAMLDEP pretyping/typing.mli OCAMLDEP pretyping/typeclasses_errors.mli OCAMLDEP pretyping/typeclasses.mli OCAMLDEP pretyping/tacred.mli OCAMLDEP pretyping/retyping.mli OCAMLDEP pretyping/redops.mli OCAMLDEP pretyping/reductionops.mli OCAMLDEP pretyping/recordops.mli OCAMLDEP pretyping/program.mli OCAMLDEP pretyping/pretyping.mli OCAMLDEP pretyping/pretype_errors.mli OCAMLDEP pretyping/nativenorm.mli OCAMLDEP pretyping/patternops.mli OCAMLDEP pretyping/miscops.mli OCAMLDEP pretyping/locusops.mli OCAMLDEP pretyping/inductiveops.mli OCAMLDEP pretyping/indrec.mli OCAMLDEP pretyping/find_subterm.mli OCAMLDEP pretyping/glob_ops.mli OCAMLDEP pretyping/evarsolve.mli OCAMLDEP pretyping/evardefine.mli OCAMLDEP pretyping/evarconv.mli OCAMLDEP pretyping/constr_matching.mli OCAMLDEP pretyping/detyping.mli OCAMLDEP pretyping/coercion.mli OCAMLDEP pretyping/classops.mli OCAMLDEP pretyping/cbv.mli OCAMLDEP pretyping/cases.mli OCAMLDEP pretyping/arguments_renaming.mli OCAMLDEP plugins/ssrmatching/ssrmatching.mli OCAMLDEP plugins/ssr/ssrview.mli OCAMLDEP plugins/ssr/ssrvernac.mli OCAMLDEP plugins/ssr/ssrtacticals.mli OCAMLDEP plugins/ssr/ssrprinters.mli OCAMLDEP plugins/ssr/ssrparser.mli OCAMLDEP plugins/ssr/ssripats.mli OCAMLDEP plugins/ssr/ssrequality.mli OCAMLDEP plugins/ssr/ssrfwd.mli OCAMLDEP plugins/ssr/ssrelim.mli OCAMLDEP plugins/ssr/ssrbwd.mli OCAMLDEP plugins/ssr/ssrast.mli OCAMLDEP plugins/setoid_ring/newring_ast.mli OCAMLDEP plugins/ssr/ssrcommon.mli OCAMLDEP plugins/rtauto/refl_tauto.mli OCAMLDEP plugins/setoid_ring/newring.mli OCAMLDEP plugins/rtauto/proof_search.mli OCAMLDEP plugins/nsatz/utile.mli OCAMLDEP plugins/romega/const_omega.mli OCAMLDEP plugins/nsatz/polynom.mli OCAMLDEP plugins/nsatz/nsatz.mli OCAMLDEP plugins/nsatz/ideal.mli OCAMLDEP plugins/micromega/sos_types.mli OCAMLDEP plugins/micromega/sos.mli OCAMLDEP plugins/micromega/micromega.mli OCAMLDEP plugins/ltac/tauto.mli OCAMLDEP plugins/ltac/tactic_matching.mli OCAMLDEP plugins/ltac/tactic_option.mli OCAMLDEP plugins/ltac/tactic_debug.mli OCAMLDEP plugins/ltac/tacsubst.mli OCAMLDEP plugins/ltac/tacinterp.mli OCAMLDEP plugins/ltac/tacexpr.mli OCAMLDEP plugins/ltac/tacenv.mli OCAMLDEP plugins/ltac/tacintern.mli OCAMLDEP plugins/ltac/tacentries.mli OCAMLDEP plugins/ltac/taccoerce.mli OCAMLDEP plugins/ltac/tacarg.mli OCAMLDEP plugins/ltac/rewrite.mli OCAMLDEP plugins/ltac/profile_ltac.mli OCAMLDEP plugins/ltac/pptactic.mli OCAMLDEP plugins/ltac/pltac.mli OCAMLDEP plugins/ltac/extratactics.mli OCAMLDEP plugins/ltac/extraargs.mli OCAMLDEP plugins/ltac/evar_tactics.mli OCAMLDEP plugins/funind/recdef.mli OCAMLDEP plugins/funind/indfun_common.mli OCAMLDEP plugins/funind/glob_termops.mli OCAMLDEP plugins/funind/glob_term_to_relation.mli OCAMLDEP plugins/funind/indfun.mli OCAMLDEP plugins/funind/functional_principles_types.mli OCAMLDEP plugins/funind/functional_principles_proofs.mli OCAMLDEP plugins/firstorder/unify.mli OCAMLDEP plugins/firstorder/sequent.mli OCAMLDEP plugins/firstorder/rules.mli OCAMLDEP plugins/firstorder/formula.mli OCAMLDEP plugins/firstorder/instances.mli OCAMLDEP plugins/firstorder/ground.mli OCAMLDEP plugins/extraction/table.mli OCAMLDEP plugins/extraction/scheme.mli OCAMLDEP plugins/extraction/modutil.mli OCAMLDEP plugins/extraction/ocaml.mli OCAMLDEP plugins/extraction/mlutil.mli OCAMLDEP plugins/extraction/miniml.mli OCAMLDEP plugins/extraction/json.mli OCAMLDEP plugins/extraction/haskell.mli OCAMLDEP plugins/extraction/extraction.mli OCAMLDEP plugins/extraction/extract_env.mli OCAMLDEP plugins/extraction/common.mli OCAMLDEP plugins/derive/derive.mli OCAMLDEP plugins/cc/cctac.mli OCAMLDEP plugins/cc/ccalgo.mli OCAMLDEP plugins/cc/ccproof.mli OCAMLDEP parsing/tok.mli OCAMLDEP parsing/pcoq.mli OCAMLDEP parsing/egramml.mli OCAMLDEP parsing/egramcoq.mli OCAMLDEP parsing/cLexer.mli OCAMLDEP library/univops.mli OCAMLDEP library/summary.mli OCAMLDEP library/states.mli OCAMLDEP library/nametab.mli OCAMLDEP library/nameops.mli OCAMLDEP library/loadpath.mli OCAMLDEP library/library.mli OCAMLDEP library/libobject.mli OCAMLDEP library/libnames.mli OCAMLDEP library/lib.mli OCAMLDEP library/kindops.mli OCAMLDEP library/heads.mli OCAMLDEP library/goptions.mli OCAMLDEP library/keys.mli OCAMLDEP library/globnames.mli OCAMLDEP library/dischargedhypsmap.mli OCAMLDEP library/decls.mli OCAMLDEP library/global.mli OCAMLDEP library/declaremods.mli OCAMLDEP library/coqlib.mli OCAMLDEP lib/util.mli OCAMLDEP lib/xml_datatype.mli OCAMLDEP lib/unionfind.mli OCAMLDEP lib/unicode.mli OCAMLDEP lib/trie.mli OCAMLDEP lib/terminal.mli OCAMLDEP lib/system.mli OCAMLDEP lib/store.mli OCAMLDEP lib/stateid.mli OCAMLDEP lib/spawn.mli OCAMLDEP lib/segmenttree.mli OCAMLDEP lib/rtree.mli OCAMLDEP lib/remoteCounter.mli OCAMLDEP lib/profile.mli OCAMLDEP lib/predicate.mli OCAMLDEP lib/pp.mli OCAMLDEP lib/option.mli OCAMLDEP lib/monad.mli OCAMLDEP lib/loc.mli OCAMLDEP lib/int.mli OCAMLDEP lib/iStream.mli OCAMLDEP lib/hook.mli OCAMLDEP lib/heap.mli OCAMLDEP lib/hashset.mli OCAMLDEP lib/hashcons.mli OCAMLDEP lib/hMap.mli OCAMLDEP lib/genarg.mli OCAMLDEP lib/future.mli OCAMLDEP lib/flags.mli OCAMLDEP lib/feedback.mli OCAMLDEP lib/explore.mli OCAMLDEP lib/exninfo.mli OCAMLDEP lib/envars.mli OCAMLDEP lib/dyn.mli OCAMLDEP lib/deque.mli OCAMLDEP lib/coqProject_file.mli OCAMLDEP lib/control.mli OCAMLDEP lib/canary.mli OCAMLDEP lib/cWarnings.mli OCAMLDEP lib/cUnix.mli OCAMLDEP lib/cString.mli OCAMLDEP lib/cThread.mli OCAMLDEP lib/cStack.mli OCAMLDEP lib/cSet.mli OCAMLDEP lib/cSig.mli OCAMLDEP lib/cObj.mli OCAMLDEP lib/cMap.mli OCAMLDEP lib/cList.mli OCAMLDEP lib/cErrors.mli OCAMLDEP lib/cEphemeron.mli OCAMLDEP lib/cAst.mli OCAMLDEP lib/cArray.mli OCAMLDEP lib/bigint.mli OCAMLDEP lib/backtrace.mli OCAMLDEP lib/aux_file.mli OCAMLDEP kernel/vconv.mli OCAMLDEP kernel/vm.mli OCAMLDEP kernel/vars.mli OCAMLDEP kernel/univ.mli OCAMLDEP kernel/uint31.mli OCAMLDEP kernel/uGraph.mli OCAMLDEP kernel/type_errors.mli OCAMLDEP kernel/typeops.mli OCAMLDEP kernel/term.mli OCAMLDEP kernel/term_typing.mli OCAMLDEP kernel/sorts.mli OCAMLDEP kernel/safe_typing.mli OCAMLDEP kernel/retroknowledge.mli OCAMLDEP kernel/subtyping.mli OCAMLDEP kernel/reduction.mli OCAMLDEP kernel/primitives.mli OCAMLDEP kernel/pre_env.mli OCAMLDEP kernel/opaqueproof.mli OCAMLDEP kernel/nativevalues.mli OCAMLDEP kernel/nativelibrary.mli OCAMLDEP kernel/nativelib.mli OCAMLDEP kernel/nativelambda.mli OCAMLDEP kernel/nativeinstr.mli OCAMLDEP kernel/nativeconv.mli OCAMLDEP kernel/nativecode.mli OCAMLDEP kernel/names.mli OCAMLDEP kernel/modops.mli OCAMLDEP kernel/mod_subst.mli OCAMLDEP kernel/inductive.mli OCAMLDEP kernel/mod_typing.mli OCAMLDEP kernel/indtypes.mli OCAMLDEP kernel/evar.mli OCAMLDEP kernel/esubst.mli OCAMLDEP kernel/environ.mli OCAMLDEP kernel/declareops.mli OCAMLDEP kernel/entries.mli OCAMLDEP kernel/csymtable.mli OCAMLDEP kernel/cooking.mli OCAMLDEP kernel/conv_oracle.mli OCAMLDEP kernel/context.mli OCAMLDEP kernel/constr.mli OCAMLDEP kernel/cemitcodes.mli OCAMLDEP kernel/cbytegen.mli OCAMLDEP kernel/cbytecodes.mli OCAMLDEP kernel/cClosure.mli OCAMLDEP interp/topconstr.mli OCAMLDEP interp/syntax_def.mli OCAMLDEP interp/stdarg.mli OCAMLDEP interp/smartlocate.mli OCAMLDEP interp/reserve.mli OCAMLDEP interp/ppextend.mli OCAMLDEP interp/notation_ops.mli OCAMLDEP interp/notation.mli OCAMLDEP interp/modintern.mli OCAMLDEP interp/implicit_quantifiers.mli OCAMLDEP interp/impargs.mli OCAMLDEP interp/genintern.mli OCAMLDEP interp/dumpglob.mli OCAMLDEP interp/declare.mli OCAMLDEP interp/constrintern.mli OCAMLDEP interp/constrextern.mli OCAMLDEP interp/constrexpr_ops.mli OCAMLDEP ide/xmlprotocol.mli OCAMLDEP ide/xml_printer.mli OCAMLDEP ide/xml_lexer.mli OCAMLDEP ide/xml_parser.mli OCAMLDEP ide/wg_Segment.mli OCAMLDEP ide/wg_ScriptView.mli OCAMLDEP ide/wg_ProofView.mli OCAMLDEP ide/wg_Notebook.mli OCAMLDEP ide/wg_Find.mli OCAMLDEP ide/wg_MessageView.mli OCAMLDEP ide/wg_Detachable.mli OCAMLDEP ide/wg_Completion.mli OCAMLDEP ide/wg_Command.mli OCAMLDEP ide/utils/configwin_types.mli OCAMLDEP ide/utils/configwin_ihm.mli OCAMLDEP ide/utils/configwin.mli OCAMLDEP ide/tags.mli OCAMLDEP ide/session.mli OCAMLDEP ide/serialize.mli OCAMLDEP ide/sentence.mli OCAMLDEP ide/richpp.mli OCAMLDEP ide/preferences.mli OCAMLDEP ide/minilib.mli OCAMLDEP ide/interface.mli OCAMLDEP ide/ideutils.mli OCAMLDEP ide/fileOps.mli OCAMLDEP ide/document.mli OCAMLDEP ide/coqide.mli OCAMLDEP ide/coqOps.mli OCAMLDEP ide/coq.mli OCAMLDEP grammar/q_util.mli OCAMLDEP engine/uState.mli OCAMLDEP engine/universes.mli OCAMLDEP engine/proofview_monad.mli OCAMLDEP engine/termops.mli OCAMLDEP engine/proofview.mli OCAMLDEP engine/namegen.mli OCAMLDEP engine/logic_monad.mli OCAMLDEP engine/geninterp.mli OCAMLDEP engine/ftactic.mli OCAMLDEP engine/evd.mli OCAMLDEP engine/evarutil.mli OCAMLDEP engine/eConstr.mli OCAMLDEP config/coq_config.mli OCAMLC -c -pp grammar/argextend.mlp OCAMLDEP ide/coqide_main.ml OCAMLC -c -pp grammar/q_util.mlp OCAMLDEP kernel/copcodes.ml OCAMLDEP tools/ocamllibdep.ml OCAMLDEP tools/gallina_lexer.ml OCAMLDEP tools/coqwc.ml OCAMLDEP tools/coqdoc/cpretty.ml OCAMLDEP tools/tolink.ml OCAMLDEP ide/utf8_convert.ml OCAMLDEP ide/coq_lex.ml OCAMLDEP ide/xml_lexer.ml OCAMLDEP tools/coqdep_lexer.ml OCAMLDEP ide/config_lexer.ml OCAMLDEP vernac/vernacinterp.ml OCAMLDEP vernac/vernacprop.ml OCAMLDEP vernac/vernacentries.ml OCAMLDEP vernac/topfmt.ml OCAMLDEP vernac/search.ml OCAMLDEP vernac/record.ml OCAMLDEP vernac/mltop.ml OCAMLDEP vernac/metasyntax.ml OCAMLDEP vernac/obligations.ml OCAMLDEP vernac/lemmas.ml OCAMLDEP vernac/locality.ml OCAMLDEP vernac/indschemes.ml OCAMLDEP vernac/himsg.ml OCAMLDEP vernac/command.ml OCAMLDEP vernac/discharge.ml OCAMLDEP vernac/explainErr.ml OCAMLDEP vernac/declareDef.ml OCAMLDEP vernac/classes.ml OCAMLDEP vernac/auto_ind_decl.ml OCAMLDEP vernac/class.ml OCAMLDEP vernac/assumptions.ml OCAMLDEP toplevel/vernac.ml OCAMLDEP toplevel/usage.ml OCAMLDEP toplevel/coqtop.ml OCAMLDEP toplevel/coqloop.ml OCAMLDEP toplevel/coqinit.ml OCAMLDEP tools/mkwinapp.ml OCAMLDEP tools/md5sum.ml OCAMLDEP tools/gallina.ml OCAMLDEP tools/fake_ide.ml OCAMLDEP tools/coqworkmgr.ml OCAMLDEP tools/coqmktop.ml OCAMLDEP tools/coqdoc/tokens.ml OCAMLDEP tools/coqdoc/output.ml OCAMLDEP tools/coqdoc/main.ml OCAMLDEP tools/coqdoc/index.ml OCAMLDEP tools/coqdoc/cdglobals.ml OCAMLDEP tools/coqdoc/alpha.ml OCAMLDEP tools/coqdep_common.ml OCAMLDEP tools/coqdep.ml OCAMLDEP tools/coqdep_boot.ml OCAMLDEP tools/coqc.ml OCAMLDEP tools/coq_makefile.ml OCAMLDEP tools/coq_tex.ml OCAMLDEP tactics/term_dnet.ml OCAMLDEP tactics/tactics.ml OCAMLDEP tactics/tacticals.ml OCAMLDEP tactics/leminv.ml OCAMLDEP tactics/inv.ml OCAMLDEP tactics/ind_tables.ml OCAMLDEP tactics/hipattern.ml OCAMLDEP tactics/hints.ml OCAMLDEP tactics/equality.ml OCAMLDEP tactics/eqschemes.ml OCAMLDEP tactics/eqdecide.ml OCAMLDEP tactics/eauto.ml OCAMLDEP tactics/elimschemes.ml OCAMLDEP tactics/dnet.ml OCAMLDEP tactics/dn.ml OCAMLDEP tactics/elim.ml OCAMLDEP tactics/contradiction.ml OCAMLDEP tactics/class_tactics.ml OCAMLDEP tactics/autorewrite.ml OCAMLDEP tactics/btermdn.ml OCAMLDEP tactics/auto.ml OCAMLDEP stm/workerPool.ml OCAMLDEP stm/workerLoop.ml OCAMLDEP stm/vio_checking.ml OCAMLDEP stm/vernac_classifier.ml OCAMLDEP stm/vcs.ml OCAMLDEP stm/tacworkertop.ml OCAMLDEP stm/stm.ml OCAMLDEP stm/tQueue.ml OCAMLDEP stm/queryworkertop.ml OCAMLDEP stm/proofworkertop.ml OCAMLDEP stm/proofBlockDelimiter.ml OCAMLDEP stm/spawned.ml OCAMLDEP stm/coqworkmgrApi.ml OCAMLDEP stm/asyncTaskQueue.ml OCAMLDEP stm/dag.ml OCAMLDEP proofs/refiner.ml OCAMLDEP proofs/tacmach.ml OCAMLDEP proofs/refine.ml OCAMLDEP proofs/proof.ml OCAMLDEP proofs/redexpr.ml OCAMLDEP proofs/proof_global.ml OCAMLDEP proofs/proof_using.ml OCAMLDEP proofs/pfedit.ml OCAMLDEP proofs/miscprint.ml OCAMLDEP proofs/logic.ml OCAMLDEP proofs/goal.ml OCAMLDEP proofs/evar_refiner.ml OCAMLDEP proofs/clenvtac.ml OCAMLDEP proofs/clenv.ml OCAMLDEP printing/printmod.ml OCAMLDEP printing/printer.ml OCAMLDEP printing/ppvernac.ml OCAMLDEP printing/pputils.ml OCAMLDEP printing/ppconstr.ml OCAMLDEP printing/prettyp.ml OCAMLDEP printing/genprint.ml OCAMLDEP pretyping/vnorm.ml OCAMLDEP pretyping/unification.ml OCAMLDEP pretyping/typing.ml OCAMLDEP pretyping/typeclasses_errors.ml OCAMLDEP pretyping/typeclasses.ml OCAMLDEP pretyping/tacred.ml OCAMLDEP pretyping/retyping.ml OCAMLDEP pretyping/reductionops.ml OCAMLDEP pretyping/redops.ml OCAMLDEP pretyping/recordops.ml OCAMLDEP pretyping/program.ml OCAMLDEP pretyping/pretyping.ml OCAMLDEP pretyping/pretype_errors.ml OCAMLDEP pretyping/patternops.ml OCAMLDEP pretyping/nativenorm.ml OCAMLDEP pretyping/miscops.ml OCAMLDEP pretyping/locusops.ml OCAMLDEP pretyping/inductiveops.ml OCAMLDEP pretyping/indrec.ml OCAMLDEP pretyping/glob_ops.ml OCAMLDEP pretyping/find_subterm.ml OCAMLDEP pretyping/evarsolve.ml OCAMLDEP pretyping/evardefine.ml OCAMLDEP pretyping/evarconv.ml OCAMLDEP pretyping/detyping.ml OCAMLDEP pretyping/constr_matching.ml OCAMLDEP pretyping/coercion.ml OCAMLDEP pretyping/classops.ml OCAMLDEP pretyping/cbv.ml OCAMLDEP pretyping/cases.ml OCAMLDEP pretyping/arguments_renaming.ml OCAMLDEP plugins/syntax/z_syntax.ml OCAMLDEP plugins/syntax/string_syntax.ml OCAMLDEP plugins/syntax/r_syntax.ml OCAMLDEP plugins/syntax/nat_syntax.ml OCAMLDEP plugins/syntax/int31_syntax.ml OCAMLDEP plugins/syntax/ascii_syntax.ml OCAMLDEP plugins/ssr/ssrview.ml OCAMLDEP plugins/ssr/ssrtacticals.ml OCAMLDEP plugins/ssr/ssrprinters.ml OCAMLDEP plugins/ssr/ssripats.ml OCAMLDEP plugins/ssr/ssrfwd.ml OCAMLDEP plugins/ssr/ssrequality.ml OCAMLDEP plugins/ssr/ssrelim.ml OCAMLDEP plugins/ssr/ssrcommon.ml OCAMLDEP plugins/ssr/ssrbwd.ml OCAMLDEP plugins/setoid_ring/newring.ml OCAMLDEP plugins/rtauto/refl_tauto.ml OCAMLDEP plugins/rtauto/proof_search.ml OCAMLDEP plugins/romega/refl_omega.ml OCAMLDEP plugins/romega/const_omega.ml OCAMLDEP plugins/quote/quote.ml OCAMLDEP plugins/omega/omega.ml OCAMLDEP plugins/omega/coq_omega.ml OCAMLDEP plugins/nsatz/utile.ml OCAMLDEP plugins/nsatz/polynom.ml OCAMLDEP plugins/nsatz/nsatz.ml OCAMLDEP plugins/nsatz/ideal.ml OCAMLDEP plugins/micromega/sos_lib.ml OCAMLDEP plugins/micromega/sos.ml OCAMLDEP plugins/micromega/sos_types.ml OCAMLDEP plugins/micromega/polynomial.ml OCAMLDEP plugins/micromega/mutils.ml OCAMLDEP plugins/micromega/micromega.ml OCAMLDEP plugins/micromega/coq_micromega.ml OCAMLDEP plugins/ltac/tauto.ml OCAMLDEP plugins/micromega/certificate.ml OCAMLDEP plugins/micromega/persistent_cache.ml OCAMLDEP plugins/ltac/tactic_option.ml OCAMLDEP plugins/ltac/tactic_matching.ml OCAMLDEP plugins/micromega/csdpcert.ml OCAMLDEP plugins/micromega/mfourier.ml OCAMLDEP plugins/ltac/tactic_debug.ml OCAMLDEP plugins/ltac/tacsubst.ml OCAMLDEP plugins/ltac/tacintern.ml OCAMLDEP plugins/ltac/tacinterp.ml OCAMLDEP plugins/ltac/tacenv.ml OCAMLDEP plugins/ltac/taccoerce.ml OCAMLDEP plugins/ltac/tacentries.ml OCAMLDEP plugins/ltac/tacarg.ml OCAMLDEP plugins/ltac/rewrite.ml OCAMLDEP plugins/ltac/pptactic.ml OCAMLDEP plugins/ltac/pltac.ml OCAMLDEP plugins/ltac/profile_ltac.ml OCAMLDEP plugins/funind/recdef.ml OCAMLDEP plugins/ltac/evar_tactics.ml OCAMLDEP plugins/funind/merge.ml OCAMLDEP plugins/funind/invfun.ml OCAMLDEP plugins/funind/indfun_common.ml OCAMLDEP plugins/funind/indfun.ml OCAMLDEP plugins/funind/glob_termops.ml OCAMLDEP plugins/funind/glob_term_to_relation.ml OCAMLDEP plugins/funind/functional_principles_types.ml OCAMLDEP plugins/funind/functional_principles_proofs.ml OCAMLDEP plugins/fourier/fourierR.ml OCAMLDEP plugins/fourier/fourier.ml OCAMLDEP plugins/firstorder/unify.ml OCAMLDEP plugins/firstorder/sequent.ml OCAMLDEP plugins/firstorder/rules.ml OCAMLDEP plugins/firstorder/ground.ml OCAMLDEP plugins/firstorder/instances.ml OCAMLDEP plugins/firstorder/formula.ml OCAMLDEP plugins/extraction/table.ml OCAMLDEP plugins/extraction/scheme.ml OCAMLDEP plugins/extraction/modutil.ml OCAMLDEP plugins/extraction/mlutil.ml OCAMLDEP plugins/extraction/json.ml OCAMLDEP plugins/extraction/ocaml.ml OCAMLDEP plugins/extraction/extraction.ml OCAMLDEP plugins/extraction/extract_env.ml OCAMLDEP plugins/extraction/common.ml OCAMLDEP plugins/extraction/haskell.ml OCAMLDEP plugins/derive/derive.ml OCAMLDEP plugins/cc/cctac.ml OCAMLDEP plugins/extraction/big.ml OCAMLDEP plugins/cc/ccproof.ml OCAMLDEP plugins/cc/ccalgo.ml OCAMLDEP plugins/btauto/refl_btauto.ml OCAMLDEP parsing/tok.ml OCAMLDEP parsing/pcoq.ml OCAMLDEP parsing/egramml.ml OCAMLDEP parsing/egramcoq.ml OCAMLDEP library/univops.ml OCAMLDEP library/states.ml OCAMLDEP library/summary.ml OCAMLDEP library/nametab.ml OCAMLDEP library/nameops.ml OCAMLDEP library/loadpath.ml OCAMLDEP library/libobject.ml OCAMLDEP library/library.ml OCAMLDEP library/libnames.ml OCAMLDEP library/lib.ml OCAMLDEP library/keys.ml OCAMLDEP library/kindops.ml OCAMLDEP library/heads.ml OCAMLDEP library/goptions.ml OCAMLDEP library/globnames.ml OCAMLDEP library/global.ml OCAMLDEP library/dischargedhypsmap.ml OCAMLDEP library/decls.ml OCAMLDEP library/declaremods.ml OCAMLDEP lib/util.ml OCAMLDEP library/coqlib.ml OCAMLDEP lib/unionfind.ml OCAMLDEP lib/unicodetable.ml OCAMLDEP lib/unicode.ml OCAMLDEP lib/trie.ml OCAMLDEP lib/terminal.ml OCAMLDEP lib/system.ml OCAMLDEP lib/stateid.ml OCAMLDEP lib/store.ml OCAMLDEP lib/spawn.ml OCAMLDEP lib/segmenttree.ml OCAMLDEP lib/remoteCounter.ml OCAMLDEP lib/rtree.ml OCAMLDEP lib/profile.ml OCAMLDEP lib/predicate.ml OCAMLDEP lib/pp.ml OCAMLDEP lib/option.ml OCAMLDEP lib/monad.ml OCAMLDEP lib/minisys.ml OCAMLDEP lib/loc.ml OCAMLDEP lib/int.ml OCAMLDEP lib/iStream.ml OCAMLDEP lib/hook.ml OCAMLDEP lib/hashset.ml OCAMLDEP lib/heap.ml OCAMLDEP lib/hMap.ml OCAMLDEP lib/hashcons.ml OCAMLDEP lib/genarg.ml OCAMLDEP lib/future.ml OCAMLDEP lib/flags.ml OCAMLDEP lib/feedback.ml OCAMLDEP lib/explore.ml OCAMLDEP lib/exninfo.ml OCAMLDEP lib/envars.ml OCAMLDEP lib/dyn.ml OCAMLDEP lib/deque.ml OCAMLDEP lib/control.ml OCAMLDEP lib/canary.ml OCAMLDEP lib/cWarnings.ml OCAMLDEP lib/cUnix.ml OCAMLDEP lib/cThread.ml OCAMLDEP lib/cString.ml OCAMLDEP lib/cStack.ml OCAMLDEP lib/cSet.ml OCAMLDEP lib/cObj.ml OCAMLDEP lib/cMap.ml OCAMLDEP lib/cList.ml OCAMLDEP lib/cErrors.ml OCAMLDEP lib/cEphemeron.ml OCAMLDEP lib/cAst.ml OCAMLDEP lib/backtrace.ml OCAMLDEP lib/bigint.ml OCAMLDEP lib/cArray.ml OCAMLDEP lib/aux_file.ml OCAMLDEP kernel/vm.ml OCAMLDEP kernel/vconv.ml OCAMLDEP kernel/vars.ml OCAMLDEP kernel/univ.ml OCAMLDEP kernel/uint31.ml OCAMLDEP kernel/uGraph.ml OCAMLDEP kernel/type_errors.ml OCAMLDEP kernel/typeops.ml OCAMLDEP kernel/term_typing.ml OCAMLDEP kernel/term.ml OCAMLDEP kernel/subtyping.ml OCAMLDEP kernel/sorts.ml OCAMLDEP kernel/safe_typing.ml OCAMLDEP kernel/retroknowledge.ml OCAMLDEP kernel/reduction.ml OCAMLDEP kernel/primitives.ml OCAMLDEP kernel/pre_env.ml OCAMLDEP kernel/opaqueproof.ml OCAMLDEP kernel/nativevalues.ml OCAMLDEP kernel/nativelibrary.ml OCAMLDEP kernel/nativelib.ml OCAMLDEP kernel/nativelambda.ml OCAMLDEP kernel/nativeconv.ml OCAMLDEP kernel/nativecode.ml OCAMLDEP kernel/names.ml OCAMLDEP kernel/modops.ml OCAMLDEP kernel/mod_typing.ml OCAMLDEP kernel/mod_subst.ml OCAMLDEP kernel/inductive.ml OCAMLDEP kernel/indtypes.ml OCAMLDEP kernel/evar.ml OCAMLDEP kernel/esubst.ml OCAMLDEP kernel/environ.ml OCAMLDEP kernel/declarations.ml OCAMLDEP kernel/declareops.ml OCAMLDEP kernel/csymtable.ml OCAMLDEP kernel/cooking.ml OCAMLDEP kernel/conv_oracle.ml OCAMLDEP kernel/context.ml OCAMLDEP kernel/constr.ml OCAMLDEP kernel/cemitcodes.ml OCAMLDEP kernel/cbytegen.ml OCAMLDEP kernel/cbytecodes.ml OCAMLDEP kernel/cClosure.ml OCAMLDEP intf/vernacexpr.ml OCAMLDEP intf/tactypes.ml OCAMLDEP intf/pattern.ml OCAMLDEP intf/notation_term.ml OCAMLDEP intf/misctypes.ml OCAMLDEP intf/glob_term.ml OCAMLDEP intf/locus.ml OCAMLDEP intf/genredexpr.ml OCAMLDEP intf/extend.ml OCAMLDEP intf/evar_kinds.ml OCAMLDEP intf/decl_kinds.ml OCAMLDEP intf/constrexpr.ml OCAMLDEP interp/topconstr.ml OCAMLDEP interp/syntax_def.ml OCAMLDEP interp/stdarg.ml OCAMLDEP interp/smartlocate.ml OCAMLDEP interp/reserve.ml OCAMLDEP interp/ppextend.ml OCAMLDEP interp/notation_ops.ml OCAMLDEP interp/notation.ml OCAMLDEP interp/modintern.ml OCAMLDEP interp/implicit_quantifiers.ml OCAMLDEP interp/impargs.ml OCAMLDEP interp/dumpglob.ml OCAMLDEP interp/genintern.ml OCAMLDEP interp/constrintern.ml OCAMLDEP interp/declare.ml OCAMLDEP interp/constrextern.ml OCAMLDEP interp/constrexpr_ops.ml OCAMLDEP ide/xmlprotocol.ml OCAMLDEP ide/xml_parser.ml OCAMLDEP ide/xml_printer.ml OCAMLDEP ide/wg_Segment.ml OCAMLDEP ide/wg_ScriptView.ml OCAMLDEP ide/wg_ProofView.ml OCAMLDEP ide/wg_Notebook.ml OCAMLDEP ide/wg_MessageView.ml OCAMLDEP ide/wg_Find.ml OCAMLDEP ide/wg_Detachable.ml OCAMLDEP ide/wg_Completion.ml OCAMLDEP ide/wg_Command.ml OCAMLDEP ide/utils/configwin_messages.ml OCAMLDEP ide/utils/configwin_ihm.ml OCAMLDEP ide/utils/configwin.ml OCAMLDEP ide/tags.ml OCAMLDEP ide/session.ml OCAMLDEP ide/serialize.ml OCAMLDEP ide/richpp.ml OCAMLDEP ide/sentence.ml OCAMLDEP ide/preferences.ml OCAMLDEP ide/nanoPG.ml OCAMLDEP ide/minilib.ml OCAMLDEP ide/macos_prehook.ml OCAMLDEP ide/ideutils.ml OCAMLDEP ide/ide_slave.ml OCAMLDEP ide/gtk_parsing.ml OCAMLDEP ide/fileOps.ml OCAMLDEP ide/document.ml OCAMLDEP ide/coqide_ui.ml OCAMLDEP ide/coqide.ml OCAMLDEP ide/coq_commands.ml OCAMLDEP ide/coqOps.ml OCAMLDEP ide/coq.ml OCAMLDEP engine/universes.ml OCAMLDEP engine/uState.ml OCAMLDEP engine/termops.ml OCAMLDEP engine/proofview_monad.ml OCAMLDEP engine/proofview.ml OCAMLDEP engine/namegen.ml OCAMLDEP engine/logic_monad.ml OCAMLDEP engine/geninterp.ml OCAMLDEP engine/ftactic.ml OCAMLDEP engine/evd.ml OCAMLDEP engine/evarutil.ml OCAMLDEP engine/eConstr.ml OCAMLDEP dev/vm_printers.ml OCAMLDEP dev/top_printers.ml OCAMLDEP dev/db_printers.ml OCAMLDEP configure.ml OCAMLDEP dev/dynlink.ml OCAMLDEP config/coq_config.ml OCAMLOPT tools/ocamllibdep.ml OCAMLC -c -pp grammar/tacextend.mlp OCAMLC lib/unicodetable.ml OCAMLC -c -pp grammar/vernacextend.mlp OCAMLBEST -o bin/ocamllibdep Testing grammar/grammar.cma OCAMLC -a grammar/grammar.cma OCAMLLIBDEP plugins/syntax/z_syntax_plugin.mlpack OCAMLLIBDEP plugins/syntax/string_syntax_plugin.mlpack OCAMLLIBDEP plugins/syntax/r_syntax_plugin.mlpack OCAMLLIBDEP plugins/syntax/int31_syntax_plugin.mlpack OCAMLLIBDEP plugins/syntax/ascii_syntax_plugin.mlpack OCAMLLIBDEP plugins/ssr/ssreflect_plugin.mlpack OCAMLLIBDEP plugins/ssrmatching/ssrmatching_plugin.mlpack OCAMLLIBDEP plugins/setoid_ring/newring_plugin.mlpack OCAMLLIBDEP plugins/rtauto/rtauto_plugin.mlpack OCAMLLIBDEP plugins/syntax/nat_syntax_plugin.mlpack OCAMLLIBDEP plugins/nsatz/nsatz_plugin.mlpack OCAMLLIBDEP plugins/omega/omega_plugin.mlpack OCAMLLIBDEP plugins/quote/quote_plugin.mlpack OCAMLLIBDEP plugins/romega/romega_plugin.mlpack OCAMLLIBDEP plugins/micromega/micromega_plugin.mlpack OCAMLLIBDEP plugins/ltac/tauto_plugin.mlpack OCAMLLIBDEP plugins/funind/recdef_plugin.mlpack OCAMLLIBDEP plugins/ltac/ltac_plugin.mlpack OCAMLLIBDEP plugins/fourier/fourier_plugin.mlpack OCAMLLIBDEP plugins/firstorder/ground_plugin.mlpack OCAMLLIBDEP plugins/extraction/extraction_plugin.mlpack OCAMLLIBDEP plugins/derive/derive_plugin.mlpack OCAMLLIBDEP plugins/cc/cc_plugin.mlpack OCAMLLIBDEP plugins/btauto/btauto_plugin.mlpack OCAMLLIBDEP toplevel/toplevel.mllib OCAMLLIBDEP tactics/tactics.mllib OCAMLLIBDEP vernac/vernac.mllib OCAMLLIBDEP printing/printing.mllib OCAMLLIBDEP proofs/proofs.mllib OCAMLLIBDEP stm/stm.mllib OCAMLLIBDEP stm/proofworkertop.mllib OCAMLLIBDEP pretyping/pretyping.mllib OCAMLLIBDEP stm/queryworkertop.mllib OCAMLLIBDEP stm/tacworkertop.mllib OCAMLLIBDEP parsing/parsing.mllib OCAMLLIBDEP parsing/highparsing.mllib OCAMLLIBDEP library/library.mllib OCAMLLIBDEP lib/lib.mllib OCAMLLIBDEP lib/clib.mllib OCAMLLIBDEP kernel/kernel.mllib OCAMLLIBDEP interp/interp.mllib OCAMLLIBDEP intf/intf.mllib OCAMLLIBDEP ide/ide.mllib OCAMLLIBDEP ide/coqidetop.mllib OCAMLLIBDEP engine/engine.mllib CAMLP5O plugins/ssrmatching/ssrmatching.ml4 CAMLP5O plugins/ssr/ssrvernac.ml4 CAMLP5O plugins/ssr/ssrparser.ml4 CAMLP5O plugins/rtauto/g_rtauto.ml4 CAMLP5O plugins/romega/g_romega.ml4 OCAMLLIBDEP checker/check.mllib CAMLP5O plugins/quote/g_quote.ml4 CAMLP5O plugins/setoid_ring/g_newring.ml4 CAMLP5O plugins/omega/g_omega.ml4 CAMLP5O plugins/nsatz/g_nsatz.ml4 CAMLP5O plugins/micromega/g_micromega.ml4 CAMLP5O plugins/ltac/profile_ltac_tactics.ml4 CAMLP5O plugins/ltac/g_rewrite.ml4 CAMLP5O plugins/ltac/g_tactic.ml4 CAMLP5O plugins/ltac/g_ltac.ml4 CAMLP5O plugins/ltac/g_obligations.ml4 CAMLP5O plugins/ltac/g_eqdecide.ml4 CAMLP5O plugins/ltac/g_class.ml4 CAMLP5O plugins/ltac/g_auto.ml4 CAMLP5O plugins/ltac/extratactics.ml4 Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex]. CAMLP5O plugins/ltac/coretactics.ml4 CAMLP5O plugins/ltac/extraargs.ml4 CAMLP5O plugins/funind/g_indfun.ml4 CAMLP5O plugins/fourier/g_fourier.ml4 CAMLP5O plugins/firstorder/g_ground.ml4 CAMLP5O plugins/extraction/g_extraction.ml4 CAMLP5O plugins/derive/g_derive.ml4 CAMLP5O plugins/cc/g_congruence.ml4 CAMLP5O plugins/btauto/g_btauto.ml4 CAMLP5O parsing/g_vernac.ml4 CAMLP5O parsing/g_proofs.ml4 CAMLP5O parsing/g_prim.ml4 CAMLP5O parsing/cLexer.ml4 CAMLP5O parsing/g_constr.ml4 CAMLP5O lib/coqProject_file.ml4 OCAMLDEP plugins/ssr/ssrvernac.ml OCAMLDEP plugins/ssr/ssrparser.ml OCAMLDEP plugins/setoid_ring/g_newring.ml OCAMLDEP plugins/rtauto/g_rtauto.ml OCAMLDEP plugins/ssrmatching/ssrmatching.ml OCAMLDEP plugins/quote/g_quote.ml OCAMLDEP plugins/omega/g_omega.ml OCAMLDEP plugins/nsatz/g_nsatz.ml OCAMLDEP plugins/micromega/g_micromega.ml OCAMLDEP plugins/romega/g_romega.ml OCAMLDEP plugins/ltac/g_obligations.ml OCAMLDEP plugins/ltac/g_tactic.ml OCAMLDEP plugins/ltac/g_eqdecide.ml OCAMLDEP plugins/ltac/g_ltac.ml OCAMLDEP plugins/ltac/profile_ltac_tactics.ml OCAMLDEP plugins/ltac/g_rewrite.ml OCAMLDEP plugins/ltac/g_class.ml OCAMLDEP plugins/ltac/g_auto.ml OCAMLDEP plugins/ltac/extratactics.ml OCAMLDEP plugins/ltac/extraargs.ml OCAMLDEP plugins/ltac/coretactics.ml OCAMLDEP plugins/funind/g_indfun.ml OCAMLDEP plugins/fourier/g_fourier.ml OCAMLDEP plugins/firstorder/g_ground.ml OCAMLDEP plugins/extraction/g_extraction.ml OCAMLDEP plugins/derive/g_derive.ml OCAMLDEP plugins/cc/g_congruence.ml OCAMLDEP plugins/btauto/g_btauto.ml OCAMLDEP parsing/g_vernac.ml OCAMLDEP parsing/g_proofs.ml OCAMLDEP parsing/g_prim.ml OCAMLDEP parsing/g_constr.ml OCAMLDEP parsing/cLexer.ml OCAMLDEP lib/coqProject_file.ml OCAMLOPT lib/unicodetable.ml OCAMLC lib/unicode.ml OCAMLC lib/minisys.ml OCAMLOPT lib/unicode.ml OCAMLOPT lib/minisys.ml OCAMLOPT tools/coqdep_lexer.ml OCAMLOPT tools/coqdep_common.ml OCAMLOPT tools/coqdep_boot.ml OCAMLBEST -o bin/coqdep_boot COQDEP plugins/ssr/ssrfun.v COQDEP plugins/ssr/ssreflect.v COQDEP plugins/ssr/ssrbool.v COQDEP plugins/setoid_ring/ZArithRing.v COQDEP plugins/setoid_ring/Rings_Z.v COQDEP plugins/ssrmatching/ssrmatching.v COQDEP plugins/setoid_ring/Rings_R.v COQDEP plugins/setoid_ring/Ring_theory.v COQDEP plugins/setoid_ring/Ring_tac.v COQDEP plugins/setoid_ring/Ring.v COQDEP plugins/setoid_ring/Ring_base.v COQDEP plugins/setoid_ring/Ring_polynom.v COQDEP plugins/setoid_ring/Ncring_tac.v COQDEP plugins/setoid_ring/RealField.v COQDEP plugins/setoid_ring/Rings_Q.v COQDEP plugins/setoid_ring/Ncring_polynom.v COQDEP plugins/setoid_ring/Ncring_initial.v COQDEP plugins/setoid_ring/Ncring.v COQDEP plugins/setoid_ring/NArithRing.v COQDEP plugins/setoid_ring/Integral_domain.v COQDEP plugins/setoid_ring/InitialRing.v COQDEP plugins/setoid_ring/Field_theory.v COQDEP plugins/setoid_ring/Field_tac.v COQDEP plugins/setoid_ring/Field.v COQDEP plugins/setoid_ring/Cring.v COQDEP plugins/setoid_ring/BinList.v COQDEP plugins/setoid_ring/ArithRing.v COQDEP plugins/setoid_ring/Algebra_syntax.v COQDEP plugins/rtauto/Rtauto.v COQDEP plugins/rtauto/Bintree.v COQDEP plugins/romega/ReflOmegaCore.v COQDEP plugins/quote/Quote.v COQDEP plugins/omega/PreOmega.v COQDEP plugins/romega/ROmega.v COQDEP plugins/omega/OmegaTactic.v COQDEP plugins/omega/OmegaPlugin.v COQDEP plugins/omega/OmegaLemmas.v COQDEP plugins/omega/Omega.v COQDEP plugins/nsatz/Nsatz.v COQDEP plugins/micromega/ZCoeff.v COQDEP plugins/micromega/VarMap.v COQDEP plugins/micromega/ZMicromega.v COQDEP plugins/micromega/RingMicromega.v COQDEP plugins/micromega/Tauto.v COQDEP plugins/micromega/QMicromega.v COQDEP plugins/micromega/Refl.v COQDEP plugins/micromega/OrderedRing.v COQDEP plugins/micromega/Lra.v COQDEP plugins/micromega/Psatz.v COQDEP plugins/micromega/RMicromega.v COQDEP plugins/micromega/Lqa.v COQDEP plugins/micromega/MExtraction.v COQDEP plugins/micromega/EnvRing.v COQDEP plugins/micromega/Lia.v COQDEP plugins/micromega/Env.v COQDEP plugins/funind/Recdef.v COQDEP plugins/ltac/Ltac.v COQDEP plugins/fourier/Fourier_util.v COQDEP plugins/fourier/Fourier.v COQDEP plugins/funind/FunInd.v COQDEP plugins/extraction/Extraction.v COQDEP plugins/extraction/ExtrOcamlString.v COQDEP plugins/extraction/ExtrOcamlIntConv.v COQDEP plugins/extraction/ExtrOcamlNatBigInt.v COQDEP plugins/extraction/ExtrOcamlBigIntConv.v COQDEP plugins/extraction/ExtrOcamlBasic.v COQDEP plugins/extraction/ExtrHaskellZNum.v COQDEP plugins/extraction/ExtrOcamlZBigInt.v COQDEP plugins/extraction/ExtrOcamlZInt.v COQDEP plugins/extraction/ExtrOcamlNatInt.v COQDEP plugins/extraction/ExtrHaskellZInteger.v COQDEP plugins/extraction/ExtrHaskellZInt.v COQDEP plugins/extraction/ExtrHaskellString.v COQDEP plugins/extraction/ExtrHaskellNatNum.v COQDEP plugins/extraction/ExtrHaskellNatInteger.v COQDEP plugins/extraction/ExtrHaskellNatInt.v COQDEP plugins/extraction/ExtrHaskellBasic.v COQDEP plugins/derive/Derive.v COQDEP plugins/btauto/Reflect.v COQDEP plugins/btauto/Algebra.v COQDEP theories/ZArith/auxiliary.v COQDEP theories/ZArith/Zpower.v COQDEP plugins/btauto/Btauto.v COQDEP theories/ZArith/Zpow_facts.v COQDEP theories/ZArith/Zsqrt_compat.v COQDEP theories/ZArith/Zpow_def.v COQDEP theories/ZArith/Zpow_alt.v COQDEP theories/ZArith/Zwf.v COQDEP theories/ZArith/Zquot.v COQDEP theories/ZArith/Znat.v COQDEP theories/ZArith/Zmisc.v COQDEP theories/ZArith/Zorder.v COQDEP theories/ZArith/Zminmax.v COQDEP theories/ZArith/Znumtheory.v COQDEP theories/ZArith/Zmin.v COQDEP theories/ZArith/Zmax.v COQDEP theories/ZArith/Zhints.v COQDEP theories/ZArith/Zgcd_alt.v COQDEP theories/ZArith/Zeven.v COQDEP theories/ZArith/Zdiv.v COQDEP theories/ZArith/Zeuclid.v COQDEP theories/ZArith/Zdigits.v COQDEP theories/ZArith/Zcomplements.v COQDEP theories/ZArith/Zcompare.v COQDEP theories/ZArith/Zabs.v COQDEP theories/ZArith/Zbool.v COQDEP theories/ZArith/Zlogarithm.v COQDEP theories/ZArith/ZArith_dec.v COQDEP theories/ZArith/ZArith_base.v COQDEP theories/ZArith/ZArith.v COQDEP theories/ZArith/Wf_Z.v COQDEP theories/ZArith/Int.v COQDEP theories/ZArith/BinInt.v COQDEP theories/Wellfounded/Well_Ordering.v COQDEP theories/Wellfounded/Transitive_Closure.v COQDEP theories/Wellfounded/Inclusion.v COQDEP theories/Wellfounded/Wellfounded.v COQDEP theories/Wellfounded/Disjoint_Union.v COQDEP theories/Vectors/VectorSpec.v COQDEP theories/Vectors/VectorEq.v COQDEP theories/ZArith/BinIntDef.v COQDEP theories/Wellfounded/Lexicographic_Exponentiation.v COQDEP theories/Vectors/Vector.v COQDEP theories/Wellfounded/Inverse_Image.v COQDEP theories/Vectors/Fin.v COQDEP theories/Unicode/Utf8.v COQDEP theories/Structures/OrdersTac.v COQDEP theories/Wellfounded/Union.v COQDEP theories/Unicode/Utf8_core.v COQDEP theories/Structures/OrdersEx.v COQDEP theories/Structures/OrdersAlt.v COQDEP theories/Vectors/VectorDef.v COQDEP theories/Structures/Orders.v COQDEP theories/Structures/OrdersFacts.v COQDEP theories/Structures/OrdersLists.v COQDEP theories/Wellfounded/Lexicographic_Product.v COQDEP theories/Structures/OrderedTypeEx.v COQDEP theories/Structures/OrderedType.v COQDEP theories/Structures/EqualitiesFacts.v COQDEP theories/Structures/DecidableTypeEx.v COQDEP theories/Strings/Ascii.v COQDEP theories/Structures/GenericMinMax.v COQDEP theories/Structures/Equalities.v COQDEP theories/Structures/OrderedTypeAlt.v COQDEP theories/Sorting/Sorting.v COQDEP theories/Sorting/Sorted.v COQDEP theories/Strings/String.v COQDEP theories/Sorting/Permutation.v COQDEP theories/Sorting/PermutSetoid.v COQDEP theories/Structures/DecidableType.v COQDEP theories/Sets/Uniset.v COQDEP theories/Sorting/Mergesort.v COQDEP theories/Sorting/Heap.v COQDEP theories/Sets/Relations_3_facts.v COQDEP theories/Sets/Relations_2_facts.v COQDEP theories/Sets/Relations_2.v COQDEP theories/Sets/Relations_3.v COQDEP theories/Sorting/PermutEq.v COQDEP theories/Sets/Relations_1.v COQDEP theories/Sets/Relations_1_facts.v COQDEP theories/Sets/Powerset_facts.v COQDEP theories/Sets/Powerset_Classical_facts.v COQDEP theories/Sets/Powerset.v COQDEP theories/Sets/Permut.v COQDEP theories/Sets/Partial_Order.v COQDEP theories/Sets/Multiset.v COQDEP theories/Sets/Integers.v COQDEP theories/Sets/Infinite_sets.v COQDEP theories/Sets/Finite_sets_facts.v COQDEP theories/Sets/Finite_sets.v COQDEP theories/Sets/Ensembles.v COQDEP theories/Sets/Image.v COQDEP theories/Sets/Constructive_sets.v COQDEP theories/Setoids/Setoid.v COQDEP theories/Relations/Relation_Operators.v COQDEP theories/Sets/Classical_sets.v COQDEP theories/Relations/Relations.v COQDEP theories/Sets/Cpo.v COQDEP theories/Reals/Sqrt_reg.v COQDEP theories/Relations/Operators_Properties.v COQDEP theories/Reals/SplitRmult.v COQDEP theories/Relations/Relation_Definitions.v COQDEP theories/Reals/SplitAbsolu.v COQDEP theories/Reals/SeqSeries.v COQDEP theories/Reals/SeqProp.v COQDEP theories/Reals/Rtrigo_reg.v COQDEP theories/Reals/Rtrigo_fun.v COQDEP theories/Reals/Rtrigo_def.v COQDEP theories/Reals/Rtrigo_calc.v COQDEP theories/Reals/Rtrigo_alt.v COQDEP theories/Reals/Rtrigo1.v COQDEP theories/Reals/Rtrigo.v COQDEP theories/Reals/Rsqrt_def.v COQDEP theories/Reals/Rtopology.v COQDEP theories/Reals/Rseries.v COQDEP theories/Reals/Rprod.v COQDEP theories/Reals/Rpower.v COQDEP theories/Reals/Rminmax.v COQDEP theories/Reals/Rlogic.v COQDEP theories/Reals/RiemannInt_SF.v COQDEP theories/Reals/RiemannInt.v COQDEP theories/Reals/Rlimit.v COQDEP theories/Reals/Rgeom.v COQDEP theories/Reals/Reals.v COQDEP theories/Reals/Rpow_def.v COQDEP theories/Reals/Rfunctions.v COQDEP theories/Reals/Rderiv.v COQDEP theories/Reals/Rsigma.v COQDEP theories/Reals/Rdefinitions.v COQDEP theories/Reals/Rbasic_fun.v COQDEP theories/Reals/Raxioms.v COQDEP theories/Reals/Ranalysis5.v COQDEP theories/Reals/Ratan.v COQDEP theories/Reals/Ranalysis4.v COQDEP theories/Reals/Rcomplete.v COQDEP theories/Reals/Ranalysis3.v COQDEP theories/Reals/Ranalysis_reg.v COQDEP theories/Reals/Rbase.v COQDEP theories/Reals/R_sqrt.v COQDEP theories/Reals/Ranalysis2.v COQDEP theories/Reals/R_sqr.v COQDEP theories/Reals/Ranalysis.v COQDEP theories/Reals/Ranalysis1.v COQDEP theories/Reals/R_Ifp.v COQDEP theories/Reals/RList.v COQDEP theories/Reals/PartSum.v COQDEP theories/Reals/ROrderedType.v COQDEP theories/Reals/RIneq.v COQDEP theories/Reals/PSeries_reg.v COQDEP theories/Reals/NewtonInt.v COQDEP theories/Reals/Machin.v COQDEP theories/Reals/MVT.v COQDEP theories/Reals/Integration.v COQDEP theories/Reals/DiscrR.v COQDEP theories/Reals/Exp_prop.v COQDEP theories/Reals/Cos_rel.v COQDEP theories/Reals/Cos_plus.v COQDEP theories/Reals/Binomial.v COQDEP theories/Reals/Cauchy_prod.v COQDEP theories/Reals/ArithProp.v COQDEP theories/Reals/AltSeries.v COQDEP theories/Reals/Alembert.v COQDEP theories/QArith/Qround.v COQDEP theories/QArith/Qring.v COQDEP theories/QArith/Qreduction.v COQDEP theories/QArith/Qreals.v COQDEP theories/QArith/Qminmax.v COQDEP theories/QArith/Qpower.v COQDEP theories/QArith/Qfield.v COQDEP theories/QArith/Qcanon.v COQDEP theories/QArith/QOrderedType.v COQDEP theories/QArith/Qabs.v COQDEP theories/QArith/Qcabs.v COQDEP theories/QArith/QArith_base.v COQDEP theories/QArith/QArith.v COQDEP theories/Program/Wf.v COQDEP theories/Program/Tactics.v COQDEP theories/Program/Utils.v COQDEP theories/Program/Syntax.v COQDEP theories/Program/Program.v COQDEP theories/Program/Equality.v COQDEP theories/Program/Subset.v COQDEP theories/Program/Combinators.v COQDEP theories/Program/Basics.v COQDEP theories/PArith/POrderedType.v COQDEP theories/PArith/BinPosDef.v COQDEP theories/PArith/BinPos.v COQDEP theories/PArith/PArith.v COQDEP theories/Numbers/Natural/Peano/NPeano.v COQDEP theories/Numbers/Natural/Binary/NBinary.v COQDEP theories/PArith/Pnat.v COQDEP theories/Numbers/NumPrelude.v COQDEP theories/Numbers/Natural/Abstract/NProperties.v COQDEP theories/Numbers/Natural/Abstract/NStrongRec.v COQDEP theories/Numbers/Natural/Abstract/NSqrt.v COQDEP theories/Numbers/Natural/Abstract/NSub.v COQDEP theories/Numbers/Natural/Abstract/NPow.v COQDEP theories/Numbers/Natural/Abstract/NParity.v COQDEP theories/Numbers/Natural/Abstract/NOrder.v COQDEP theories/Numbers/Natural/Abstract/NMulOrder.v COQDEP theories/Numbers/Natural/Abstract/NMaxMin.v COQDEP theories/Numbers/Natural/Abstract/NLog.v COQDEP theories/Numbers/Natural/Abstract/NLcm.v COQDEP theories/Numbers/Natural/Abstract/NGcd.v COQDEP theories/Numbers/Natural/Abstract/NDiv.v COQDEP theories/Numbers/Natural/Abstract/NIso.v COQDEP theories/Numbers/Natural/Abstract/NDefOps.v COQDEP theories/Numbers/Natural/Abstract/NBits.v COQDEP theories/Numbers/Natural/Abstract/NBase.v COQDEP theories/Numbers/Natural/Abstract/NAxioms.v COQDEP theories/Numbers/Natural/Abstract/NAddOrder.v COQDEP theories/Numbers/Natural/Abstract/NAdd.v COQDEP theories/Numbers/NatInt/NZProperties.v COQDEP theories/Numbers/NatInt/NZSqrt.v COQDEP theories/Numbers/NatInt/NZPow.v COQDEP theories/Numbers/NatInt/NZParity.v COQDEP theories/Numbers/NatInt/NZLog.v COQDEP theories/Numbers/NatInt/NZGcd.v COQDEP theories/Numbers/NatInt/NZOrder.v COQDEP theories/Numbers/NatInt/NZDomain.v COQDEP theories/Numbers/NatInt/NZMulOrder.v COQDEP theories/Numbers/NatInt/NZDiv.v COQDEP theories/Numbers/NatInt/NZMul.v COQDEP theories/Numbers/NatInt/NZBits.v COQDEP theories/Numbers/NatInt/NZBase.v COQDEP theories/Numbers/NatInt/NZAxioms.v COQDEP theories/Numbers/NatInt/NZAddOrder.v COQDEP theories/Numbers/NatInt/NZAdd.v COQDEP theories/Numbers/NaryFunctions.v COQDEP theories/Numbers/Integer/NatPairs/ZNatPairs.v COQDEP theories/Numbers/Integer/Binary/ZBinary.v COQDEP theories/Numbers/Integer/Abstract/ZProperties.v COQDEP theories/Numbers/Integer/Abstract/ZSgnAbs.v COQDEP theories/Numbers/Integer/Abstract/ZPow.v COQDEP theories/Numbers/Integer/Abstract/ZParity.v COQDEP theories/Numbers/Integer/Abstract/ZMulOrder.v COQDEP theories/Numbers/Integer/Abstract/ZMul.v COQDEP theories/Numbers/Integer/Abstract/ZLt.v COQDEP theories/Numbers/Integer/Abstract/ZGcd.v COQDEP theories/Numbers/Integer/Abstract/ZLcm.v COQDEP theories/Numbers/Integer/Abstract/ZMaxMin.v COQDEP theories/Numbers/Integer/Abstract/ZDivTrunc.v COQDEP theories/Numbers/Integer/Abstract/ZDivFloor.v COQDEP theories/Numbers/Integer/Abstract/ZDivEucl.v COQDEP theories/Numbers/Integer/Abstract/ZBits.v COQDEP theories/Numbers/Integer/Abstract/ZBase.v COQDEP theories/Numbers/Integer/Abstract/ZAxioms.v COQDEP theories/Numbers/Integer/Abstract/ZAddOrder.v COQDEP theories/Numbers/Integer/Abstract/ZAdd.v COQDEP theories/Numbers/Cyclic/ZModulo/ZModulo.v COQDEP theories/Numbers/Cyclic/Int31/Ring31.v COQDEP theories/Numbers/Cyclic/Int31/Int31.v COQDEP theories/Numbers/Cyclic/Int31/Cyclic31.v COQDEP theories/Numbers/Cyclic/Abstract/NZCyclic.v COQDEP theories/Numbers/Cyclic/Abstract/DoubleType.v COQDEP theories/Numbers/Cyclic/Abstract/CyclicAxioms.v COQDEP theories/Numbers/BinNums.v COQDEP theories/NArith/Nsqrt_def.v COQDEP theories/NArith/Ngcd_def.v COQDEP theories/NArith/Ndist.v COQDEP theories/NArith/Nnat.v COQDEP theories/NArith/Ndiv_def.v COQDEP theories/NArith/Ndigits.v COQDEP theories/NArith/Ndec.v COQDEP theories/NArith/BinNat.v COQDEP theories/NArith/NArith.v COQDEP theories/MSets/MSets.v COQDEP theories/NArith/BinNatDef.v COQDEP theories/MSets/MSetWeakList.v COQDEP theories/MSets/MSetToFiniteSet.v COQDEP theories/MSets/MSetRBT.v COQDEP theories/MSets/MSetProperties.v COQDEP theories/MSets/MSetList.v COQDEP theories/MSets/MSetPositive.v COQDEP theories/MSets/MSetInterface.v COQDEP theories/MSets/MSetGenTree.v COQDEP theories/MSets/MSetFacts.v COQDEP theories/MSets/MSetDecide.v COQDEP theories/MSets/MSetAVL.v COQDEP theories/Logic/WeakFan.v COQDEP theories/Logic/WKL.v COQDEP theories/MSets/MSetEqProperties.v COQDEP theories/Logic/SetoidChoice.v COQDEP theories/Logic/RelationalChoice.v COQDEP theories/Logic/SetIsType.v COQDEP theories/Logic/PropExtensionalityFacts.v COQDEP theories/Logic/PropFacts.v COQDEP theories/Logic/JMeq.v COQDEP theories/Logic/PropExtensionality.v COQDEP theories/Logic/ProofIrrelevance.v COQDEP theories/Logic/ProofIrrelevanceFacts.v COQDEP theories/Logic/IndefiniteDescription.v COQDEP theories/Logic/Hurkens.v COQDEP theories/Logic/FunctionalExtensionality.v COQDEP theories/Logic/FinFun.v COQDEP theories/Logic/ExtensionalityFacts.v COQDEP theories/Logic/ExtensionalFunctionRepresentative.v COQDEP theories/Logic/EqdepFacts.v COQDEP theories/Logic/Eqdep_dec.v COQDEP theories/Logic/Eqdep.v COQDEP theories/Logic/Diaconescu.v COQDEP theories/Logic/Description.v COQDEP theories/Logic/Epsilon.v COQDEP theories/Logic/ConstructiveEpsilon.v COQDEP theories/Logic/Classical_Prop.v COQDEP theories/Logic/Classical_Pred_Type.v COQDEP theories/Logic/ClassicalEpsilon.v COQDEP theories/Logic/ClassicalFacts.v COQDEP theories/Logic/Decidable.v COQDEP theories/Logic/ClassicalDescription.v COQDEP theories/Logic/ClassicalUniqueChoice.v COQDEP theories/Logic/ClassicalChoice.v COQDEP theories/Logic/Classical.v COQDEP theories/Logic/ChoiceFacts.v COQDEP theories/Logic/Berardi.v COQDEP theories/Lists/Streams.v COQDEP theories/Lists/StreamMemo.v COQDEP theories/Lists/SetoidPermutation.v COQDEP theories/Lists/SetoidList.v COQDEP theories/Lists/ListTactics.v COQDEP theories/Lists/ListSet.v COQDEP theories/Lists/ListDec.v COQDEP theories/Init/Wf.v COQDEP theories/Init/Tactics.v COQDEP theories/Init/Specif.v COQDEP theories/Lists/List.v COQDEP theories/Init/Prelude.v COQDEP theories/Init/Tauto.v COQDEP theories/Init/Nat.v COQDEP theories/Init/Logic_Type.v COQDEP theories/Init/Notations.v COQDEP theories/Init/Logic.v COQDEP theories/Init/Peano.v COQDEP theories/Init/Datatypes.v COQDEP theories/FSets/FSets.v COQDEP theories/FSets/FSetWeakList.v COQDEP theories/FSets/FSetToFiniteSet.v COQDEP theories/FSets/FSetProperties.v COQDEP theories/FSets/FSetPositive.v COQDEP theories/FSets/FSetList.v COQDEP theories/FSets/FSetFacts.v COQDEP theories/FSets/FSetInterface.v COQDEP theories/FSets/FSetDecide.v COQDEP theories/FSets/FSetBridge.v COQDEP theories/FSets/FSetEqProperties.v COQDEP theories/FSets/FMapWeakList.v COQDEP theories/FSets/FSetAVL.v COQDEP theories/FSets/FMapPositive.v COQDEP theories/FSets/FMaps.v COQDEP theories/FSets/FSetCompat.v COQDEP theories/FSets/FMapList.v COQDEP theories/FSets/FMapInterface.v COQDEP theories/FSets/FMapFullAVL.v COQDEP theories/FSets/FMapFacts.v COQDEP theories/FSets/FMapAVL.v COQDEP theories/Compat/Coq86.v COQDEP theories/Compat/Coq85.v COQDEP theories/Compat/AdmitAxiom.v COQDEP theories/Classes/SetoidTactics.v COQDEP theories/Classes/SetoidClass.v COQDEP theories/Classes/SetoidDec.v COQDEP theories/Classes/RelationClasses.v COQDEP theories/Classes/RelationPairs.v COQDEP theories/Classes/Morphisms_Relations.v COQDEP theories/Classes/Morphisms_Prop.v COQDEP theories/Classes/Init.v COQDEP theories/Classes/Morphisms.v COQDEP theories/Classes/Equivalence.v COQDEP theories/Classes/EquivDec.v COQDEP theories/Classes/DecidableClass.v COQDEP theories/Classes/CRelationClasses.v COQDEP theories/Classes/CMorphisms.v COQDEP theories/Classes/CEquivalence.v COQDEP theories/Bool/Zerob.v COQDEP theories/Bool/Sumbool.v COQDEP theories/Bool/DecBool.v COQDEP theories/Bool/Bvector.v COQDEP theories/Bool/IfProp.v COQDEP theories/Bool/BoolEq.v COQDEP theories/Arith/Wf_nat.v COQDEP theories/Bool/Bool.v COQDEP theories/Arith/Plus.v COQDEP theories/Arith/PeanoNat.v COQDEP theories/Arith/Minus.v COQDEP theories/Arith/Mult.v COQDEP theories/Arith/Min.v COQDEP theories/Arith/Max.v COQDEP theories/Arith/Le.v COQDEP theories/Arith/Peano_dec.v COQDEP theories/Arith/Gt.v COQDEP theories/Arith/Lt.v COQDEP theories/Arith/Factorial.v COQDEP theories/Arith/Even.v COQDEP theories/Arith/Euclid.v COQDEP theories/Arith/EqNat.v COQDEP theories/Arith/Div2.v COQDEP theories/Arith/Compare_dec.v COQDEP theories/Arith/Compare.v COQDEP theories/Arith/Between.v COQDEP theories/Arith/Bool_nat.v COQDEP theories/Arith/Arith_base.v COQDEP theories/Arith/Arith.v OCAMLC lib/terminal.mli OCAMLC lib/canary.mli OCAMLC lib/hook.mli OCAMLC config/coq_config.mli OCAMLC lib/hashset.mli OCAMLC lib/option.mli OCAMLC lib/store.mli OCAMLC lib/exninfo.mli OCAMLC lib/iStream.mli OCAMLC lib/cSig.mli OCAMLC lib/cObj.mli OCAMLC lib/deque.mli OCAMLC lib/flags.mli OCAMLC lib/control.mli OCAMLC lib/cArray.mli OCAMLC lib/pp.mli OCAMLC lib/xml_datatype.mli OCAMLC lib/cUnix.mli OCAMLC lib/envars.mli OCAMLC lib/monad.mli OCAMLC lib/coqProject_file.mli OCAMLC tools/tolink.ml OCAMLC lib/bigint.mli OCAMLC lib/cThread.mli OCAMLC lib/spawn.mli OCAMLC lib/trie.mli OCAMLC lib/profile.mli OCAMLC lib/explore.mli OCAMLC lib/rtree.mli OCAMLC lib/predicate.mli OCAMLC lib/heap.mli OCAMLC lib/unionfind.mli OCAMLC lib/genarg.mli OCAMLC lib/cEphemeron.mli OCAMLC lib/future.mli OCAMLC lib/remoteCounter.mli OCAMLC kernel/uint31.mli OCAMLC kernel/copcodes.ml OCAMLC kernel/primitives.mli OCAMLC intf/decl_kinds.ml OCAMLC library/summary.mli OCAMLC engine/logic_monad.mli OCAMLC parsing/tok.mli OCAMLC tactics/dnet.mli OCAMLC tactics/dn.mli OCAMLC stm/spawned.mli OCAMLC stm/dag.mli OCAMLC stm/tQueue.mli OCAMLC stm/workerPool.mli OCAMLC stm/coqworkmgrApi.mli OCAMLC stm/vio_checking.mli OCAMLC stm/workerLoop.mli OCAMLC toplevel/usage.mli OCAMLC toplevel/coqtop.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 OCAMLC plugins/ltac/tauto.mli OCAMLC plugins/fourier/fourier.ml OCAMLC plugins/micromega/sos_types.mli OCAMLC plugins/micromega/micromega.mli OCAMLC plugins/nsatz/utile.mli OCAMLC plugins/nsatz/polynom.mli OCAMLC plugins/rtauto/proof_search.mli OCAMLC plugins/ssr/ssrvernac.mli MD5SUM cic.mli OCAMLC checker/values.ml OCAMLC checker/check_stat.mli OCAMLC plugins/micromega/sos_lib.ml OCAMLC ide/xml_lexer.mli OCAMLC ide/xml_parser.mli OCAMLC ide/xml_printer.mli OCAMLC ide/richpp.mli OCAMLC tools/gallina_lexer.ml OCAMLC tools/coq_tex.ml OCAMLC tools/coqwc.ml OCAMLC tools/coqdoc/cdglobals.mli OCAMLC tools/coqdoc/alpha.mli OCAMLC tools/coqworkmgr.ml OCAMLC ide/minilib.mli OCAMLC ide/utils/configwin_messages.ml OCAMLC ide/utils/configwin_types.mli OCAMLC ide/utils/configwin.mli OCAMLC ide/tags.mli OCAMLC ide/wg_Notebook.mli OCAMLC ide/sentence.mli OCAMLC ide/utf8_convert.ml OCAMLC ide/wg_Segment.mli OCAMLC ide/wg_Detachable.mli OCAMLC ide/wg_Find.mli OCAMLC ide/coq_commands.ml OCAMLC ide/coqide.mli CHECK revision OCAMLOPT config/coq_config.ml OCAMLOPT lib/terminal.ml OCAMLOPT lib/hook.ml OCAMLOPT lib/canary.ml OCAMLC lib/cMap.mli OCAMLC lib/dyn.mli OCAMLC lib/hashcons.mli OCAMLOPT lib/option.ml OCAMLOPT lib/store.ml OCAMLC lib/backtrace.mli OCAMLC lib/loc.mli OCAMLOPT lib/iStream.ml OCAMLC lib/cList.mli OCAMLOPT lib/cObj.ml OCAMLC lib/cStack.mli OCAMLOPT lib/monad.ml OCAMLOPT tools/tolink.ml OCAMLC lib/system.mli OCAMLOPT lib/cThread.ml OCAMLOPT lib/trie.ml OCAMLOPT lib/predicate.ml OCAMLOPT lib/heap.ml OCAMLOPT lib/unionfind.ml OCAMLOPT lib/cEphemeron.ml OCAMLOPT kernel/uint31.ml OCAMLC kernel/evar.mli OCAMLOPT kernel/copcodes.ml OCAMLOPT kernel/primitives.ml OCAMLOPT intf/decl_kinds.ml OCAMLOPT parsing/tok.ml OCAMLC library/states.mli OCAMLC library/kindops.mli OCAMLC interp/ppextend.mli OCAMLC printing/genprint.mli OCAMLOPT tactics/dnet.ml OCAMLC vernac/locality.mli OCAMLC stm/vcs.mli OCAMLOPT toplevel/usage.ml OCAMLOPT plugins/fourier/fourier.ml OCAMLOPT plugins/micromega/sos_types.ml OCAMLOPT plugins/micromega/micromega.ml OCAMLC plugins/nsatz/ideal.mli OCAMLOPT checker/values.ml OCAMLC checker/validate.ml OCAMLOPT plugins/micromega/sos_lib.ml OCAMLC plugins/micromega/sos.mli OCAMLC ide/serialize.mli OCAMLOPT ide/xml_printer.ml OCAMLOPT ide/xml_lexer.ml OCAMLOPT tools/gallina_lexer.ml OCAMLC tools/gallina.ml OCAMLOPT tools/coq_tex.ml OCAMLOPT tools/coqwc.ml OCAMLOPT tools/coqdoc/cdglobals.ml OCAMLC tools/coqdoc/cpretty.mli OCAMLC tools/coqdoc/index.mli OCAMLC tools/coqc.ml OCAMLOPT ide/utils/configwin_messages.ml OCAMLC ide/utils/configwin_ihm.mli OCAMLOPT ide/tags.ml OCAMLOPT ide/utf8_convert.ml OCAMLC ide/coq_lex.ml OCAMLC ide/gtk_parsing.ml OCAMLOPT ide/wg_Detachable.ml OCAMLOPT ide/coq_commands.ml OCAMLOPT lib/cMap.ml OCAMLC lib/int.mli OCAMLC lib/cSet.mli OCAMLC lib/hMap.mli OCAMLOPT lib/exninfo.ml OCAMLC lib/cAst.mli OCAMLC lib/cString.mli OCAMLC lib/stateid.mli OCAMLC lib/aux_file.mli OCAMLC lib/cErrors.mli OCAMLC lib/cWarnings.mli OCAMLOPT plugins/micromega/sos.ml OCAMLOPT checker/validate.ml OCAMLOPT ide/xml_parser.ml OCAMLBEST -o bin/coq-tex OCAMLOPT tools/gallina.ml OCAMLBEST -o bin/coqwc OCAMLOPT tools/coqdoc/alpha.ml OCAMLC tools/coqdoc/tokens.mli OCAMLC tools/coqdoc/output.mli OCAMLOPT ide/coq_lex.ml OCAMLC lib/util.mli OCAMLC lib/feedback.mli OCAMLC tools/coqmktop.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 parsing/cLexer.mli OCAMLC plugins/micromega/mutils.ml OCAMLC plugins/micromega/persistent_cache.ml OCAMLC ide/document.mli OCAMLC tools/coqdep.ml OCAMLC tools/coq_makefile.ml OCAMLC tools/coqdoc/main.ml OCAMLC ide/config_lexer.ml OCAMLC ide/preferences.mli OCAMLC ide/ideutils.mli OCAMLOPT lib/int.ml OCAMLOPT lib/backtrace.ml OCAMLOPT lib/loc.ml OCAMLC kernel/names.mli OCAMLC kernel/esubst.mli OCAMLC intf/extend.ml OCAMLC vernac/explainErr.mli OCAMLC vernac/topfmt.mli OCAMLC stm/asyncTaskQueue.mli OCAMLC plugins/omega/omega.ml OCAMLC plugins/micromega/polynomial.ml OCAMLC checker/names.mli OCAMLC checker/esubst.mli OCAMLC plugins/micromega/csdpcert.ml OCAMLBEST -o bin/gallina OCAMLC ide/interface.mli OCAMLOPT tools/coqdoc/index.ml OCAMLOPT ide/sentence.ml OCAMLC ide/fileOps.mli OCAMLC ide/coqide_ui.ml OCAMLC ide/wg_MessageView.mli OCAMLOPT lib/flags.ml OCAMLOPT lib/cAst.ml OCAMLC kernel/univ.mli OCAMLC kernel/conv_oracle.mli OCAMLC library/libnames.mli OCAMLC library/loadpath.mli OCAMLOPT stm/dag.ml OCAMLC toplevel/coqinit.mli OCAMLOPT plugins/micromega/mutils.ml OCAMLC ide/coq.mli OCAMLC ide/xmlprotocol.mli OCAMLC ide/wg_ProofView.mli OCAMLOPT lib/dyn.ml OCAMLOPT lib/hashset.ml OCAMLOPT lib/deque.ml OCAMLOPT lib/hMap.ml OCAMLOPT lib/cList.ml OCAMLOPT lib/pp.ml OCAMLOPT lib/bigint.ml OCAMLC kernel/uGraph.mli OCAMLC kernel/sorts.mli OCAMLOPT kernel/evar.ml OCAMLOPT stm/coqworkmgrApi.ml OCAMLC library/dischargedhypsmap.mli OCAMLC checker/univ.mli OCAMLC tools/fake_ide.ml OCAMLOPT tools/coqdoc/tokens.ml OCAMLC plugins/micromega/mfourier.ml OCAMLC ide/wg_Completion.mli OCAMLOPT lib/control.ml OCAMLOPT lib/stateid.ml OCAMLC kernel/constr.mli OCAMLOPT plugins/micromega/csdpcert.ml OCAMLOPT lib/hashcons.ml OCAMLOPT plugins/micromega/polynomial.ml OCAMLC ide/wg_ScriptView.mli OCAMLOPT interp/ppextend.ml OCAMLC checker/cic.mli OCAMLOPT tools/coqdoc/output.ml OCAMLOPT lib/cErrors.ml OCAMLOPT stm/workerLoop.ml OCAMLOPT tools/coqworkmgr.ml OCAMLOPT lib/cStack.ml OCAMLOPT lib/cArray.ml OCAMLC kernel/context.mli OCAMLOPT lib/feedback.ml OCAMLC ide/coqOps.mli OCAMLOPT ide/document.ml OCAMLC checker/print.ml OCAMLOPT lib/cSet.ml OCAMLC checker/term.mli OCAMLC checker/environ.mli OCAMLOPT lib/cString.ml OCAMLOPT lib/profile.ml OCAMLC checker/declarations.mli OCAMLOPT lib/spawn.ml OCAMLOPT lib/future.ml OCAMLOPT lib/remoteCounter.ml OCAMLC kernel/vars.mli OCAMLC kernel/term.mli OCAMLOPT library/kindops.ml OCAMLOPT stm/workerPool.ml OCAMLOPT stm/tQueue.ml OCAMLOPT plugins/nsatz/utile.ml OCAMLOPT plugins/micromega/mfourier.ml OCAMLOPT plugins/micromega/persistent_cache.ml OCAMLC checker/closure.mli OCAMLC checker/modops.mli OCAMLC checker/type_errors.mli OCAMLC checker/reduction.mli OCAMLC checker/inductive.mli OCAMLC checker/typeops.mli OCAMLC checker/indtypes.mli OCAMLC checker/subtyping.mli OCAMLC checker/mod_checking.mli OCAMLC checker/safe_typing.mli OCAMLOPT ide/serialize.ml OCAMLC ide/wg_Command.mli OCAMLOPT lib/util.ml OCAMLOPT lib/cUnix.ml OCAMLOPT lib/cWarnings.ml OCAMLOPT lib/explore.ml OCAMLC kernel/cbytecodes.mli OCAMLC kernel/mod_subst.mli OCAMLC kernel/nativevalues.mli OCAMLC intf/misctypes.ml OCAMLC library/nameops.mli OCAMLOPT stm/vcs.ml OCAMLOPT stm/spawned.ml OCAMLOPT tools/coqdoc/cpretty.ml OCAMLC checker/check.ml OCAMLC ide/session.mli OCAMLC kernel/opaqueproof.mli OCAMLC library/globnames.mli OCAMLC library/libobject.mli OCAMLC library/goptions.mli OCAMLC tactics/term_dnet.mli OCAMLOPT lib/coqProject_file.ml OCAMLOPT lib/aux_file.ml OCAMLC kernel/nativeinstr.mli OCAMLC kernel/vm.mli OCAMLC kernel/cemitcodes.mli OCAMLOPT library/summary.ml OCAMLOPT engine/logic_monad.ml OCAMLC intf/locus.ml OCAMLOPT parsing/cLexer.ml OCAMLOPT tactics/dn.ml OCAMLC proofs/miscprint.mli OCAMLOPT plugins/omega/omega.ml OCAMLC plugins/extraction/miniml.mli OCAMLOPT vernac/topfmt.ml OCAMLOPT plugins/nsatz/polynom.ml OCAMLOPT checker/names.ml OCAMLOPT checker/esubst.ml OCAMLC checker/checker.ml OCAMLOPT ide/wg_Notebook.ml OCAMLOPT ide/richpp.ml OCAMLOPT ide/config_lexer.ml OCAMLC ide/nanoPG.ml OCAMLOPT lib/envars.ml OCAMLOPT lib/rtree.ml OCAMLOPT lib/system.ml OCAMLOPT lib/genarg.ml OCAMLOPT kernel/names.ml OCAMLOPT kernel/esubst.ml OCAMLC kernel/retroknowledge.mli OCAMLC library/nametab.mli OCAMLC intf/evar_kinds.ml OCAMLC library/library.mli OCAMLC library/keys.mli OCAMLC library/lib.mli OCAMLC library/coqlib.mli OCAMLC pretyping/locusops.mli OCAMLC interp/smartlocate.mli 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 OCAMLOPT plugins/nsatz/ideal.ml OCAMLC plugins/extraction/extract_env.mli OCAMLOPT checker/univ.ml OCAMLOPT ide/xmlprotocol.ml OCAMLOPT tools/coqc.ml OCAMLOPT tools/coqdoc/main.ml OCAMLOPT tools/coq_makefile.ml OCAMLOPT ide/minilib.ml OCAMLOPT -a -o lib/lib.cmxa OCAMLOPT tools/coqmktop.ml OCAMLC kernel/declarations.ml OCAMLOPT -a -o lib/clib.cmxa OCAMLOPT printing/genprint.ml OCAMLOPT intf/extend.ml OCAMLOPT tools/coqdep.ml OCAMLOPT kernel/univ.ml OCAMLOPT kernel/conv_oracle.ml OCAMLOPT library/libnames.ml OCAMLC library/univops.mli OCAMLOPT library/nameops.ml OCAMLBEST -o plugins/micromega/csdpcert OCAMLBEST -o bin/coqworkmgr OCAMLOPT ide/utils/configwin_ihm.ml OCAMLOPT ide/gtk_parsing.ml OCAMLC kernel/entries.mli OCAMLC kernel/pre_env.mli OCAMLBEST -o bin/coqdoc OCAMLBEST -o bin/coqc OCAMLBEST -o bin/coqmktop OCAMLOPT library/dischargedhypsmap.ml OCAMLBEST -o bin/coq_makefile OCAMLBEST -o bin/coqdep OCAMLOPT checker/term.ml OCAMLOPT checker/print.ml OCAMLC kernel/declareops.mli OCAMLOPT library/loadpath.ml OCAMLC vernac/discharge.mli OCAMLOPT tools/fake_ide.ml OCAMLC kernel/cbytegen.mli OCAMLC kernel/nativelambda.mli OCAMLC kernel/environ.mli OCAMLC kernel/csymtable.mli OCAMLOPT kernel/uGraph.ml OCAMLOPT kernel/sorts.ml OCAMLC kernel/nativecode.mli OCAMLC kernel/cClosure.mli OCAMLC kernel/type_errors.mli OCAMLC kernel/reduction.mli OCAMLC kernel/modops.mli OCAMLC kernel/inductive.mli OCAMLC kernel/typeops.mli OCAMLC kernel/indtypes.mli OCAMLC kernel/cooking.mli OCAMLC kernel/subtyping.mli OCAMLC kernel/mod_typing.mli OCAMLC kernel/vconv.mli OCAMLC kernel/nativelibrary.mli OCAMLC engine/universes.mli OCAMLC library/decls.mli OCAMLC library/heads.mli OCAMLC pretyping/arguments_renaming.mli OCAMLC printing/printmod.mli OCAMLC plugins/extraction/table.mli OCAMLC plugins/extraction/extraction.mli OCAMLOPT checker/declarations.ml OCAMLOPT kernel/constr.ml OCAMLOPT ide/utils/configwin.ml OCAMLC kernel/nativelib.mli OCAMLC kernel/nativeconv.mli OCAMLC kernel/term_typing.mli OCAMLC kernel/safe_typing.mli OCAMLC plugins/extraction/mlutil.mli OCAMLOPT ide/preferences.ml OCAMLC engine/uState.mli OCAMLC interp/declare.mli OCAMLC library/global.mli OCAMLC engine/evd.mli OCAMLOPT checker/environ.ml OCAMLOPT kernel/context.ml OCAMLC engine/eConstr.mli OCAMLC pretyping/indrec.mli OCAMLC engine/proofview_monad.mli OCAMLC tactics/ind_tables.mli OCAMLC tactics/elimschemes.mli OCAMLC vernac/auto_ind_decl.mli OCAMLC plugins/firstorder/formula.mli OCAMLC plugins/firstorder/unify.mli OCAMLC tactics/eqschemes.mli OCAMLC intf/pattern.ml OCAMLC engine/namegen.mli OCAMLC engine/termops.mli OCAMLC engine/evarutil.mli OCAMLC engine/proofview.mli OCAMLC pretyping/pretype_errors.mli OCAMLC pretyping/reductionops.mli OCAMLC pretyping/inductiveops.mli OCAMLC pretyping/vnorm.mli OCAMLC pretyping/nativenorm.mli OCAMLC pretyping/retyping.mli OCAMLC pretyping/cbv.mli OCAMLC pretyping/typing.mli OCAMLC pretyping/evardefine.mli OCAMLC pretyping/constr_matching.mli OCAMLC pretyping/classops.mli OCAMLC proofs/goal.mli OCAMLC pretyping/program.mli OCAMLC proofs/refine.mli OCAMLC tactics/btermdn.mli OCAMLC tactics/hipattern.mli OCAMLC tactics/contradiction.mli OCAMLC vernac/search.mli OCAMLC tactics/eqdecide.mli OCAMLC plugins/nsatz/nsatz.mli OCAMLC plugins/romega/const_omega.mli OCAMLOPT checker/closure.ml OCAMLOPT checker/type_errors.ml OCAMLOPT checker/modops.ml OCAMLOPT ide/ideutils.ml OCAMLOPT ide/coqide_ui.ml OCAMLOPT kernel/vars.ml OCAMLC engine/ftactic.mli OCAMLC pretyping/evarsolve.mli OCAMLC pretyping/find_subterm.mli OCAMLC pretyping/recordops.mli OCAMLC pretyping/tacred.mli OCAMLC proofs/proof_type.mli OCAMLC plugins/cc/ccalgo.mli OCAMLC engine/geninterp.mli OCAMLC pretyping/evarconv.mli OCAMLC proofs/logic.mli OCAMLC proofs/refiner.mli OCAMLC plugins/cc/ccproof.mli OCAMLC intf/glob_term.ml OCAMLOPT kernel/term.ml OCAMLC plugins/cc/cctac.mli OCAMLOPT checker/reduction.ml OCAMLC intf/constrexpr.ml OCAMLC pretyping/glob_ops.mli OCAMLC pretyping/coercion.mli OCAMLC pretyping/detyping.mli OCAMLC pretyping/patternops.mli OCAMLC pretyping/cases.mli OCAMLC intf/notation_term.ml OCAMLC intf/tactypes.ml OCAMLC intf/genredexpr.ml OCAMLC interp/constrexpr_ops.mli OCAMLC pretyping/typeclasses_errors.mli OCAMLC interp/topconstr.mli OCAMLC interp/modintern.mli OCAMLC interp/impargs.mli OCAMLC printing/ppconstr.mli OCAMLC proofs/proof.mli OCAMLC tactics/leminv.mli OCAMLC plugins/funind/glob_term_to_relation.mli OCAMLC plugins/derive/derive.mli OCAMLC printing/prettyp.mli OCAMLOPT ide/coq.ml OCAMLOPT ide/wg_Segment.ml OCAMLOPT ide/wg_MessageView.ml OCAMLOPT ide/wg_Find.ml OCAMLOPT ide/fileOps.ml OCAMLOPT kernel/mod_subst.ml OCAMLOPT kernel/cbytecodes.ml OCAMLOPT kernel/nativevalues.ml OCAMLOPT intf/misctypes.ml OCAMLC intf/vernacexpr.ml OCAMLC pretyping/miscops.mli OCAMLC pretyping/redops.mli OCAMLC pretyping/pretyping.mli OCAMLC interp/genintern.mli OCAMLC interp/stdarg.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_using.mli OCAMLC proofs/proof_global.mli OCAMLC proofs/redexpr.mli OCAMLC parsing/pcoq.mli OCAMLC parsing/egramcoq.mli OCAMLC printing/pputils.mli OCAMLC printing/printer.mli OCAMLC printing/ppvernac.mli OCAMLC tactics/equality.mli OCAMLC tactics/inv.mli OCAMLC vernac/vernacprop.mli OCAMLC vernac/record.mli OCAMLC vernac/himsg.mli OCAMLC vernac/indschemes.mli OCAMLC vernac/mltop.mli OCAMLC vernac/vernacinterp.mli OCAMLC stm/vernac_classifier.mli OCAMLC toplevel/vernac.mli OCAMLC plugins/ltac/tacexpr.mli OCAMLC plugins/funind/glob_termops.mli OCAMLC plugins/micromega/certificate.ml OCAMLOPT checker/inductive.ml OCAMLOPT ide/wg_ProofView.ml OCAMLOPT ide/wg_Completion.ml OCAMLOPT ide/wg_Command.ml OCAMLOPT kernel/opaqueproof.ml OCAMLOPT kernel/cemitcodes.ml OCAMLOPT kernel/retroknowledge.ml OCAMLOPT kernel/vm.ml OCAMLOPT library/globnames.ml OCAMLOPT library/libobject.ml OCAMLOPT intf/locus.ml OCAMLC library/declaremods.mli OCAMLC pretyping/typeclasses.mli OCAMLC pretyping/unification.mli OCAMLC interp/dumpglob.mli OCAMLC interp/constrextern.mli OCAMLC interp/constrintern.mli OCAMLOPT proofs/miscprint.ml OCAMLC proofs/evar_refiner.mli OCAMLC proofs/tacmach.mli OCAMLC proofs/pfedit.mli OCAMLC proofs/clenv.mli OCAMLC parsing/egramml.mli OCAMLC vernac/lemmas.mli OCAMLC vernac/classes.mli OCAMLC vernac/assumptions.mli OCAMLC stm/stm.mli OCAMLC vernac/vernacentries.mli OCAMLC parsing/g_constr.ml OCAMLC toplevel/coqloop.mli OCAMLC parsing/g_prim.ml OCAMLC plugins/ltac/tacarg.mli OCAMLC plugins/ltac/pptactic.mli OCAMLC plugins/ltac/pltac.mli OCAMLC plugins/ltac/taccoerce.mli OCAMLC plugins/ltac/tacsubst.mli OCAMLC plugins/ltac/tactic_debug.mli OCAMLC plugins/ltac/tacenv.mli OCAMLC plugins/ltac/profile_ltac.mli OCAMLC plugins/ltac/tacintern.mli OCAMLC plugins/ltac/tactic_matching.mli OCAMLC plugins/ltac/tactic_option.mli OCAMLC plugins/ltac/extratactics.mli OCAMLC plugins/syntax/z_syntax.ml OCAMLC plugins/syntax/nat_syntax.ml OCAMLC plugins/setoid_ring/newring_ast.mli OCAMLC plugins/funind/indfun_common.mli OCAMLC plugins/funind/functional_principles_types.mli OCAMLC plugins/funind/indfun.mli OCAMLC plugins/syntax/int31_syntax.ml OCAMLC plugins/syntax/r_syntax.ml OCAMLC plugins/syntax/ascii_syntax.ml OCAMLC plugins/derive/g_derive.ml OCAMLC plugins/rtauto/refl_tauto.mli OCAMLC plugins/ssr/ssrparser.mli OCAMLOPT checker/typeops.ml OCAMLC ide/ide_slave.ml OCAMLOPT ide/wg_ScriptView.ml OCAMLOPT kernel/declarations.ml OCAMLOPT library/nametab.ml OCAMLOPT intf/evar_kinds.ml OCAMLOPT pretyping/locusops.ml OCAMLC proofs/clenvtac.mli OCAMLC tactics/tacticals.mli OCAMLC tactics/tactics.mli OCAMLC tactics/hints.mli OCAMLC tactics/autorewrite.mli OCAMLC vernac/metasyntax.mli OCAMLC vernac/class.mli OCAMLC vernac/declareDef.mli OCAMLC vernac/obligations.mli OCAMLC vernac/command.mli OCAMLC stm/proofBlockDelimiter.mli OCAMLC stm/proofworkertop.ml OCAMLC stm/tacworkertop.ml OCAMLC stm/queryworkertop.ml OCAMLC plugins/ltac/tacinterp.mli OCAMLC plugins/ltac/tacentries.mli OCAMLC plugins/ltac/tacarg.ml OCAMLC plugins/ltac/pptactic.ml OCAMLC plugins/ltac/pltac.ml OCAMLC plugins/ltac/taccoerce.ml OCAMLC plugins/ltac/tacenv.ml OCAMLC plugins/ltac/tacsubst.ml OCAMLC plugins/ltac/tactic_debug.ml OCAMLC plugins/ltac/tacintern.ml OCAMLC plugins/ltac/profile_ltac.ml OCAMLC plugins/ltac/tactic_matching.ml OCAMLC plugins/firstorder/sequent.mli OCAMLC plugins/quote/quote.ml OCAMLC plugins/setoid_ring/newring.mli OCAMLC plugins/omega/coq_omega.ml OCAMLC plugins/funind/recdef.mli OCAMLC plugins/funind/functional_principles_proofs.mli OCAMLC plugins/funind/merge.ml OCAMLC plugins/fourier/fourierR.ml OCAMLC plugins/micromega/coq_micromega.ml OCAMLC -pack -o plugins/syntax/ascii_syntax_plugin.cmo OCAMLC plugins/btauto/refl_btauto.ml OCAMLC plugins/ssrmatching/ssrmatching.mli OCAMLOPT checker/indtypes.ml OCAMLOPT ide/coqOps.ml OCAMLOPT checker/subtyping.ml OCAMLOPT kernel/declareops.ml OCAMLOPT library/univops.ml OCAMLC tactics/elim.mli OCAMLOPT library/lib.ml OCAMLC tactics/auto.mli OCAMLC tactics/eauto.mli OCAMLC tactics/class_tactics.mli OCAMLC parsing/g_vernac.ml OCAMLC plugins/ltac/evar_tactics.mli OCAMLC plugins/ltac/extraargs.mli OCAMLC plugins/ltac/profile_ltac_tactics.ml OCAMLC plugins/ltac/rewrite.mli OCAMLC plugins/ltac/g_eqdecide.ml OCAMLC plugins/ltac/tacentries.ml OCAMLC plugins/ltac/tacinterp.ml OCAMLC plugins/ltac/tactic_option.ml OCAMLC plugins/firstorder/rules.mli OCAMLC plugins/firstorder/ground.mli OCAMLC plugins/syntax/string_syntax.ml OCAMLC plugins/ltac/g_obligations.ml OCAMLC plugins/ltac/coretactics.ml OCAMLC plugins/ltac/g_auto.ml OCAMLC plugins/ltac/g_class.ml OCAMLC plugins/ltac/g_rewrite.ml OCAMLC plugins/ltac/g_tactic.ml OCAMLC plugins/ltac/evar_tactics.ml OCAMLC plugins/ltac/extraargs.ml OCAMLC plugins/ltac/extratactics.ml OCAMLC plugins/firstorder/instances.mli OCAMLC plugins/ltac/rewrite.ml File "plugins/ltac/tacentries.ml", line 219, characters 8-9: Warning 56: this match case is unreachable. Consider replacing it with a refutation case ' -> .' OCAMLOPT checker/mod_checking.ml OCAMLOPT kernel/pre_env.ml OCAMLOPT library/goptions.ml OCAMLOPT library/keys.ml OCAMLOPT vernac/locality.ml OCAMLOPT kernel/cbytegen.ml OCAMLOPT kernel/nativelambda.ml OCAMLOPT ide/session.ml OCAMLOPT checker/safe_typing.ml OCAMLOPT plugins/rtauto/proof_search.ml OCAMLC parsing/g_proofs.ml OCAMLOPT checker/check_stat.ml OCAMLOPT checker/check.ml OCAMLC plugins/ltac/g_ltac.ml OCAMLOPT kernel/nativecode.ml OCAMLOPT kernel/environ.ml OCAMLOPT checker/checker.ml OCAMLOPT ide/nanoPG.ml OCAMLC -pack -o plugins/ltac/ltac_plugin.cmo OCAMLOPT kernel/modops.ml OCAMLOPT kernel/csymtable.ml OCAMLOPT kernel/cClosure.ml OCAMLOPT -a -o checker/check.cmxa OCAMLC plugins/firstorder/g_ground.ml OCAMLC plugins/quote/g_quote.ml OCAMLC plugins/setoid_ring/g_newring.ml OCAMLC plugins/cc/g_congruence.ml OCAMLC plugins/omega/g_omega.ml OCAMLC plugins/extraction/g_extraction.ml OCAMLC plugins/funind/invfun.ml OCAMLC plugins/micromega/g_micromega.ml OCAMLC plugins/fourier/g_fourier.ml OCAMLC plugins/nsatz/g_nsatz.ml OCAMLC plugins/ssrmatching/ssrmatching.ml OCAMLC plugins/btauto/g_btauto.ml OCAMLC plugins/rtauto/g_rtauto.ml OCAMLOPT -o bin/coqchk OCAMLOPT ide/coqide.ml OCAMLOPT kernel/reduction.ml OCAMLOPT kernel/nativelib.ml OCAMLOPT kernel/nativelibrary.ml OCAMLC -pack -o plugins/omega/omega_plugin.cmo OCAMLC plugins/romega/refl_omega.ml OCAMLC plugins/funind/g_indfun.ml OCAMLOPT kernel/nativeconv.ml OCAMLOPT kernel/vconv.ml OCAMLOPT kernel/type_errors.ml OCAMLC plugins/romega/g_romega.ml true bin/coqchk true bin/coqchk OCAMLC -pack -o plugins/ssrmatching/ssrmatching_plugin.cmo OCAMLOPT kernel/inductive.ml OCAMLC plugins/ssr/ssrast.mli OCAMLC plugins/ssr/ssrcommon.mli OCAMLC plugins/ssr/ssrtacticals.mli OCAMLC plugins/ssr/ssrelim.mli OCAMLC plugins/ssr/ssrbwd.mli OCAMLC plugins/ssr/ssrequality.mli OCAMLC plugins/ssr/ssrfwd.mli OCAMLC plugins/ssr/ssrprinters.mli OCAMLC plugins/ssr/ssripats.mli OCAMLOPT -a -o ide/ide.cmxa OCAMLC plugins/ssr/ssrview.mli OCAMLOPT kernel/typeops.ml OCAMLOPT -o bin/coqide OCAMLOPT kernel/cooking.ml OCAMLOPT kernel/subtyping.ml OCAMLOPT kernel/indtypes.ml OCAMLOPT kernel/mod_typing.ml OCAMLOPT kernel/term_typing.ml OCAMLOPT kernel/safe_typing.ml true bin/coqide OCAMLOPT library/global.ml OCAMLOPT -a -o kernel/kernel.cmxa OCAMLOPT library/decls.ml OCAMLOPT engine/universes.ml OCAMLOPT library/heads.ml OCAMLOPT stm/asyncTaskQueue.ml OCAMLOPT engine/uState.ml OCAMLOPT engine/evd.ml OCAMLOPT engine/proofview_monad.ml OCAMLOPT engine/eConstr.ml OCAMLOPT intf/pattern.ml OCAMLOPT pretyping/pretype_errors.ml OCAMLOPT engine/namegen.ml OCAMLOPT engine/termops.ml OCAMLOPT pretyping/find_subterm.ml OCAMLOPT vernac/discharge.ml OCAMLOPT tactics/term_dnet.ml OCAMLOPT engine/evarutil.ml OCAMLOPT pretyping/reductionops.ml OCAMLOPT engine/proofview.ml OCAMLOPT engine/ftactic.ml OCAMLOPT engine/geninterp.ml OCAMLOPT -a -o engine/engine.cmxa OCAMLOPT interp/stdarg.ml OCAMLOPT intf/glob_term.ml OCAMLOPT pretyping/cbv.ml OCAMLOPT pretyping/evardefine.ml OCAMLOPT plugins/firstorder/unify.ml OCAMLOPT pretyping/recordops.ml OCAMLOPT pretyping/inductiveops.ml OCAMLOPT parsing/pcoq.ml OCAMLOPT plugins/ltac/tacarg.ml OCAMLOPT intf/constrexpr.ml OCAMLOPT intf/genredexpr.ml OCAMLOPT intf/tactypes.ml OCAMLOPT pretyping/typeclasses_errors.ml OCAMLOPT intf/notation_term.ml OCAMLOPT pretyping/arguments_renaming.ml OCAMLOPT pretyping/nativenorm.ml OCAMLOPT pretyping/indrec.ml OCAMLOPT pretyping/vnorm.ml OCAMLOPT pretyping/miscops.ml OCAMLOPT pretyping/redops.ml OCAMLOPT printing/pputils.ml OCAMLOPT intf/vernacexpr.ml OCAMLOPT plugins/ltac/pltac.ml OCAMLOPT parsing/g_prim.ml OCAMLOPT interp/impargs.ml OCAMLOPT pretyping/retyping.ml OCAMLOPT interp/constrexpr_ops.ml OCAMLOPT pretyping/glob_ops.ml OCAMLOPT library/declaremods.ml OCAMLOPT -a -o intf/intf.cmxa OCAMLOPT parsing/egramml.ml OCAMLOPT proofs/proof_using.ml OCAMLOPT vernac/vernacprop.ml OCAMLOPT vernac/mltop.ml OCAMLOPT parsing/g_constr.ml OCAMLOPT vernac/vernacinterp.ml OCAMLOPT pretyping/patternops.ml OCAMLOPT pretyping/evarsolve.ml OCAMLOPT library/library.ml OCAMLOPT tactics/btermdn.ml OCAMLOPT pretyping/constr_matching.ml OCAMLOPT library/states.ml OCAMLOPT library/coqlib.ml OCAMLOPT pretyping/detyping.ml OCAMLOPT plugins/ltac/tactic_matching.ml OCAMLOPT -a -o library/library.cmxa OCAMLOPT pretyping/evarconv.ml OCAMLOPT pretyping/program.ml OCAMLOPT interp/genintern.ml OCAMLOPT interp/notation_ops.ml OCAMLOPT pretyping/typing.ml OCAMLOPT pretyping/tacred.ml OCAMLOPT interp/reserve.ml OCAMLOPT pretyping/classops.ml OCAMLOPT proofs/redexpr.ml OCAMLOPT plugins/ltac/taccoerce.ml OCAMLOPT pretyping/typeclasses.ml OCAMLOPT proofs/goal.ml OCAMLOPT interp/dumpglob.ml OCAMLOPT interp/notation.ml OCAMLOPT pretyping/coercion.ml OCAMLOPT proofs/logic.ml OCAMLOPT pretyping/cases.ml OCAMLOPT proofs/refine.ml OCAMLOPT interp/declare.ml OCAMLOPT interp/syntax_def.ml OCAMLOPT plugins/syntax/z_syntax.ml OCAMLOPT plugins/syntax/nat_syntax.ml OCAMLOPT plugins/syntax/int31_syntax.ml OCAMLOPT plugins/syntax/r_syntax.ml OCAMLOPT plugins/syntax/ascii_syntax.ml OCAMLOPT proofs/refiner.ml OCAMLOPT -pack -o plugins/syntax/nat_syntax_plugin.cmx OCAMLOPT -pack -o plugins/syntax/int31_syntax_plugin.cmx OCAMLOPT -pack -o plugins/syntax/r_syntax_plugin.cmx OCAMLOPT -shared -o plugins/syntax/nat_syntax_plugin.cmxs OCAMLOPT interp/smartlocate.ml OCAMLOPT -pack -o plugins/syntax/ascii_syntax_plugin.cmx OCAMLOPT -pack -o plugins/syntax/z_syntax_plugin.cmx OCAMLOPT -shared -o plugins/syntax/int31_syntax_plugin.cmxs OCAMLOPT tactics/ind_tables.ml OCAMLOPT -shared -o plugins/syntax/r_syntax_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/z_syntax_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/ascii_syntax_plugin.cmxs OCAMLOPT plugins/syntax/string_syntax.ml OCAMLOPT interp/topconstr.ml OCAMLOPT tactics/elimschemes.ml OCAMLOPT tactics/eqschemes.ml OCAMLOPT -pack -o plugins/syntax/string_syntax_plugin.cmx OCAMLOPT pretyping/pretyping.ml OCAMLOPT interp/implicit_quantifiers.ml OCAMLOPT parsing/egramcoq.ml OCAMLOPT -shared -o plugins/syntax/string_syntax_plugin.cmxs OCAMLOPT -a -o parsing/parsing.cmxa OCAMLOPT interp/constrintern.ml OCAMLOPT proofs/evar_refiner.ml OCAMLOPT pretyping/unification.ml OCAMLOPT interp/constrextern.ml OCAMLOPT interp/modintern.ml OCAMLOPT proofs/tacmach.ml OCAMLOPT vernac/metasyntax.ml OCAMLOPT proofs/proof.ml OCAMLOPT -a -o pretyping/pretyping.cmxa OCAMLOPT proofs/clenv.ml OCAMLOPT plugins/cc/ccalgo.ml OCAMLOPT plugins/romega/const_omega.ml OCAMLOPT tactics/hipattern.ml OCAMLOPT plugins/micromega/certificate.ml OCAMLOPT proofs/proof_global.ml OCAMLOPT proofs/clenvtac.ml OCAMLOPT proofs/pfedit.ml OCAMLOPT stm/vernac_classifier.ml OCAMLOPT plugins/derive/derive.ml OCAMLOPT plugins/firstorder/formula.ml OCAMLOPT plugins/cc/ccproof.ml OCAMLOPT -a -o interp/interp.cmxa OCAMLOPT printing/ppconstr.ml OCAMLOPT tactics/tacticals.ml OCAMLOPT plugins/derive/g_derive.ml OCAMLOPT vernac/search.ml OCAMLOPT -a -o proofs/proofs.cmxa OCAMLOPT -pack -o plugins/derive/derive_plugin.cmx OCAMLOPT -shared -o plugins/derive/derive_plugin.cmxs OCAMLOPT printing/printer.ml OCAMLOPT printing/ppvernac.ml OCAMLOPT printing/printmod.ml OCAMLOPT tactics/hints.ml OCAMLOPT vernac/himsg.ml OCAMLOPT vernac/assumptions.ml OCAMLOPT tactics/tactics.ml OCAMLOPT plugins/ltac/pptactic.ml OCAMLOPT plugins/ltac/tacsubst.ml OCAMLOPT plugins/extraction/table.ml OCAMLOPT plugins/ltac/tacenv.ml OCAMLOPT printing/prettyp.ml OCAMLOPT plugins/extraction/mlutil.ml OCAMLOPT vernac/explainErr.ml OCAMLOPT plugins/firstorder/sequent.ml OCAMLOPT plugins/ltac/tacintern.ml OCAMLOPT plugins/ltac/tactic_debug.ml OCAMLOPT -a -o printing/printing.cmxa OCAMLOPT plugins/ltac/tacentries.ml OCAMLOPT plugins/extraction/extraction.ml OCAMLOPT plugins/extraction/common.ml OCAMLOPT plugins/extraction/modutil.ml File "plugins/ltac/tacentries.ml", line 219, characters 8-9: Warning 56: this match case is unreachable. Consider replacing it with a refutation case ' -> .' OCAMLOPT plugins/extraction/haskell.ml OCAMLOPT plugins/extraction/json.ml OCAMLOPT plugins/extraction/ocaml.ml OCAMLOPT plugins/extraction/scheme.ml OCAMLOPT tactics/elim.ml OCAMLOPT tactics/contradiction.ml OCAMLOPT tactics/leminv.ml OCAMLOPT tactics/auto.ml OCAMLOPT tactics/equality.ml OCAMLOPT vernac/lemmas.ml OCAMLOPT plugins/firstorder/rules.ml OCAMLOPT plugins/quote/quote.ml OCAMLOPT plugins/micromega/coq_micromega.ml OCAMLOPT plugins/btauto/refl_btauto.ml OCAMLOPT plugins/nsatz/nsatz.ml OCAMLOPT plugins/firstorder/instances.ml OCAMLOPT tactics/eauto.ml OCAMLOPT vernac/declareDef.ml OCAMLOPT vernac/class.ml OCAMLOPT vernac/obligations.ml OCAMLOPT tactics/class_tactics.ml OCAMLOPT tactics/eqdecide.ml OCAMLOPT tactics/autorewrite.ml OCAMLOPT tactics/inv.ml OCAMLOPT vernac/auto_ind_decl.ml OCAMLOPT plugins/cc/cctac.ml OCAMLOPT plugins/funind/indfun_common.ml OCAMLOPT plugins/fourier/fourierR.ml OCAMLOPT plugins/omega/coq_omega.ml OCAMLOPT plugins/funind/glob_termops.ml OCAMLOPT -a -o tactics/tactics.cmxa OCAMLOPT vernac/indschemes.ml OCAMLOPT vernac/command.ml OCAMLOPT vernac/classes.ml OCAMLOPT plugins/funind/merge.ml OCAMLOPT plugins/funind/glob_term_to_relation.ml OCAMLOPT vernac/record.ml OCAMLOPT vernac/vernacentries.ml OCAMLOPT stm/stm.ml OCAMLOPT plugins/extraction/extract_env.ml OCAMLOPT -a -o vernac/vernac.cmxa OCAMLOPT stm/vio_checking.ml OCAMLOPT toplevel/vernac.ml OCAMLOPT stm/proofBlockDelimiter.ml OCAMLOPT plugins/ltac/profile_ltac.ml OCAMLOPT toplevel/coqloop.ml OCAMLOPT toplevel/coqinit.ml OCAMLOPT -a -o stm/stm.cmxa OCAMLOPT plugins/ltac/profile_ltac_tactics.ml OCAMLOPT plugins/ltac/tacinterp.ml OCAMLOPT parsing/g_vernac.ml OCAMLOPT toplevel/coqtop.ml OCAMLOPT stm/proofworkertop.ml OCAMLOPT stm/tacworkertop.ml OCAMLOPT stm/queryworkertop.ml OCAMLOPT -a -o toplevel/toplevel.cmxa OCAMLOPT ide/ide_slave.ml OCAMLOPT -shared -o stm/proofworkertop.cmxs OCAMLOPT -shared -o stm/queryworkertop.cmxs OCAMLOPT -shared -o stm/tacworkertop.cmxs OCAMLOPT -a -o ide/coqidetop.cmxa OCAMLOPT -shared -o ide/coqidetop.cmxs OCAMLBEST -o bin/fake_ide OCAMLOPT plugins/ltac/extraargs.ml OCAMLOPT plugins/ltac/tactic_option.ml OCAMLOPT plugins/ltac/evar_tactics.ml OCAMLOPT plugins/ltac/g_class.ml OCAMLOPT plugins/ltac/rewrite.ml OCAMLOPT plugins/ltac/g_auto.ml OCAMLOPT plugins/ltac/g_eqdecide.ml OCAMLOPT parsing/g_proofs.ml OCAMLOPT plugins/ltac/coretactics.ml OCAMLOPT plugins/ltac/extratactics.ml OCAMLOPT plugins/ltac/g_tactic.ml OCAMLOPT plugins/ltac/g_obligations.ml OCAMLOPT -a -o parsing/highparsing.cmxa OCAMLOPT plugins/ltac/g_ltac.ml COQMKTOP -o bin/coqtop findlib: [WARNING] Interface profile.cmi occurs in several directories: /usr/pkg/lib/ocaml/compiler-libs, lib findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/pkg/lib/ocaml/compiler-libs, /usr/pkg/lib/ocaml OCAMLOPT plugins/ltac/g_rewrite.ml true bin/coqtop true bin/coqtop OCAMLOPT -pack -o plugins/ltac/ltac_plugin.cmx OCAMLOPT -shared -o plugins/ltac/ltac_plugin.cmxs OCAMLOPT plugins/cc/g_congruence.ml OCAMLOPT plugins/firstorder/ground.ml OCAMLOPT plugins/quote/g_quote.ml OCAMLOPT plugins/omega/g_omega.ml OCAMLOPT plugins/extraction/g_extraction.ml OCAMLOPT plugins/ltac/tauto.ml OCAMLOPT plugins/fourier/g_fourier.ml OCAMLOPT plugins/micromega/g_micromega.ml OCAMLOPT plugins/btauto/g_btauto.ml OCAMLOPT plugins/rtauto/refl_tauto.ml OCAMLOPT plugins/funind/invfun.ml OCAMLOPT plugins/ssrmatching/ssrmatching.ml OCAMLOPT plugins/nsatz/g_nsatz.ml OCAMLOPT -pack -o plugins/omega/omega_plugin.cmx OCAMLOPT -pack -o plugins/btauto/btauto_plugin.cmx OCAMLOPT -pack -o plugins/cc/cc_plugin.cmx OCAMLOPT -pack -o plugins/fourier/fourier_plugin.cmx OCAMLOPT -pack -o plugins/nsatz/nsatz_plugin.cmx OCAMLOPT -pack -o plugins/quote/quote_plugin.cmx OCAMLOPT plugins/firstorder/g_ground.ml OCAMLOPT -pack -o plugins/micromega/micromega_plugin.cmx OCAMLOPT -pack -o plugins/ltac/tauto_plugin.cmx OCAMLOPT plugins/rtauto/g_rtauto.ml OCAMLOPT -shared -o plugins/omega/omega_plugin.cmxs OCAMLOPT plugins/romega/refl_omega.ml OCAMLOPT -shared -o plugins/btauto/btauto_plugin.cmxs OCAMLOPT -pack -o plugins/extraction/extraction_plugin.cmx COQC -noinit theories/Init/Notations.v OCAMLOPT -shared -o plugins/cc/cc_plugin.cmxs OCAMLOPT -shared -o plugins/fourier/fourier_plugin.cmxs OCAMLOPT -shared -o plugins/nsatz/nsatz_plugin.cmxs OCAMLOPT -shared -o plugins/ltac/tauto_plugin.cmxs OCAMLOPT plugins/setoid_ring/newring.ml OCAMLOPT -shared -o plugins/quote/quote_plugin.cmxs OCAMLOPT -pack -o plugins/rtauto/rtauto_plugin.cmx OCAMLOPT -pack -o plugins/firstorder/ground_plugin.cmx OCAMLOPT -shared -o plugins/extraction/extraction_plugin.cmxs OCAMLOPT -shared -o plugins/micromega/micromega_plugin.cmxs OCAMLOPT plugins/funind/recdef.ml OCAMLOPT -pack -o plugins/ssrmatching/ssrmatching_plugin.cmx OCAMLOPT -shared -o plugins/rtauto/rtauto_plugin.cmxs OCAMLOPT -shared -o plugins/firstorder/ground_plugin.cmxs OCAMLOPT plugins/ssr/ssrprinters.ml OCAMLOPT -shared -o plugins/ssrmatching/ssrmatching_plugin.cmxs OCAMLOPT plugins/romega/g_romega.ml OCAMLOPT plugins/ssr/ssrcommon.ml COQC -noinit theories/Init/Logic.v OCAMLOPT plugins/setoid_ring/g_newring.ml OCAMLOPT -pack -o plugins/romega/romega_plugin.cmx OCAMLOPT -shared -o plugins/romega/romega_plugin.cmxs OCAMLOPT -pack -o plugins/setoid_ring/newring_plugin.cmx OCAMLOPT -shared -o plugins/setoid_ring/newring_plugin.cmxs OCAMLOPT plugins/funind/functional_principles_proofs.ml OCAMLOPT plugins/ssr/ssrelim.ml OCAMLOPT plugins/ssr/ssrview.ml OCAMLOPT plugins/ssr/ssrtacticals.ml OCAMLOPT plugins/ssr/ssrbwd.ml OCAMLOPT plugins/ssr/ssrequality.ml OCAMLOPT plugins/funind/functional_principles_types.ml COQC -noinit theories/Init/Datatypes.v OCAMLOPT plugins/ssr/ssripats.ml OCAMLOPT plugins/funind/indfun.ml OCAMLOPT plugins/ssr/ssrfwd.ml COQC -noinit theories/Init/Specif.v COQC -noinit theories/Init/Nat.v COQC -noinit theories/Init/Wf.v COQC -noinit theories/Init/Tauto.v OCAMLOPT plugins/funind/g_indfun.ml COQC -noinit theories/Init/Logic_Type.v OCAMLOPT plugins/ssr/ssrparser.ml OCAMLOPT -pack -o plugins/funind/recdef_plugin.cmx OCAMLOPT -shared -o plugins/funind/recdef_plugin.cmxs COQC -noinit theories/Init/Peano.v COQC -noinit theories/Init/Tactics.v OCAMLOPT plugins/ssr/ssrvernac.ml COQC -noinit theories/Init/Prelude.v OCAMLOPT -pack -o plugins/ssr/ssreflect_plugin.cmx COQC theories/Program/Basics.v COQC theories/Program/Tactics.v COQC theories/Relations/Relation_Definitions.v COQC theories/Logic/Decidable.v COQC theories/Logic/EqdepFacts.v COQC theories/Numbers/BinNums.v COQC theories/Bool/Bool.v COQC theories/Bool/Sumbool.v COQC theories/Bool/DecBool.v COQC theories/Logic/FunctionalExtensionality.v COQC plugins/extraction/Extraction.v COQC plugins/quote/Quote.v COQC theories/Sets/Ensembles.v COQC theories/Compat/AdmitAxiom.v COQC theories/Sets/Relations_1.v COQC theories/Lists/Streams.v COQC theories/Logic/Berardi.v COQC theories/Logic/PropExtensionalityFacts.v COQC theories/Logic/Hurkens.v COQC theories/Logic/RelationalChoice.v COQC theories/Logic/ExtensionalFunctionRepresentative.v COQC theories/Logic/ExtensionalityFacts.v COQC theories/Logic/PropFacts.v COQC theories/Logic/SetIsType.v COQC theories/Sets/Permut.v COQC theories/Unicode/Utf8_core.v COQC theories/Wellfounded/Inclusion.v COQC theories/Wellfounded/Inverse_Image.v COQC plugins/derive/Derive.v COQC plugins/extraction/ExtrHaskellBasic.v COQC plugins/extraction/ExtrOcamlBasic.v COQC plugins/ltac/Ltac.v COQC plugins/setoid_ring/Algebra_syntax.v COQC plugins/ssrmatching/ssrmatching.v OCAMLOPT -shared -o plugins/ssr/ssreflect_plugin.cmxs COQC theories/Classes/Init.v COQC theories/Relations/Relation_Operators.v COQC theories/Logic/Eqdep_dec.v COQC theories/PArith/BinPosDef.v COQC theories/Program/Utils.v COQC theories/Logic/ProofIrrelevanceFacts.v COQC theories/Logic/Eqdep.v COQC theories/Program/Combinators.v COQC plugins/funind/FunInd.v COQC theories/Sets/Constructive_sets.v COQC theories/Sets/Partial_Order.v COQC theories/Sets/Relations_1_facts.v COQC theories/Sets/Relations_2.v COQC theories/Sets/Uniset.v COQC theories/Unicode/Utf8.v COQC plugins/ssr/ssreflect.v COQC theories/Classes/RelationClasses.v COQC theories/Classes/CRelationClasses.v COQC theories/Bool/BoolEq.v COQC theories/Bool/IfProp.v COQC theories/Logic/ProofIrrelevance.v COQC theories/Logic/JMeq.v COQC theories/Wellfounded/Disjoint_Union.v COQC theories/Wellfounded/Transitive_Closure.v COQC theories/Wellfounded/Well_Ordering.v COQC theories/Relations/Operators_Properties.v COQC theories/Compat/Coq86.v COQC theories/Sets/Finite_sets.v COQC theories/Lists/StreamMemo.v COQC theories/Sets/Relations_2_facts.v COQC theories/Sets/Relations_3.v COQC theories/Sets/Cpo.v COQC plugins/ssr/ssrfun.v COQC theories/Program/Wf.v COQC theories/Wellfounded/Lexicographic_Product.v COQC theories/Wellfounded/Union.v COQC theories/Program/Equality.v COQC theories/Compat/Coq85.v COQC theories/Classes/CMorphisms.v COQC theories/Sets/Relations_3_facts.v COQC theories/Sets/Powerset.v COQC theories/Relations/Relations.v COQC theories/Classes/Morphisms.v COQC theories/Program/Subset.v COQC plugins/ssr/ssrbool.v COQC theories/Sets/Powerset_facts.v COQC theories/Classes/CEquivalence.v COQC theories/Classes/Equivalence.v COQC theories/Classes/Morphisms_Prop.v COQC theories/Classes/SetoidTactics.v COQC theories/Setoids/Setoid.v COQC theories/Numbers/NumPrelude.v COQC theories/Structures/Equalities.v COQC theories/Structures/Orders.v COQC theories/Structures/OrdersTac.v COQC theories/Structures/OrdersFacts.v COQC theories/Structures/GenericMinMax.v COQC theories/Numbers/NatInt/NZAxioms.v COQC theories/Numbers/NatInt/NZBase.v COQC theories/Numbers/NatInt/NZOrder.v COQC theories/Numbers/NatInt/NZAdd.v COQC theories/Numbers/NatInt/NZMul.v COQC theories/Numbers/NatInt/NZAddOrder.v COQC theories/Numbers/NatInt/NZMulOrder.v COQC theories/Numbers/NatInt/NZPow.v COQC theories/Numbers/NatInt/NZSqrt.v COQC theories/Numbers/NatInt/NZDiv.v COQC theories/Numbers/NatInt/NZGcd.v COQC theories/Numbers/NatInt/NZParity.v COQC theories/Numbers/NatInt/NZProperties.v COQC theories/Numbers/NatInt/NZLog.v COQC theories/Numbers/NatInt/NZBits.v COQC theories/Numbers/Integer/Abstract/ZAxioms.v COQC theories/Numbers/Natural/Abstract/NAxioms.v COQC theories/Numbers/Integer/Abstract/ZBase.v COQC theories/Numbers/Natural/Abstract/NBase.v COQC theories/Numbers/Integer/Abstract/ZAdd.v COQC theories/Numbers/Natural/Abstract/NIso.v COQC theories/Numbers/Natural/Abstract/NAdd.v COQC theories/Numbers/Integer/Abstract/ZMul.v COQC theories/Numbers/Natural/Abstract/NOrder.v COQC theories/Numbers/Integer/Abstract/ZLt.v COQC theories/Numbers/Integer/Abstract/ZAddOrder.v COQC theories/Numbers/Natural/Abstract/NAddOrder.v COQC theories/Numbers/Natural/Abstract/NMulOrder.v COQC theories/Numbers/Integer/Abstract/ZMulOrder.v COQC theories/Numbers/Natural/Abstract/NSub.v COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v COQC theories/Numbers/Integer/Abstract/ZParity.v COQC theories/Numbers/Integer/Abstract/ZMaxMin.v COQC theories/Numbers/Natural/Abstract/NParity.v COQC theories/Numbers/Natural/Abstract/NSqrt.v COQC theories/Numbers/Natural/Abstract/NDiv.v COQC theories/Numbers/Natural/Abstract/NMaxMin.v COQC theories/Numbers/Natural/Abstract/NGcd.v COQC theories/Numbers/Natural/Abstract/NStrongRec.v COQC theories/Numbers/Natural/Abstract/NPow.v COQC theories/Numbers/Natural/Abstract/NLcm.v COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v COQC theories/Numbers/Integer/Abstract/ZPow.v COQC theories/Numbers/Integer/Abstract/ZGcd.v COQC theories/Numbers/Integer/Abstract/ZDivEucl.v COQC theories/Numbers/Integer/Abstract/ZDivFloor.v COQC theories/Numbers/Natural/Abstract/NLog.v COQC theories/Numbers/Natural/Abstract/NBits.v COQC theories/Numbers/Integer/Abstract/ZBits.v COQC theories/Numbers/Integer/Abstract/ZLcm.v COQC theories/Numbers/Natural/Abstract/NProperties.v COQC theories/Arith/PeanoNat.v COQC theories/Arith/EqNat.v COQC theories/Arith/Min.v COQC theories/Arith/Max.v COQC theories/Arith/Le.v COQC theories/Arith/Even.v COQC theories/Arith/Lt.v COQC theories/Arith/Minus.v COQC theories/Arith/Between.v COQC theories/Arith/Peano_dec.v COQC theories/Arith/Plus.v COQC theories/Arith/Mult.v COQC theories/PArith/BinPos.v COQC theories/Arith/Gt.v COQC theories/Sets/Multiset.v COQC theories/Numbers/NatInt/NZDomain.v COQC theories/Arith/Div2.v COQC theories/Numbers/Natural/Peano/NPeano.v COQC theories/Numbers/Integer/Abstract/ZProperties.v COQC theories/Lists/List.v COQC theories/Arith/Compare_dec.v COQC theories/Arith/Factorial.v COQC theories/Arith/Wf_nat.v COQC theories/Arith/Bool_nat.v COQC theories/Arith/Arith_base.v COQC plugins/funind/Recdef.v COQC theories/Logic/ClassicalFacts.v COQC theories/Arith/Euclid.v COQC theories/Vectors/Fin.v COQC theories/Arith/Compare.v COQC theories/Logic/PropExtensionality.v COQC theories/Logic/Classical_Prop.v COQC theories/PArith/Pnat.v COQC theories/PArith/POrderedType.v COQC theories/NArith/BinNatDef.v COQC theories/Logic/Classical_Pred_Type.v COQC theories/Lists/ListTactics.v COQC theories/Sorting/Sorted.v COQC theories/Lists/ListDec.v COQC theories/Logic/WeakFan.v COQC plugins/setoid_ring/BinList.v COQC theories/Numbers/NaryFunctions.v COQC plugins/micromega/Refl.v COQC plugins/rtauto/Bintree.v COQC theories/Wellfounded/Lexicographic_Exponentiation.v COQC theories/Lists/ListSet.v COQC theories/Vectors/VectorDef.v COQC theories/NArith/BinNat.v COQC theories/Logic/Classical.v COQC theories/PArith/PArith.v COQC theories/Logic/FinFun.v COQC theories/Logic/ClassicalUniqueChoice.v COQC theories/Sets/Classical_sets.v COQC theories/Lists/SetoidList.v COQC plugins/micromega/Tauto.v COQC plugins/rtauto/Rtauto.v COQC theories/Vectors/VectorSpec.v COQC theories/Wellfounded/Wellfounded.v COQC theories/Sets/Powerset_Classical_facts.v COQC theories/Sorting/Permutation.v COQC plugins/setoid_ring/Ring_theory.v COQC theories/ZArith/BinIntDef.v COQC theories/NArith/Nnat.v COQC theories/NArith/Nsqrt_def.v COQC theories/NArith/Ngcd_def.v COQC theories/Numbers/Natural/Binary/NBinary.v COQC theories/NArith/Ndiv_def.v COQC theories/Vectors/VectorEq.v COQC theories/Sets/Finite_sets_facts.v COQC theories/Vectors/Vector.v COQC theories/Structures/DecidableType.v COQC theories/Classes/RelationPairs.v COQC theories/Structures/OrderedType.v COQC theories/Lists/SetoidPermutation.v COQC theories/Sorting/Mergesort.v COQC theories/Strings/Ascii.v COQC theories/ZArith/BinInt.v COQC theories/Sets/Image.v COQC theories/Bool/Bvector.v COQC theories/Structures/EqualitiesFacts.v COQC theories/MSets/MSetInterface.v COQC theories/Numbers/Natural/Abstract/NDefOps.v COQC theories/Structures/OrderedTypeAlt.v COQC theories/FSets/FSetInterface.v COQC theories/FSets/FMapInterface.v COQC theories/Structures/OrdersAlt.v COQC theories/Sorting/Sorting.v COQC theories/Sets/Infinite_sets.v COQC theories/Program/Syntax.v COQC theories/NArith/Ndigits.v COQC theories/FSets/FMapList.v COQC theories/FSets/FMapWeakList.v COQC theories/FSets/FSetBridge.v COQC theories/Program/Program.v COQC theories/Structures/OrdersLists.v COQC theories/Sets/Integers.v COQC theories/MSets/MSetWeakList.v COQC theories/MSets/MSetGenTree.v COQC theories/Classes/EquivDec.v COQC theories/Classes/SetoidClass.v COQC theories/Classes/Morphisms_Relations.v COQC theories/MSets/MSetList.v COQC theories/ZArith/Zeven.v COQC theories/ZArith/Zcompare.v COQC theories/ZArith/Znat.v COQC plugins/setoid_ring/Ring_polynom.v COQC theories/ZArith/Int.v COQC theories/ZArith/Zpow_def.v COQC theories/Numbers/Integer/Binary/ZBinary.v COQC theories/Structures/OrdersEx.v COQC plugins/micromega/Env.v COQC theories/ZArith/Zeuclid.v COQC theories/ZArith/Zpow_alt.v COQC theories/ZArith/Zorder.v COQC theories/MSets/MSetRBT.v COQC plugins/micromega/EnvRing.v COQC plugins/omega/OmegaLemmas.v COQC theories/MSets/MSetAVL.v COQC theories/ZArith/ZArith_dec.v COQC theories/ZArith/Zmin.v COQC theories/ZArith/Zmax.v COQC theories/ZArith/auxiliary.v COQC theories/ZArith/Zminmax.v COQC theories/ZArith/Zmisc.v COQC theories/ZArith/Wf_Z.v COQC theories/ZArith/Zabs.v COQC theories/ZArith/Zbool.v COQC theories/ZArith/Zhints.v COQC theories/ZArith/ZArith_base.v COQC theories/MSets/MSetPositive.v COQC plugins/romega/ReflOmegaCore.v COQC plugins/setoid_ring/Ncring.v COQC theories/Reals/Rdefinitions.v COQC plugins/setoid_ring/InitialRing.v COQC theories/Reals/Rpow_def.v COQC theories/Reals/Raxioms.v COQC plugins/setoid_ring/Ncring_polynom.v COQC plugins/setoid_ring/Ring_tac.v COQC plugins/setoid_ring/Ring_base.v COQC plugins/setoid_ring/Ring.v COQC plugins/setoid_ring/ZArithRing.v COQC plugins/setoid_ring/NArithRing.v COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v COQC plugins/setoid_ring/Field_theory.v COQC plugins/micromega/OrderedRing.v COQC plugins/setoid_ring/ArithRing.v COQC theories/Arith/Arith.v COQC theories/NArith/NArith.v COQC plugins/omega/PreOmega.v COQC theories/Classes/SetoidDec.v COQC theories/Bool/Zerob.v COQC theories/NArith/Ndec.v COQC theories/Logic/ConstructiveEpsilon.v COQC theories/NArith/Ndist.v COQC theories/Strings/String.v COQC theories/Logic/ChoiceFacts.v COQC plugins/extraction/ExtrHaskellNatNum.v COQC plugins/extraction/ExtrOcamlNatInt.v COQC plugins/extraction/ExtrOcamlNatBigInt.v COQC plugins/micromega/RingMicromega.v COQC plugins/extraction/ExtrHaskellNatInt.v COQC plugins/extraction/ExtrHaskellNatInteger.v COQC plugins/omega/Omega.v COQC plugins/omega/OmegaPlugin.v COQC plugins/omega/OmegaTactic.v COQC plugins/extraction/ExtrOcamlString.v COQC plugins/extraction/ExtrHaskellString.v COQC theories/Logic/WKL.v COQC theories/Sorting/PermutSetoid.v COQC theories/ZArith/Zsqrt_compat.v COQC theories/ZArith/Zwf.v COQC theories/ZArith/Zcomplements.v COQC plugins/romega/ROmega.v COQC theories/Logic/Description.v COQC theories/Logic/ClassicalEpsilon.v COQC theories/Logic/ClassicalChoice.v COQC theories/Logic/Epsilon.v COQC theories/Logic/IndefiniteDescription.v COQC theories/Logic/Diaconescu.v COQC theories/Logic/ClassicalDescription.v COQC theories/Logic/SetoidChoice.v COQC theories/ZArith/Zdiv.v COQC theories/ZArith/Zpower.v COQC theories/Sorting/Heap.v COQC theories/Sorting/PermutEq.v COQC plugins/setoid_ring/Field_tac.v COQC plugins/setoid_ring/Field.v COQC theories/ZArith/Zlogarithm.v COQC theories/ZArith/Znumtheory.v COQC theories/ZArith/Zquot.v COQC plugins/setoid_ring/RealField.v COQC theories/Reals/RIneq.v COQC theories/ZArith/ZArith.v COQC theories/FSets/FMapAVL.v COQC theories/Structures/OrderedTypeEx.v COQC theories/Numbers/Cyclic/Abstract/DoubleType.v COQC theories/Classes/DecidableClass.v COQC plugins/micromega/VarMap.v COQC theories/ZArith/Zdigits.v COQC plugins/extraction/ExtrHaskellZNum.v COQC plugins/extraction/ExtrOcamlBigIntConv.v COQC theories/QArith/QArith_base.v COQC plugins/extraction/ExtrOcamlIntConv.v COQC plugins/extraction/ExtrOcamlZBigInt.v COQC plugins/extraction/ExtrOcamlZInt.v COQC plugins/micromega/ZCoeff.v COQC theories/ZArith/Zpow_facts.v COQC theories/ZArith/Zgcd_alt.v COQC theories/Reals/DiscrR.v COQC theories/Reals/Rlogic.v COQC plugins/btauto/Algebra.v COQC theories/Numbers/Cyclic/Int31/Int31.v COQC plugins/extraction/ExtrHaskellZInt.v COQC plugins/extraction/ExtrHaskellZInteger.v COQC theories/Reals/Rbase.v COQC theories/FSets/FMapPositive.v COQC theories/Structures/DecidableTypeEx.v COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v COQC theories/FSets/FSetPositive.v COQC theories/QArith/Qfield.v COQC theories/QArith/QOrderedType.v COQC theories/QArith/Qreduction.v COQC theories/QArith/Qminmax.v COQC theories/FSets/FSetFacts.v COQC theories/FSets/FMapFacts.v COQC theories/MSets/MSetFacts.v COQC theories/QArith/Qreals.v COQC plugins/fourier/Fourier_util.v COQC theories/Reals/SplitRmult.v COQC theories/Reals/R_Ifp.v COQC theories/Reals/ROrderedType.v COQC theories/QArith/Qring.v COQC theories/QArith/Qpower.v COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v COQC theories/Numbers/Cyclic/Int31/Cyclic31.v COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v COQC theories/QArith/QArith.v COQC plugins/fourier/Fourier.v COQC theories/MSets/MSetDecide.v COQC theories/FSets/FSetCompat.v COQC theories/FSets/FSetDecide.v COQC plugins/btauto/Reflect.v COQC theories/QArith/Qcanon.v COQC theories/QArith/Qround.v COQC theories/QArith/Qabs.v COQC plugins/micromega/QMicromega.v COQC plugins/micromega/RMicromega.v COQC plugins/micromega/ZMicromega.v COQC plugins/setoid_ring/Ncring_initial.v COQC theories/Reals/Rbasic_fun.v COQC theories/FSets/FSetList.v COQC theories/FSets/FSetAVL.v COQC theories/FSets/FSetWeakList.v COQC theories/MSets/MSetProperties.v COQC theories/FSets/FMaps.v COQC theories/QArith/Qcabs.v COQC theories/FSets/FSetProperties.v COQC plugins/micromega/Lqa.v COQC plugins/micromega/Lra.v COQC theories/Reals/SplitAbsolu.v COQC theories/Reals/R_sqr.v COQC theories/Reals/ArithProp.v COQC theories/Reals/Rminmax.v COQC plugins/btauto/Btauto.v COQC theories/FSets/FMapFullAVL.v COQC plugins/micromega/MExtraction.v COQC plugins/micromega/Lia.v COQC theories/Reals/Rfunctions.v COQC plugins/micromega/Psatz.v COQC theories/MSets/MSetToFiniteSet.v COQC theories/MSets/MSetEqProperties.v COQC theories/Numbers/Cyclic/Int31/Ring31.v COQC theories/MSets/MSets.v COQC theories/Reals/Rlimit.v COQC theories/Reals/RList.v COQC theories/Reals/Rseries.v COQC theories/FSets/FSetToFiniteSet.v COQC theories/FSets/FSetEqProperties.v COQC plugins/setoid_ring/Ncring_tac.v COQC theories/Reals/Rderiv.v COQC theories/Reals/SeqProp.v COQC theories/FSets/FSets.v COQC theories/Reals/Ranalysis1.v COQC theories/Reals/Rcomplete.v COQC theories/Reals/Ranalysis2.v COQC theories/Reals/Rtopology.v COQC theories/Reals/PartSum.v COQC plugins/setoid_ring/Cring.v COQC theories/Reals/AltSeries.v COQC theories/Reals/Binomial.v COQC theories/Reals/Cauchy_prod.v COQC theories/Reals/Alembert.v COQC theories/Reals/Rsigma.v COQC theories/Reals/Ranalysis3.v COQC theories/Reals/MVT.v COQC plugins/setoid_ring/Integral_domain.v COQC theories/Reals/Rprod.v COQC plugins/setoid_ring/Rings_Q.v COQC plugins/setoid_ring/Rings_Z.v COQC theories/Reals/SeqSeries.v COQC theories/Reals/Rsqrt_def.v COQC theories/Reals/PSeries_reg.v COQC theories/Reals/Rtrigo_fun.v COQC theories/Reals/Rtrigo_def.v COQC theories/Reals/R_sqrt.v COQC theories/Reals/Rtrigo_alt.v COQC theories/Reals/Cos_rel.v COQC theories/Reals/Sqrt_reg.v COQC theories/Reals/Cos_plus.v COQC theories/Reals/Rtrigo1.v COQC theories/Reals/Rtrigo_reg.v COQC theories/Reals/Rtrigo_calc.v COQC theories/Reals/Rgeom.v COQC theories/Reals/Exp_prop.v COQC theories/Reals/Ranalysis4.v COQC theories/Reals/Rpower.v COQC theories/Reals/Ranalysis_reg.v COQC theories/Reals/RiemannInt_SF.v COQC theories/Reals/RiemannInt.v COQC theories/Reals/Ranalysis5.v COQC theories/Reals/Ratan.v COQC theories/Reals/Machin.v COQC theories/Reals/Rtrigo.v COQC theories/Reals/Ranalysis.v COQC theories/Reals/NewtonInt.v COQC theories/Reals/Integration.v COQC theories/Reals/Reals.v COQC plugins/setoid_ring/Rings_R.v COQC plugins/nsatz/Nsatz.v gmake[1]: Leaving directory '/data/scratch/lang/coq/work/coq-8.7.2'