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