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