printf ' ' | fink --no-use-binary-dist --yes rebuild coqide 2>&1 WARNING: your info file index has not been updated for 15 days. You should run 'fink selfupdate' to get the latest package descriptions. The package 'coqide' will be built without being installed. Reading build dependency for coqide-8.3pl3-1... Reading dependency for coqide-8.3pl3-1... Reading build conflict for coqide-8.3pl3-1... The following package will be rebuilt: coqide Setting runtime build-lock... dpkg-deb -b /sw/build.build/root-fink-buildlock-coqide-8.3pl3-1 /sw/build.build dpkg-deb: building package `fink-buildlock-coqide-8.3pl3-1' in `/sw/build.build/fink-buildlock-coqide-8.3pl3-1_2014.08.09-12.25.16_darwin-x86_64.deb'. Installing build-lock package... /sw/bin/dpkg-lockwait -i /sw/build.build/fink-buildlock-coqide-8.3pl3-1_2014.08.09-12.25.16_darwin-x86_64.deb Selecting previously deselected package fink-buildlock-coqide-8.3pl3-1. (Reading database ... 14805 files and directories currently installed.) Unpacking fink-buildlock-coqide-8.3pl3-1 (from .../fink-buildlock-coqide-8.3pl3-1_2014.08.09-12.25.16_darwin-x86_64.deb) ... Setting up fink-buildlock-coqide-8.3pl3-1 (2014.08.09-12.25.16) ... sudo -u fink-bld [ENV] sh -c /tmp/fink.oLxxK env LANG=C LC_ALL=C /sw/bin/tar --no-same-owner --no-same-permissions -xvf /sw/src/coq-8.3pl3.tar.gz coq-8.3pl3/ coq-8.3pl3/bin/ coq-8.3pl3/COPYRIGHT coq-8.3pl3/README.win coq-8.3pl3/Makefile.build coq-8.3pl3/COMPATIBILITY coq-8.3pl3/INSTALL.ide coq-8.3pl3/Makefile.stage2 coq-8.3pl3/INSTALL coq-8.3pl3/lib/ coq-8.3pl3/lib/tries.ml coq-8.3pl3/lib/gmap.ml coq-8.3pl3/lib/pp.mli coq-8.3pl3/lib/option.mli coq-8.3pl3/lib/envars.ml coq-8.3pl3/lib/doc.tex coq-8.3pl3/lib/rtree.mli coq-8.3pl3/lib/system.ml coq-8.3pl3/lib/hashcons.ml coq-8.3pl3/lib/fmap.ml coq-8.3pl3/lib/bigint.mli coq-8.3pl3/lib/compat.ml4 coq-8.3pl3/lib/profile.ml coq-8.3pl3/lib/segmenttree.ml coq-8.3pl3/lib/gset.mli coq-8.3pl3/lib/explore.ml coq-8.3pl3/lib/edit.mli coq-8.3pl3/lib/hashcons.mli coq-8.3pl3/lib/lib.mllib coq-8.3pl3/lib/fmap.mli coq-8.3pl3/lib/bigint.ml coq-8.3pl3/lib/profile.mli coq-8.3pl3/lib/util.mli coq-8.3pl3/lib/system.mli coq-8.3pl3/lib/pp_control.ml coq-8.3pl3/lib/fset.mli coq-8.3pl3/lib/gset.ml coq-8.3pl3/lib/dnet.mli coq-8.3pl3/lib/heap.mli coq-8.3pl3/lib/pp_control.mli coq-8.3pl3/lib/dyn.mli coq-8.3pl3/lib/envars.mli coq-8.3pl3/lib/rtree.ml coq-8.3pl3/lib/gmapl.mli coq-8.3pl3/lib/edit.ml coq-8.3pl3/lib/tlm.ml coq-8.3pl3/lib/predicate.ml coq-8.3pl3/lib/gmapl.ml coq-8.3pl3/lib/dnet.ml coq-8.3pl3/lib/fset.ml coq-8.3pl3/lib/bstack.mli coq-8.3pl3/lib/explore.mli coq-8.3pl3/lib/pp.ml4 coq-8.3pl3/lib/tries.mli coq-8.3pl3/lib/flags.ml coq-8.3pl3/lib/bstack.ml coq-8.3pl3/lib/util.ml coq-8.3pl3/lib/refutpat.ml4 coq-8.3pl3/lib/dyn.ml coq-8.3pl3/lib/segmenttree.mli coq-8.3pl3/lib/unicodetable.ml coq-8.3pl3/lib/option.ml coq-8.3pl3/lib/predicate.mli coq-8.3pl3/lib/heap.ml coq-8.3pl3/lib/tlm.mli coq-8.3pl3/lib/gmap.mli coq-8.3pl3/lib/flags.mli coq-8.3pl3/INSTALL.macosx coq-8.3pl3/toplevel/ coq-8.3pl3/toplevel/doc.tex coq-8.3pl3/toplevel/whelp.mli coq-8.3pl3/toplevel/class.mli coq-8.3pl3/toplevel/vernacentries.ml coq-8.3pl3/toplevel/classes.mli coq-8.3pl3/toplevel/lemmas.ml coq-8.3pl3/toplevel/cerrors.mli coq-8.3pl3/toplevel/ind_tables.mli coq-8.3pl3/toplevel/search.ml coq-8.3pl3/toplevel/coqinit.mli coq-8.3pl3/toplevel/class.ml coq-8.3pl3/toplevel/metasyntax.mli coq-8.3pl3/toplevel/libtypes.ml coq-8.3pl3/toplevel/vernacexpr.ml coq-8.3pl3/toplevel/vernacinterp.mli coq-8.3pl3/toplevel/auto_ind_decl.mli coq-8.3pl3/toplevel/indschemes.ml coq-8.3pl3/toplevel/libtypes.mli coq-8.3pl3/toplevel/vernac.mli coq-8.3pl3/toplevel/coqtop.mli coq-8.3pl3/toplevel/toplevel.mllib coq-8.3pl3/toplevel/search.mli coq-8.3pl3/toplevel/usage.mli coq-8.3pl3/toplevel/indschemes.mli coq-8.3pl3/toplevel/lemmas.mli coq-8.3pl3/toplevel/auto_ind_decl.ml coq-8.3pl3/toplevel/himsg.mli coq-8.3pl3/toplevel/discharge.ml coq-8.3pl3/toplevel/ind_tables.ml coq-8.3pl3/toplevel/vernacinterp.ml coq-8.3pl3/toplevel/mltop.ml4 coq-8.3pl3/toplevel/autoinstance.ml coq-8.3pl3/toplevel/record.ml coq-8.3pl3/toplevel/discharge.mli coq-8.3pl3/toplevel/himsg.ml coq-8.3pl3/toplevel/vernacentries.mli coq-8.3pl3/toplevel/toplevel.ml coq-8.3pl3/toplevel/whelp.ml4 coq-8.3pl3/toplevel/classes.ml coq-8.3pl3/toplevel/vernac.ml coq-8.3pl3/toplevel/command.ml coq-8.3pl3/toplevel/mltop.mli coq-8.3pl3/toplevel/coqtop.ml coq-8.3pl3/toplevel/coqinit.ml coq-8.3pl3/toplevel/autoinstance.mli coq-8.3pl3/toplevel/toplevel.mli coq-8.3pl3/toplevel/command.mli coq-8.3pl3/toplevel/cerrors.ml coq-8.3pl3/toplevel/usage.ml coq-8.3pl3/toplevel/metasyntax.ml coq-8.3pl3/toplevel/record.mli coq-8.3pl3/tools/ coq-8.3pl3/tools/README.coq-tex coq-8.3pl3/tools/coq.el coq-8.3pl3/tools/coq-db.el coq-8.3pl3/tools/coq_makefile.ml4 coq-8.3pl3/tools/coq_tex.ml4 coq-8.3pl3/tools/coq-sl.sty coq-8.3pl3/tools/README.emacs coq-8.3pl3/tools/coqdep_lexer.mll coq-8.3pl3/tools/coqdep_boot.ml coq-8.3pl3/tools/check-translate coq-8.3pl3/tools/gallina.ml coq-8.3pl3/tools/beautify-archive coq-8.3pl3/tools/coqwc.mll coq-8.3pl3/tools/coqdep_common.ml coq-8.3pl3/tools/coqdep.ml coq-8.3pl3/tools/coq-inferior.el coq-8.3pl3/tools/gallina_lexer.mll coq-8.3pl3/tools/coq-syntax.el coq-8.3pl3/tools/coq-font-lock.el coq-8.3pl3/tools/mkwinapp.ml coq-8.3pl3/tools/coqdoc/ coq-8.3pl3/tools/coqdoc/alpha.mli coq-8.3pl3/tools/coqdoc/tokens.mli coq-8.3pl3/tools/coqdoc/alpha.ml coq-8.3pl3/tools/coqdoc/coqdoc.sty coq-8.3pl3/tools/coqdoc/index.ml coq-8.3pl3/tools/coqdoc/main.ml coq-8.3pl3/tools/coqdoc/coqdoc.css coq-8.3pl3/tools/coqdoc/tokens.ml coq-8.3pl3/tools/coqdoc/cpretty.mll coq-8.3pl3/tools/coqdoc/output.mli coq-8.3pl3/tools/coqdoc/style.css coq-8.3pl3/tools/coqdoc/output.ml coq-8.3pl3/tools/coqdoc/cpretty.mli coq-8.3pl3/tools/coqdoc/cdglobals.ml coq-8.3pl3/tools/coqdoc/index.mli coq-8.3pl3/interp/ coq-8.3pl3/interp/interp.mllib coq-8.3pl3/interp/implicit_quantifiers.mli coq-8.3pl3/interp/doc.tex coq-8.3pl3/interp/ppextend.ml coq-8.3pl3/interp/smartlocate.ml coq-8.3pl3/interp/implicit_quantifiers.ml coq-8.3pl3/interp/constrintern.ml coq-8.3pl3/interp/dumpglob.mli coq-8.3pl3/interp/constrextern.mli coq-8.3pl3/interp/topconstr.ml coq-8.3pl3/interp/syntax_def.ml coq-8.3pl3/interp/reserve.ml coq-8.3pl3/interp/ppextend.mli coq-8.3pl3/interp/modintern.ml coq-8.3pl3/interp/genarg.mli coq-8.3pl3/interp/notation.mli coq-8.3pl3/interp/dumpglob.ml coq-8.3pl3/interp/coqlib.ml coq-8.3pl3/interp/constrextern.ml coq-8.3pl3/interp/coqlib.mli coq-8.3pl3/interp/reserve.mli coq-8.3pl3/interp/modintern.mli coq-8.3pl3/interp/smartlocate.mli coq-8.3pl3/interp/genarg.ml coq-8.3pl3/interp/constrintern.mli coq-8.3pl3/interp/topconstr.mli coq-8.3pl3/interp/syntax_def.mli coq-8.3pl3/interp/notation.ml coq-8.3pl3/scripts/ coq-8.3pl3/scripts/coqmktop.ml coq-8.3pl3/scripts/coqc.ml coq-8.3pl3/Makefile.doc coq-8.3pl3/Makefile coq-8.3pl3/Makefile.common coq-8.3pl3/install.sh coq-8.3pl3/README.doc coq-8.3pl3/kernel/ coq-8.3pl3/kernel/mod_subst.ml coq-8.3pl3/kernel/mod_typing.ml coq-8.3pl3/kernel/byterun/ coq-8.3pl3/kernel/byterun/int64_native.h coq-8.3pl3/kernel/byterun/coq_instruct.h coq-8.3pl3/kernel/byterun/coq_values.c coq-8.3pl3/kernel/byterun/int64_emul.h coq-8.3pl3/kernel/byterun/coq_interp.c coq-8.3pl3/kernel/byterun/coq_values.h coq-8.3pl3/kernel/byterun/coq_fix_code.c coq-8.3pl3/kernel/byterun/coq_gc.h coq-8.3pl3/kernel/byterun/coq_memory.h coq-8.3pl3/kernel/byterun/coq_memory.c coq-8.3pl3/kernel/byterun/coq_interp.h coq-8.3pl3/kernel/byterun/coq_fix_code.h coq-8.3pl3/kernel/byterun/libcoqrun.clib coq-8.3pl3/kernel/sign.ml coq-8.3pl3/kernel/conv_oracle.mli coq-8.3pl3/kernel/pre_env.mli coq-8.3pl3/kernel/declarations.ml coq-8.3pl3/kernel/doc.tex coq-8.3pl3/kernel/environ.ml coq-8.3pl3/kernel/csymtable.ml coq-8.3pl3/kernel/type_errors.ml coq-8.3pl3/kernel/csymtable.mli coq-8.3pl3/kernel/environ.mli coq-8.3pl3/kernel/reduction.mli coq-8.3pl3/kernel/names.ml coq-8.3pl3/kernel/typeops.mli coq-8.3pl3/kernel/entries.mli coq-8.3pl3/kernel/declarations.mli coq-8.3pl3/kernel/term.mli coq-8.3pl3/kernel/modops.ml coq-8.3pl3/kernel/vconv.ml coq-8.3pl3/kernel/vconv.mli coq-8.3pl3/kernel/cemitcodes.ml coq-8.3pl3/kernel/cbytegen.mli coq-8.3pl3/kernel/univ.mli coq-8.3pl3/kernel/esubst.mli coq-8.3pl3/kernel/cbytegen.ml coq-8.3pl3/kernel/inductive.ml coq-8.3pl3/kernel/retroknowledge.ml coq-8.3pl3/kernel/cooking.ml coq-8.3pl3/kernel/pre_env.ml coq-8.3pl3/kernel/cbytecodes.mli coq-8.3pl3/kernel/subtyping.ml coq-8.3pl3/kernel/mod_subst.mli coq-8.3pl3/kernel/vm.ml coq-8.3pl3/kernel/kernel.mllib coq-8.3pl3/kernel/subtyping.mli coq-8.3pl3/kernel/retroknowledge.mli coq-8.3pl3/kernel/cbytecodes.ml coq-8.3pl3/kernel/cemitcodes.mli coq-8.3pl3/kernel/safe_typing.mli coq-8.3pl3/kernel/closure.ml coq-8.3pl3/kernel/mod_typing.mli coq-8.3pl3/kernel/typeops.ml coq-8.3pl3/kernel/make-opcodes coq-8.3pl3/kernel/reduction.ml coq-8.3pl3/kernel/univ.ml coq-8.3pl3/kernel/entries.ml coq-8.3pl3/kernel/cooking.mli coq-8.3pl3/kernel/type_errors.mli coq-8.3pl3/kernel/indtypes.mli coq-8.3pl3/kernel/closure.mli coq-8.3pl3/kernel/term.ml coq-8.3pl3/kernel/modops.mli coq-8.3pl3/kernel/sign.mli coq-8.3pl3/kernel/names.mli coq-8.3pl3/kernel/term_typing.mli coq-8.3pl3/kernel/inductive.mli coq-8.3pl3/kernel/term_typing.ml coq-8.3pl3/kernel/safe_typing.ml coq-8.3pl3/kernel/conv_oracle.ml coq-8.3pl3/kernel/indtypes.ml coq-8.3pl3/kernel/esubst.ml coq-8.3pl3/kernel/vm.mli coq-8.3pl3/states/ coq-8.3pl3/states/MakeInitial.v coq-8.3pl3/plugins/ coq-8.3pl3/plugins/interface/ coq-8.3pl3/plugins/field/ coq-8.3pl3/plugins/field/LegacyField_Tactic.v coq-8.3pl3/plugins/field/LegacyField_Theory.v coq-8.3pl3/plugins/field/field_plugin.mllib coq-8.3pl3/plugins/field/LegacyField.v coq-8.3pl3/plugins/field/field.ml4 coq-8.3pl3/plugins/field/LegacyField_Compl.v coq-8.3pl3/plugins/field/vo.itarget coq-8.3pl3/plugins/dp/ coq-8.3pl3/plugins/dp/Dp.v coq-8.3pl3/plugins/dp/fol.mli coq-8.3pl3/plugins/dp/dp.ml coq-8.3pl3/plugins/dp/dp_plugin.mllib coq-8.3pl3/plugins/dp/tests.v coq-8.3pl3/plugins/dp/dp_zenon.mll coq-8.3pl3/plugins/dp/test2.v coq-8.3pl3/plugins/dp/dp_why.mli coq-8.3pl3/plugins/dp/g_dp.ml4 coq-8.3pl3/plugins/dp/zenon.v coq-8.3pl3/plugins/dp/dp_why.ml coq-8.3pl3/plugins/dp/TODO coq-8.3pl3/plugins/dp/dp_zenon.mli coq-8.3pl3/plugins/dp/vo.itarget coq-8.3pl3/plugins/dp/dp.mli coq-8.3pl3/plugins/pluginsdyn.itarget coq-8.3pl3/plugins/omega/ coq-8.3pl3/plugins/omega/OmegaLemmas.v coq-8.3pl3/plugins/omega/OmegaPlugin.v coq-8.3pl3/plugins/omega/omega_plugin.mllib coq-8.3pl3/plugins/omega/Omega.v coq-8.3pl3/plugins/omega/PreOmega.v coq-8.3pl3/plugins/omega/omega.ml coq-8.3pl3/plugins/omega/g_omega.ml4 coq-8.3pl3/plugins/omega/vo.itarget coq-8.3pl3/plugins/omega/coq_omega.ml coq-8.3pl3/plugins/syntax/ coq-8.3pl3/plugins/syntax/ascii_syntax_plugin.mllib coq-8.3pl3/plugins/syntax/numbers_syntax_plugin.mllib coq-8.3pl3/plugins/syntax/ascii_syntax.ml coq-8.3pl3/plugins/syntax/z_syntax_plugin.mllib coq-8.3pl3/plugins/syntax/nat_syntax_plugin.mllib coq-8.3pl3/plugins/syntax/z_syntax.ml coq-8.3pl3/plugins/syntax/r_syntax_plugin.mllib coq-8.3pl3/plugins/syntax/r_syntax.ml coq-8.3pl3/plugins/syntax/nat_syntax.ml coq-8.3pl3/plugins/syntax/string_syntax_plugin.mllib coq-8.3pl3/plugins/syntax/numbers_syntax.ml coq-8.3pl3/plugins/syntax/string_syntax.ml coq-8.3pl3/plugins/fourier/ coq-8.3pl3/plugins/fourier/Fourier.v coq-8.3pl3/plugins/fourier/fourierR.ml coq-8.3pl3/plugins/fourier/fourier_plugin.mllib coq-8.3pl3/plugins/fourier/g_fourier.ml4 coq-8.3pl3/plugins/fourier/Fourier_util.v coq-8.3pl3/plugins/fourier/vo.itarget coq-8.3pl3/plugins/fourier/fourier.ml coq-8.3pl3/plugins/rtauto/ coq-8.3pl3/plugins/rtauto/proof_search.mli coq-8.3pl3/plugins/rtauto/proof_search.ml coq-8.3pl3/plugins/rtauto/refl_tauto.ml coq-8.3pl3/plugins/rtauto/g_rtauto.ml4 coq-8.3pl3/plugins/rtauto/Bintree.v coq-8.3pl3/plugins/rtauto/rtauto_plugin.mllib coq-8.3pl3/plugins/rtauto/refl_tauto.mli coq-8.3pl3/plugins/rtauto/Rtauto.v coq-8.3pl3/plugins/rtauto/vo.itarget coq-8.3pl3/plugins/firstorder/ coq-8.3pl3/plugins/firstorder/ground.mli coq-8.3pl3/plugins/firstorder/sequent.ml coq-8.3pl3/plugins/firstorder/sequent.mli coq-8.3pl3/plugins/firstorder/g_ground.ml4 coq-8.3pl3/plugins/firstorder/instances.mli coq-8.3pl3/plugins/firstorder/rules.ml coq-8.3pl3/plugins/firstorder/instances.ml coq-8.3pl3/plugins/firstorder/formula.ml coq-8.3pl3/plugins/firstorder/ground_plugin.mllib coq-8.3pl3/plugins/firstorder/rules.mli coq-8.3pl3/plugins/firstorder/unify.ml coq-8.3pl3/plugins/firstorder/formula.mli coq-8.3pl3/plugins/firstorder/ground.ml coq-8.3pl3/plugins/firstorder/unify.mli coq-8.3pl3/plugins/pluginsbyte.itarget coq-8.3pl3/plugins/funind/ coq-8.3pl3/plugins/funind/rawtermops.ml coq-8.3pl3/plugins/funind/indfun_common.mli coq-8.3pl3/plugins/funind/g_indfun.ml4 coq-8.3pl3/plugins/funind/recdef.ml coq-8.3pl3/plugins/funind/functional_principles_types.ml coq-8.3pl3/plugins/funind/rawtermops.mli coq-8.3pl3/plugins/funind/functional_principles_proofs.ml coq-8.3pl3/plugins/funind/indfun_common.ml coq-8.3pl3/plugins/funind/Recdef.v coq-8.3pl3/plugins/funind/merge.ml coq-8.3pl3/plugins/funind/rawterm_to_relation.ml coq-8.3pl3/plugins/funind/indfun.ml coq-8.3pl3/plugins/funind/rawterm_to_relation.mli coq-8.3pl3/plugins/funind/functional_principles_types.mli coq-8.3pl3/plugins/funind/invfun.ml coq-8.3pl3/plugins/funind/vo.itarget coq-8.3pl3/plugins/funind/functional_principles_proofs.mli coq-8.3pl3/plugins/funind/recdef_plugin.mllib coq-8.3pl3/plugins/extraction/ coq-8.3pl3/plugins/extraction/extract_env.ml coq-8.3pl3/plugins/extraction/scheme.mli coq-8.3pl3/plugins/extraction/ExtrOcamlBigIntConv.v coq-8.3pl3/plugins/extraction/ExtrOcamlIntConv.v coq-8.3pl3/plugins/extraction/ocaml.mli coq-8.3pl3/plugins/extraction/ExtrOcamlZBigInt.v coq-8.3pl3/plugins/extraction/extraction_plugin.mllib coq-8.3pl3/plugins/extraction/mlutil.ml coq-8.3pl3/plugins/extraction/miniml.mli coq-8.3pl3/plugins/extraction/haskell.mli coq-8.3pl3/plugins/extraction/extraction.ml coq-8.3pl3/plugins/extraction/ExtrOcamlString.v coq-8.3pl3/plugins/extraction/ocaml.ml coq-8.3pl3/plugins/extraction/mlutil.mli coq-8.3pl3/plugins/extraction/big.ml coq-8.3pl3/plugins/extraction/ExtrOcamlNatBigInt.v coq-8.3pl3/plugins/extraction/table.ml coq-8.3pl3/plugins/extraction/extract_env.mli coq-8.3pl3/plugins/extraction/ExtrOcamlBasic.v coq-8.3pl3/plugins/extraction/modutil.ml coq-8.3pl3/plugins/extraction/modutil.mli coq-8.3pl3/plugins/extraction/g_extraction.ml4 coq-8.3pl3/plugins/extraction/scheme.ml coq-8.3pl3/plugins/extraction/common.ml coq-8.3pl3/plugins/extraction/CHANGES coq-8.3pl3/plugins/extraction/vo.itarget coq-8.3pl3/plugins/extraction/haskell.ml coq-8.3pl3/plugins/extraction/table.mli coq-8.3pl3/plugins/extraction/extraction.mli coq-8.3pl3/plugins/extraction/README coq-8.3pl3/plugins/extraction/ExtrOcamlNatInt.v coq-8.3pl3/plugins/extraction/common.mli coq-8.3pl3/plugins/extraction/ExtrOcamlZInt.v coq-8.3pl3/plugins/subtac/ coq-8.3pl3/plugins/subtac/eterm.ml coq-8.3pl3/plugins/subtac/subtac_obligations.mli coq-8.3pl3/plugins/subtac/subtac_utils.mli coq-8.3pl3/plugins/subtac/subtac_errors.mli coq-8.3pl3/plugins/subtac/eterm.mli coq-8.3pl3/plugins/subtac/subtac_classes.ml coq-8.3pl3/plugins/subtac/subtac.ml coq-8.3pl3/plugins/subtac/subtac_utils.ml coq-8.3pl3/plugins/subtac/subtac_coercion.mli coq-8.3pl3/plugins/subtac/test/ coq-8.3pl3/plugins/subtac/test/ListsTest.v coq-8.3pl3/plugins/subtac/test/Test1.v coq-8.3pl3/plugins/subtac/test/euclid.v coq-8.3pl3/plugins/subtac/test/ListDep.v coq-8.3pl3/plugins/subtac/test/measure.v coq-8.3pl3/plugins/subtac/test/take.v coq-8.3pl3/plugins/subtac/test/id.v coq-8.3pl3/plugins/subtac/test/Mutind.v coq-8.3pl3/plugins/subtac/test/rec.v coq-8.3pl3/plugins/subtac/test/wf.v coq-8.3pl3/plugins/subtac/subtac_cases.mli coq-8.3pl3/plugins/subtac/subtac_command.ml coq-8.3pl3/plugins/subtac/subtac_classes.mli coq-8.3pl3/plugins/subtac/subtac_pretyping_F.ml coq-8.3pl3/plugins/subtac/subtac_obligations.ml coq-8.3pl3/plugins/subtac/subtac_pretyping.mli coq-8.3pl3/plugins/subtac/subtac_cases.ml coq-8.3pl3/plugins/subtac/subtac.mli coq-8.3pl3/plugins/subtac/subtac_command.mli coq-8.3pl3/plugins/subtac/g_subtac.ml4 coq-8.3pl3/plugins/subtac/subtac_errors.ml coq-8.3pl3/plugins/subtac/subtac_pretyping.ml coq-8.3pl3/plugins/subtac/subtac_plugin.mllib coq-8.3pl3/plugins/subtac/subtac_coercion.ml coq-8.3pl3/plugins/quote/ coq-8.3pl3/plugins/quote/Quote.v coq-8.3pl3/plugins/quote/g_quote.ml4 coq-8.3pl3/plugins/quote/quote_plugin.mllib coq-8.3pl3/plugins/quote/quote.ml coq-8.3pl3/plugins/quote/vo.itarget coq-8.3pl3/plugins/xml/ coq-8.3pl3/plugins/xml/xmlcommand.ml coq-8.3pl3/plugins/xml/COPYRIGHT coq-8.3pl3/plugins/xml/doubleTypeInference.mli coq-8.3pl3/plugins/xml/unshare.ml coq-8.3pl3/plugins/xml/proof2aproof.ml coq-8.3pl3/plugins/xml/xml.mli coq-8.3pl3/plugins/xml/proofTree2Xml.ml4 coq-8.3pl3/plugins/xml/xmlentries.ml4 coq-8.3pl3/plugins/xml/theoryobject.dtd coq-8.3pl3/plugins/xml/cic2acic.ml coq-8.3pl3/plugins/xml/unshare.mli coq-8.3pl3/plugins/xml/cic2Xml.ml coq-8.3pl3/plugins/xml/xml_plugin.mllib coq-8.3pl3/plugins/xml/xml.ml4 coq-8.3pl3/plugins/xml/doubleTypeInference.ml coq-8.3pl3/plugins/xml/xmlcommand.mli coq-8.3pl3/plugins/xml/dumptree.ml4 coq-8.3pl3/plugins/xml/README coq-8.3pl3/plugins/xml/acic.ml coq-8.3pl3/plugins/xml/acic2Xml.ml4 coq-8.3pl3/plugins/xml/cic.dtd coq-8.3pl3/plugins/romega/ coq-8.3pl3/plugins/romega/g_romega.ml4 coq-8.3pl3/plugins/romega/ROmega.v coq-8.3pl3/plugins/romega/const_omega.mli coq-8.3pl3/plugins/romega/romega_plugin.mllib coq-8.3pl3/plugins/romega/ReflOmegaCore.v coq-8.3pl3/plugins/romega/const_omega.ml coq-8.3pl3/plugins/romega/vo.itarget coq-8.3pl3/plugins/romega/refl_omega.ml coq-8.3pl3/plugins/romega/README coq-8.3pl3/plugins/nsatz/ coq-8.3pl3/plugins/nsatz/ideal.ml coq-8.3pl3/plugins/nsatz/nsatz.ml4 coq-8.3pl3/plugins/nsatz/utile.ml coq-8.3pl3/plugins/nsatz/polynom.ml coq-8.3pl3/plugins/nsatz/nsatz_plugin.mllib coq-8.3pl3/plugins/nsatz/polynom.mli coq-8.3pl3/plugins/nsatz/Nsatz.v coq-8.3pl3/plugins/nsatz/vo.itarget coq-8.3pl3/plugins/nsatz/utile.mli coq-8.3pl3/plugins/groebner/ coq-8.3pl3/plugins/setoid_ring/ coq-8.3pl3/plugins/setoid_ring/ArithRing.v coq-8.3pl3/plugins/setoid_ring/Ring_base.v coq-8.3pl3/plugins/setoid_ring/Field_theory.v coq-8.3pl3/plugins/setoid_ring/newring.ml4 coq-8.3pl3/plugins/setoid_ring/RealField.v coq-8.3pl3/plugins/setoid_ring/Ring_tac.v coq-8.3pl3/plugins/setoid_ring/InitialRing.v coq-8.3pl3/plugins/setoid_ring/Ring.v coq-8.3pl3/plugins/setoid_ring/Ring_equiv.v coq-8.3pl3/plugins/setoid_ring/Ring_theory.v coq-8.3pl3/plugins/setoid_ring/ZArithRing.v coq-8.3pl3/plugins/setoid_ring/Field.v coq-8.3pl3/plugins/setoid_ring/Field_tac.v coq-8.3pl3/plugins/setoid_ring/NArithRing.v coq-8.3pl3/plugins/setoid_ring/vo.itarget coq-8.3pl3/plugins/setoid_ring/Ring_polynom.v coq-8.3pl3/plugins/setoid_ring/newring_plugin.mllib coq-8.3pl3/plugins/setoid_ring/BinList.v coq-8.3pl3/plugins/cc/ coq-8.3pl3/plugins/cc/ccalgo.mli coq-8.3pl3/plugins/cc/ccproof.mli coq-8.3pl3/plugins/cc/cctac.mli coq-8.3pl3/plugins/cc/cctac.ml coq-8.3pl3/plugins/cc/ccalgo.ml coq-8.3pl3/plugins/cc/g_congruence.ml4 coq-8.3pl3/plugins/cc/cc_plugin.mllib coq-8.3pl3/plugins/cc/ccproof.ml coq-8.3pl3/plugins/cc/README coq-8.3pl3/plugins/pluginsvo.itarget coq-8.3pl3/plugins/ring/ coq-8.3pl3/plugins/ring/LegacyRing_theory.v coq-8.3pl3/plugins/ring/ring_plugin.mllib coq-8.3pl3/plugins/ring/ring.ml coq-8.3pl3/plugins/ring/g_ring.ml4 coq-8.3pl3/plugins/ring/Setoid_ring_normalize.v coq-8.3pl3/plugins/ring/Ring_normalize.v coq-8.3pl3/plugins/ring/LegacyRing.v coq-8.3pl3/plugins/ring/Ring_abstract.v coq-8.3pl3/plugins/ring/LegacyZArithRing.v coq-8.3pl3/plugins/ring/Setoid_ring.v coq-8.3pl3/plugins/ring/LegacyNArithRing.v coq-8.3pl3/plugins/ring/Setoid_ring_theory.v coq-8.3pl3/plugins/ring/LegacyArithRing.v coq-8.3pl3/plugins/ring/vo.itarget coq-8.3pl3/plugins/micromega/ coq-8.3pl3/plugins/micromega/RMicromega.v coq-8.3pl3/plugins/micromega/mfourier.ml coq-8.3pl3/plugins/micromega/MExtraction.v coq-8.3pl3/plugins/micromega/Refl.v coq-8.3pl3/plugins/micromega/LICENSE.sos coq-8.3pl3/plugins/micromega/coq_micromega.ml coq-8.3pl3/plugins/micromega/csdpcert.ml coq-8.3pl3/plugins/micromega/Psatz.v coq-8.3pl3/plugins/micromega/sos_types.ml coq-8.3pl3/plugins/micromega/micromega.mli coq-8.3pl3/plugins/micromega/g_micromega.ml4 coq-8.3pl3/plugins/micromega/mutils.ml coq-8.3pl3/plugins/micromega/VarMap.v coq-8.3pl3/plugins/micromega/persistent_cache.ml coq-8.3pl3/plugins/micromega/sos_lib.ml coq-8.3pl3/plugins/micromega/Env.v coq-8.3pl3/plugins/micromega/micromega.ml coq-8.3pl3/plugins/micromega/ZCoeff.v coq-8.3pl3/plugins/micromega/certificate.ml coq-8.3pl3/plugins/micromega/RingMicromega.v coq-8.3pl3/plugins/micromega/QMicromega.v coq-8.3pl3/plugins/micromega/OrderedRing.v coq-8.3pl3/plugins/micromega/Tauto.v coq-8.3pl3/plugins/micromega/sos.ml coq-8.3pl3/plugins/micromega/CheckerMaker.v coq-8.3pl3/plugins/micromega/micromega_plugin.mllib coq-8.3pl3/plugins/micromega/EnvRing.v coq-8.3pl3/plugins/micromega/vo.itarget coq-8.3pl3/plugins/micromega/sos.mli coq-8.3pl3/plugins/micromega/ZMicromega.v coq-8.3pl3/plugins/pluginsopt.itarget coq-8.3pl3/plugins/plugins.itarget coq-8.3pl3/test-suite/ coq-8.3pl3/test-suite/interactive/ coq-8.3pl3/test-suite/interactive/Evar.v coq-8.3pl3/test-suite/interactive/Back.v coq-8.3pl3/test-suite/bugs/ coq-8.3pl3/test-suite/bugs/opened/ coq-8.3pl3/test-suite/bugs/opened/shouldnotsucceed/ coq-8.3pl3/test-suite/bugs/opened/1773.v coq-8.3pl3/test-suite/bugs/opened/shouldnotfail/ coq-8.3pl3/test-suite/bugs/opened/shouldnotfail/1501.v coq-8.3pl3/test-suite/bugs/opened/shouldnotfail/1811.v coq-8.3pl3/test-suite/bugs/opened/shouldnotfail/743.v coq-8.3pl3/test-suite/bugs/opened/shouldnotfail/1596.v coq-8.3pl3/test-suite/bugs/opened/shouldnotfail/1671.v coq-8.3pl3/test-suite/bugs/opened/shouldnotfail/1338.v-disabled coq-8.3pl3/test-suite/bugs/closed/ coq-8.3pl3/test-suite/bugs/closed/2319.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/ coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2108.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1844.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2095.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1302.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1944.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1614.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1568.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2139.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2027.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2193.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2127.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1935.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2117.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1411.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1791.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2464.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1507.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2083.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1977.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1907.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1519.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/846.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1951.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1604.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2281.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1041.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1939.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1704.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1711.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1773.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1774.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1981.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/38.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1680.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1779.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2017.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/931.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2021.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1618.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2295.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1414.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2467.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2608.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2089.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2137.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2303.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2136.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2001.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1776.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1100.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1416.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/808_2411.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2360.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1477.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1784.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1419.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2299.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2145.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1901.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1738.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1582.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1634.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/335.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1865.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2135.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1243.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2262.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1775.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2231.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1754.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2375.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2300.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/545.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/348.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2353.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2388.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1918.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1446.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2255.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2123.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1643.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1740.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1931.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1683.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1448.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1322.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1891.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2347.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1576.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2350.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1718.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1425.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1696.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1963.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1925.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1900.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1905.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/1483.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/121.v coq-8.3pl3/test-suite/bugs/closed/shouldsucceed/2244.v coq-8.3pl3/test-suite/bugs/closed/shouldfail/ coq-8.3pl3/test-suite/bugs/closed/shouldfail/1703.v coq-8.3pl3/test-suite/bugs/closed/shouldfail/1898.v coq-8.3pl3/test-suite/bugs/closed/shouldfail/1915.v coq-8.3pl3/test-suite/bugs/closed/shouldfail/2251.v coq-8.3pl3/test-suite/bugs/closed/shouldfail/2006.v coq-8.3pl3/test-suite/bugs/closed/1780.v coq-8.3pl3/test-suite/bugs/closed/1519.v coq-8.3pl3/test-suite/bugs/closed/1787.v coq-8.3pl3/test-suite/bench/ coq-8.3pl3/test-suite/bench/lists_100.v coq-8.3pl3/test-suite/bench/lists-100.v coq-8.3pl3/test-suite/Makefile coq-8.3pl3/test-suite/check coq-8.3pl3/test-suite/kernel/ coq-8.3pl3/test-suite/kernel/inds.mv coq-8.3pl3/test-suite/success/ coq-8.3pl3/test-suite/success/OmegaPre.v coq-8.3pl3/test-suite/success/Fourier.v coq-8.3pl3/test-suite/success/CasesDep.v coq-8.3pl3/test-suite/success/TestRefine.v coq-8.3pl3/test-suite/success/Mod_ltac.v coq-8.3pl3/test-suite/success/rewrite.v coq-8.3pl3/test-suite/success/induct.v coq-8.3pl3/test-suite/success/ROmegaPre.v coq-8.3pl3/test-suite/success/dependentind.v coq-8.3pl3/test-suite/success/unification.v coq-8.3pl3/test-suite/success/mutual_ind.v coq-8.3pl3/test-suite/success/CaseAlias.v coq-8.3pl3/test-suite/success/Case11.v coq-8.3pl3/test-suite/success/DHyp.v coq-8.3pl3/test-suite/success/rewrite_iterated.v coq-8.3pl3/test-suite/success/eauto.v coq-8.3pl3/test-suite/success/Section.v coq-8.3pl3/test-suite/success/AdvancedCanonicalStructure.v coq-8.3pl3/test-suite/success/Simplify_eq.v coq-8.3pl3/test-suite/success/Case10.v coq-8.3pl3/test-suite/success/Rename.v coq-8.3pl3/test-suite/success/ROmega.v coq-8.3pl3/test-suite/success/Import.v coq-8.3pl3/test-suite/success/setoid_test_function_space.v coq-8.3pl3/test-suite/success/Funind.v coq-8.3pl3/test-suite/success/unfold.v coq-8.3pl3/test-suite/success/Inductive.v coq-8.3pl3/test-suite/success/rewrite_in.v coq-8.3pl3/test-suite/success/evars.v coq-8.3pl3/test-suite/success/Case2.v coq-8.3pl3/test-suite/success/Case9.v coq-8.3pl3/test-suite/success/ROmega0.v coq-8.3pl3/test-suite/success/Cases-bug1834.v coq-8.3pl3/test-suite/success/if.v coq-8.3pl3/test-suite/success/Fixpoint.v coq-8.3pl3/test-suite/success/cc.v coq-8.3pl3/test-suite/success/Scopes.v coq-8.3pl3/test-suite/success/autorewritein.v coq-8.3pl3/test-suite/success/Mod_params.v coq-8.3pl3/test-suite/success/Try.v coq-8.3pl3/test-suite/success/clear.v coq-8.3pl3/test-suite/success/LetPat.v coq-8.3pl3/test-suite/success/ROmega2.v coq-8.3pl3/test-suite/success/Case15.v coq-8.3pl3/test-suite/success/Omega.v coq-8.3pl3/test-suite/success/import_lib.v coq-8.3pl3/test-suite/success/Check.v coq-8.3pl3/test-suite/success/setoid_ring_module.v coq-8.3pl3/test-suite/success/instantiate.v coq-8.3pl3/test-suite/success/options.v coq-8.3pl3/test-suite/success/Discriminate.v coq-8.3pl3/test-suite/success/specialize.v coq-8.3pl3/test-suite/success/RecTutorial.v coq-8.3pl3/test-suite/success/import_mod.v coq-8.3pl3/test-suite/success/refine.v coq-8.3pl3/test-suite/success/Decompose.v coq-8.3pl3/test-suite/success/setoid_test.v coq-8.3pl3/test-suite/success/ImplicitArguments.v coq-8.3pl3/test-suite/success/Case13.v coq-8.3pl3/test-suite/success/pattern.v coq-8.3pl3/test-suite/success/unicode_utf8.v coq-8.3pl3/test-suite/success/guard.v coq-8.3pl3/test-suite/success/Conjecture.v coq-8.3pl3/test-suite/success/eqdecide.v coq-8.3pl3/test-suite/success/implicit.v coq-8.3pl3/test-suite/success/Require.v coq-8.3pl3/test-suite/success/Reordering.v coq-8.3pl3/test-suite/success/parsing.v coq-8.3pl3/test-suite/success/LegacyField.v coq-8.3pl3/test-suite/success/Case14.v coq-8.3pl3/test-suite/success/replace.v coq-8.3pl3/test-suite/success/Case18.v coq-8.3pl3/test-suite/success/Case5.v coq-8.3pl3/test-suite/success/Notations.v coq-8.3pl3/test-suite/success/Omega0.v coq-8.3pl3/test-suite/success/Reset.v coq-8.3pl3/test-suite/success/coercions.v coq-8.3pl3/test-suite/success/Print.v coq-8.3pl3/test-suite/success/Remark.v coq-8.3pl3/test-suite/success/MatchFail.v coq-8.3pl3/test-suite/success/AdvancedTypeClasses.v coq-8.3pl3/test-suite/success/hyps_inclusion.v coq-8.3pl3/test-suite/success/Typeclasses.v coq-8.3pl3/test-suite/success/setoid_test2.v coq-8.3pl3/test-suite/success/polymorphism.v coq-8.3pl3/test-suite/success/univers.v coq-8.3pl3/test-suite/success/Abstract.v coq-8.3pl3/test-suite/success/Hints.v coq-8.3pl3/test-suite/success/Field.v coq-8.3pl3/test-suite/success/Case7.v coq-8.3pl3/test-suite/success/ProgramWf.v coq-8.3pl3/test-suite/success/Case6.v coq-8.3pl3/test-suite/success/set.v coq-8.3pl3/test-suite/success/Cases.v coq-8.3pl3/test-suite/success/CanonicalStructure.v coq-8.3pl3/test-suite/success/Tauto.v coq-8.3pl3/test-suite/success/ltac.v coq-8.3pl3/test-suite/success/autointros.v coq-8.3pl3/test-suite/success/Mod_type.v coq-8.3pl3/test-suite/success/Mod_strengthen.v coq-8.3pl3/test-suite/success/Nsatz.v coq-8.3pl3/test-suite/success/LetIn.v coq-8.3pl3/test-suite/success/params_ind.v coq-8.3pl3/test-suite/success/Reg.v coq-8.3pl3/test-suite/success/Projection.v coq-8.3pl3/test-suite/success/Case16.v coq-8.3pl3/test-suite/success/coqbugs0181.v coq-8.3pl3/test-suite/success/destruct.v coq-8.3pl3/test-suite/success/extraction.v coq-8.3pl3/test-suite/success/change.v coq-8.3pl3/test-suite/success/PPFix.v coq-8.3pl3/test-suite/success/inds_type_sec.v coq-8.3pl3/test-suite/success/DiscrR.v coq-8.3pl3/test-suite/success/Injection.v coq-8.3pl3/test-suite/success/conv_pbs.v coq-8.3pl3/test-suite/success/Omega2.v coq-8.3pl3/test-suite/success/Case8.v coq-8.3pl3/test-suite/success/Case17.v coq-8.3pl3/test-suite/success/Case19.v coq-8.3pl3/test-suite/success/ImplicitTactic.v coq-8.3pl3/test-suite/success/Inversion.v coq-8.3pl3/test-suite/success/fix.v coq-8.3pl3/test-suite/success/Generalize.v coq-8.3pl3/test-suite/success/NatRing.v coq-8.3pl3/test-suite/success/simpl.v coq-8.3pl3/test-suite/success/Case3.v coq-8.3pl3/test-suite/success/Generalization.v coq-8.3pl3/test-suite/success/decl_mode.v coq-8.3pl3/test-suite/success/Case12.v coq-8.3pl3/test-suite/success/Case1.v coq-8.3pl3/test-suite/success/Record.v coq-8.3pl3/test-suite/success/intros.v coq-8.3pl3/test-suite/success/apply.v coq-8.3pl3/test-suite/prerequisite/ coq-8.3pl3/test-suite/prerequisite/make_local.v coq-8.3pl3/test-suite/prerequisite/make_notation.v coq-8.3pl3/test-suite/csdp.cache coq-8.3pl3/test-suite/complexity/ coq-8.3pl3/test-suite/complexity/ring.v coq-8.3pl3/test-suite/complexity/pretyping.v coq-8.3pl3/test-suite/complexity/unification.v coq-8.3pl3/test-suite/complexity/setoid_rewrite.v coq-8.3pl3/test-suite/complexity/ring2.v coq-8.3pl3/test-suite/complexity/lettuple.v coq-8.3pl3/test-suite/complexity/autodecomp.v coq-8.3pl3/test-suite/complexity/injection.v coq-8.3pl3/test-suite/modules/ coq-8.3pl3/test-suite/modules/PO.v coq-8.3pl3/test-suite/modules/obj.v coq-8.3pl3/test-suite/modules/grammar.v coq-8.3pl3/test-suite/modules/subtyping.v coq-8.3pl3/test-suite/modules/Tescik.v coq-8.3pl3/test-suite/modules/objects2.v coq-8.3pl3/test-suite/modules/plik.v coq-8.3pl3/test-suite/modules/mod_decl.v coq-8.3pl3/test-suite/modules/objects.v coq-8.3pl3/test-suite/modules/ind.v coq-8.3pl3/test-suite/modules/fun_objects.v coq-8.3pl3/test-suite/modules/pseudo_circular_with.v coq-8.3pl3/test-suite/modules/Przyklad.v coq-8.3pl3/test-suite/modules/sub_objects.v coq-8.3pl3/test-suite/modules/modeq.v coq-8.3pl3/test-suite/modules/Demo.v coq-8.3pl3/test-suite/modules/pliczek.v coq-8.3pl3/test-suite/modules/sig.v coq-8.3pl3/test-suite/modules/nested_mod_types.v coq-8.3pl3/test-suite/modules/injection_discriminate_inversion.v coq-8.3pl3/test-suite/modules/resolver.v coq-8.3pl3/test-suite/modules/Nat.v coq-8.3pl3/test-suite/modules/modul.v coq-8.3pl3/test-suite/failure/ coq-8.3pl3/test-suite/failure/evar1.v coq-8.3pl3/test-suite/failure/rewrite_in_hyp.v coq-8.3pl3/test-suite/failure/inductive1.v coq-8.3pl3/test-suite/failure/evarlemma.v coq-8.3pl3/test-suite/failure/Uminus.v coq-8.3pl3/test-suite/failure/clash_cons.v coq-8.3pl3/test-suite/failure/ClearBody.v coq-8.3pl3/test-suite/failure/universes2.v coq-8.3pl3/test-suite/failure/universes-buraliforti-redef.v coq-8.3pl3/test-suite/failure/Case11.v coq-8.3pl3/test-suite/failure/evarclear1.v coq-8.3pl3/test-suite/failure/circular_subtyping2.v coq-8.3pl3/test-suite/failure/universes-sections1.v coq-8.3pl3/test-suite/failure/positivity.v coq-8.3pl3/test-suite/failure/cases.v coq-8.3pl3/test-suite/failure/Case4.v coq-8.3pl3/test-suite/failure/Case10.v coq-8.3pl3/test-suite/failure/inductive2.v coq-8.3pl3/test-suite/failure/fixpoint3.v coq-8.3pl3/test-suite/failure/Sections.v coq-8.3pl3/test-suite/failure/clashes.v coq-8.3pl3/test-suite/failure/Case2.v coq-8.3pl3/test-suite/failure/Case9.v coq-8.3pl3/test-suite/failure/subtyping.v coq-8.3pl3/test-suite/failure/autorewritein.v coq-8.3pl3/test-suite/failure/evarclear2.v coq-8.3pl3/test-suite/failure/Case15.v coq-8.3pl3/test-suite/failure/fixpoint4.v coq-8.3pl3/test-suite/failure/coqbugs0266.v coq-8.3pl3/test-suite/failure/Case13.v coq-8.3pl3/test-suite/failure/pattern.v coq-8.3pl3/test-suite/failure/universes.v coq-8.3pl3/test-suite/failure/proofirrelevance.v coq-8.3pl3/test-suite/failure/guard.v coq-8.3pl3/test-suite/failure/circular_subtyping1.v coq-8.3pl3/test-suite/failure/Reordering.v coq-8.3pl3/test-suite/failure/ltac1.v coq-8.3pl3/test-suite/failure/Case14.v coq-8.3pl3/test-suite/failure/inductive3.v coq-8.3pl3/test-suite/failure/Case5.v coq-8.3pl3/test-suite/failure/Notations.v coq-8.3pl3/test-suite/failure/universes3.v coq-8.3pl3/test-suite/failure/univ_include.v coq-8.3pl3/test-suite/failure/check.v coq-8.3pl3/test-suite/failure/fixpoint1.v coq-8.3pl3/test-suite/failure/prop-set-proof-irrelevance.v coq-8.3pl3/test-suite/failure/Case7.v coq-8.3pl3/test-suite/failure/fixpoint2.v coq-8.3pl3/test-suite/failure/search.v coq-8.3pl3/test-suite/failure/Case6.v coq-8.3pl3/test-suite/failure/universes-buraliforti.v coq-8.3pl3/test-suite/failure/Tauto.v coq-8.3pl3/test-suite/failure/subtyping2.v coq-8.3pl3/test-suite/failure/universes-sections2.v coq-8.3pl3/test-suite/failure/ImportedCoercion.v coq-8.3pl3/test-suite/failure/Case16.v coq-8.3pl3/test-suite/failure/rewrite_in_hyp2.v coq-8.3pl3/test-suite/failure/Case8.v coq-8.3pl3/test-suite/failure/ltac2.v coq-8.3pl3/test-suite/failure/ltac4.v coq-8.3pl3/test-suite/failure/Case3.v coq-8.3pl3/test-suite/failure/Case12.v coq-8.3pl3/test-suite/failure/Case1.v coq-8.3pl3/test-suite/failure/rewrite_in_goal.v coq-8.3pl3/test-suite/failure/redef.v coq-8.3pl3/test-suite/failure/illtype1.v coq-8.3pl3/test-suite/typeclasses/ coq-8.3pl3/test-suite/typeclasses/NewSetoid.v coq-8.3pl3/test-suite/typeclasses/clrewrite.v coq-8.3pl3/test-suite/typeclasses/unification_delta.v coq-8.3pl3/test-suite/output/ coq-8.3pl3/test-suite/output/RealSyntax.out coq-8.3pl3/test-suite/output/Implicit.out coq-8.3pl3/test-suite/output/TranspModtype.v coq-8.3pl3/test-suite/output/PrintAssumptions.v coq-8.3pl3/test-suite/output/reduction.out coq-8.3pl3/test-suite/output/ArgumentsScope.v coq-8.3pl3/test-suite/output/Match_subterm.v coq-8.3pl3/test-suite/output/simpl.out coq-8.3pl3/test-suite/output/NumbersSyntax.out coq-8.3pl3/test-suite/output/Tactics.v coq-8.3pl3/test-suite/output/ZSyntax.v coq-8.3pl3/test-suite/output/TranspModtype.out coq-8.3pl3/test-suite/output/Naming.out coq-8.3pl3/test-suite/output/Existentials.v coq-8.3pl3/test-suite/output/Naming.v coq-8.3pl3/test-suite/output/Notations2.out coq-8.3pl3/test-suite/output/Extraction_matchs_2413.v coq-8.3pl3/test-suite/output/Fixpoint.v coq-8.3pl3/test-suite/output/ZSyntax.out coq-8.3pl3/test-suite/output/SearchRewrite.out coq-8.3pl3/test-suite/output/Sum.v coq-8.3pl3/test-suite/output/Search.out coq-8.3pl3/test-suite/output/Quote.v coq-8.3pl3/test-suite/output/SearchPattern.out coq-8.3pl3/test-suite/output/Notations.out coq-8.3pl3/test-suite/output/Search.v coq-8.3pl3/test-suite/output/Nametab.out coq-8.3pl3/test-suite/output/Intuition.out coq-8.3pl3/test-suite/output/set.out coq-8.3pl3/test-suite/output/Tactics.out coq-8.3pl3/test-suite/output/Nametab.v coq-8.3pl3/test-suite/output/NumbersSyntax.v coq-8.3pl3/test-suite/output/RealSyntax.v coq-8.3pl3/test-suite/output/SearchRewrite.v coq-8.3pl3/test-suite/output/Notations.v coq-8.3pl3/test-suite/output/PrintAssumptions.out coq-8.3pl3/test-suite/output/Sum.out coq-8.3pl3/test-suite/output/Coercions.v coq-8.3pl3/test-suite/output/reduction.v coq-8.3pl3/test-suite/output/Fixpoint.out coq-8.3pl3/test-suite/output/Existentials.out coq-8.3pl3/test-suite/output/ArgumentsScope.out coq-8.3pl3/test-suite/output/Match_subterm.out coq-8.3pl3/test-suite/output/InitSyntax.out coq-8.3pl3/test-suite/output/Implicit.v coq-8.3pl3/test-suite/output/set.v coq-8.3pl3/test-suite/output/Cases.v coq-8.3pl3/test-suite/output/Coercions.out coq-8.3pl3/test-suite/output/Cases.out coq-8.3pl3/test-suite/output/Intuition.v coq-8.3pl3/test-suite/output/Quote.out coq-8.3pl3/test-suite/output/InitSyntax.v coq-8.3pl3/test-suite/output/Notations2.v coq-8.3pl3/test-suite/output/simpl.v coq-8.3pl3/test-suite/output/Extraction_matchs_2413.out coq-8.3pl3/test-suite/output/SearchPattern.v coq-8.3pl3/test-suite/misc/ coq-8.3pl3/test-suite/misc/deps/ coq-8.3pl3/test-suite/misc/deps/lib/ coq-8.3pl3/test-suite/misc/deps/lib/foo.v coq-8.3pl3/test-suite/misc/deps/client/ coq-8.3pl3/test-suite/misc/deps/client/bar.v coq-8.3pl3/test-suite/misc/deps/client/foo.v coq-8.3pl3/test-suite/misc/deps/deps.out coq-8.3pl3/test-suite/misc/berardi_test.v coq-8.3pl3/test-suite/ide/ coq-8.3pl3/test-suite/ide/undo.v coq-8.3pl3/test-suite/micromega/ coq-8.3pl3/test-suite/micromega/square.v coq-8.3pl3/test-suite/micromega/heap3_vcgen_25.v coq-8.3pl3/test-suite/micromega/bertot.v coq-8.3pl3/test-suite/micromega/qexample.v coq-8.3pl3/test-suite/micromega/example.v coq-8.3pl3/test-suite/micromega/csdp.cache coq-8.3pl3/test-suite/micromega/zomicron.v coq-8.3pl3/test-suite/micromega/rexample.v coq-8.3pl3/test-suite/coqdoc/ coq-8.3pl3/test-suite/coqdoc/links.v coq-8.3pl3/test-suite/ideal-features/ coq-8.3pl3/test-suite/ideal-features/Case4.v coq-8.3pl3/test-suite/ideal-features/implicit_binders.v coq-8.3pl3/test-suite/ideal-features/Case9.v coq-8.3pl3/test-suite/ideal-features/universes.v coq-8.3pl3/test-suite/ideal-features/complexity/ coq-8.3pl3/test-suite/ideal-features/complexity/evars_subst.v coq-8.3pl3/test-suite/ideal-features/Apply.v coq-8.3pl3/test-suite/ideal-features/eapply_evar.v coq-8.3pl3/test-suite/ideal-features/Case8.v coq-8.3pl3/test-suite/ideal-features/evars_subst.v coq-8.3pl3/.gitignore coq-8.3pl3/checker/ coq-8.3pl3/checker/declarations.ml coq-8.3pl3/checker/environ.ml coq-8.3pl3/checker/type_errors.ml coq-8.3pl3/checker/environ.mli coq-8.3pl3/checker/checker.ml coq-8.3pl3/checker/reduction.mli coq-8.3pl3/checker/check_stat.ml coq-8.3pl3/checker/typeops.mli coq-8.3pl3/checker/declarations.mli coq-8.3pl3/checker/validate.ml coq-8.3pl3/checker/term.mli coq-8.3pl3/checker/modops.ml coq-8.3pl3/checker/main.ml coq-8.3pl3/checker/mod_checking.ml coq-8.3pl3/checker/Makefile coq-8.3pl3/checker/inductive.ml coq-8.3pl3/checker/include coq-8.3pl3/checker/subtyping.ml coq-8.3pl3/checker/check_stat.mli coq-8.3pl3/checker/subtyping.mli coq-8.3pl3/checker/check.ml coq-8.3pl3/checker/safe_typing.mli coq-8.3pl3/checker/closure.ml coq-8.3pl3/checker/typeops.ml coq-8.3pl3/checker/reduction.ml coq-8.3pl3/checker/check.mllib coq-8.3pl3/checker/type_errors.mli coq-8.3pl3/checker/indtypes.mli coq-8.3pl3/checker/.depend coq-8.3pl3/checker/closure.mli coq-8.3pl3/checker/term.ml coq-8.3pl3/checker/modops.mli coq-8.3pl3/checker/inductive.mli coq-8.3pl3/checker/safe_typing.ml coq-8.3pl3/checker/indtypes.ml coq-8.3pl3/myocamlbuild.ml coq-8.3pl3/config/ coq-8.3pl3/config/coq_config.mli coq-8.3pl3/config/Makefile.template coq-8.3pl3/LICENSE coq-8.3pl3/_tags coq-8.3pl3/Makefile.stage1 coq-8.3pl3/build coq-8.3pl3/library/ coq-8.3pl3/library/libnames.mli coq-8.3pl3/library/lib.mli coq-8.3pl3/library/lib.ml coq-8.3pl3/library/doc.tex coq-8.3pl3/library/dischargedhypsmap.ml coq-8.3pl3/library/nametab.ml coq-8.3pl3/library/assumptions.mli coq-8.3pl3/library/goptions.ml coq-8.3pl3/library/libnames.ml coq-8.3pl3/library/declaremods.mli coq-8.3pl3/library/goptions.mli coq-8.3pl3/library/decl_kinds.mli coq-8.3pl3/library/heads.mli coq-8.3pl3/library/declaremods.ml coq-8.3pl3/library/nameops.mli coq-8.3pl3/library/nameops.ml coq-8.3pl3/library/nametab.mli coq-8.3pl3/library/summary.ml coq-8.3pl3/library/dischargedhypsmap.mli coq-8.3pl3/library/global.mli coq-8.3pl3/library/decls.ml coq-8.3pl3/library/states.ml coq-8.3pl3/library/summary.mli coq-8.3pl3/library/impargs.mli coq-8.3pl3/library/decls.mli coq-8.3pl3/library/decl_kinds.ml coq-8.3pl3/library/library.ml coq-8.3pl3/library/impargs.ml coq-8.3pl3/library/libobject.mli coq-8.3pl3/library/library.mli coq-8.3pl3/library/states.mli coq-8.3pl3/library/declare.ml coq-8.3pl3/library/assumptions.ml coq-8.3pl3/library/heads.ml coq-8.3pl3/library/libobject.ml coq-8.3pl3/library/declare.mli coq-8.3pl3/library/global.ml coq-8.3pl3/library/library.mllib coq-8.3pl3/INSTALL.doc coq-8.3pl3/tactics/ coq-8.3pl3/tactics/elim.mli coq-8.3pl3/tactics/extraargs.ml4 coq-8.3pl3/tactics/eauto.mli coq-8.3pl3/tactics/doc.tex coq-8.3pl3/tactics/tactics.ml coq-8.3pl3/tactics/eqschemes.mli coq-8.3pl3/tactics/dhyp.mli coq-8.3pl3/tactics/evar_tactics.ml coq-8.3pl3/tactics/extraargs.mli coq-8.3pl3/tactics/btermdn.mli coq-8.3pl3/tactics/dn.ml coq-8.3pl3/tactics/eqschemes.ml coq-8.3pl3/tactics/elim.ml coq-8.3pl3/tactics/tacticals.ml coq-8.3pl3/tactics/tacticals.mli coq-8.3pl3/tactics/dn.mli coq-8.3pl3/tactics/equality.ml coq-8.3pl3/tactics/decl_interp.mli coq-8.3pl3/tactics/refine.ml coq-8.3pl3/tactics/nbtermdn.mli coq-8.3pl3/tactics/tactic_option.mli coq-8.3pl3/tactics/autorewrite.mli coq-8.3pl3/tactics/autorewrite.ml coq-8.3pl3/tactics/class_tactics.ml4 coq-8.3pl3/tactics/inv.mli coq-8.3pl3/tactics/tauto.ml4 coq-8.3pl3/tactics/leminv.ml coq-8.3pl3/tactics/refine.mli coq-8.3pl3/tactics/inv.ml coq-8.3pl3/tactics/hipattern.ml4 coq-8.3pl3/tactics/dhyp.ml coq-8.3pl3/tactics/hipattern.mli coq-8.3pl3/tactics/termdn.mli coq-8.3pl3/tactics/evar_tactics.mli coq-8.3pl3/tactics/auto.mli coq-8.3pl3/tactics/tactics.mllib coq-8.3pl3/tactics/decl_interp.ml coq-8.3pl3/tactics/extratactics.mli coq-8.3pl3/tactics/tactic_option.ml coq-8.3pl3/tactics/termdn.ml coq-8.3pl3/tactics/btermdn.ml coq-8.3pl3/tactics/equality.mli coq-8.3pl3/tactics/elimschemes.ml coq-8.3pl3/tactics/hightactics.mllib coq-8.3pl3/tactics/eqdecide.ml4 coq-8.3pl3/tactics/eauto.ml4 coq-8.3pl3/tactics/elimschemes.mli coq-8.3pl3/tactics/tactics.mli coq-8.3pl3/tactics/decl_proof_instr.ml coq-8.3pl3/tactics/hiddentac.mli coq-8.3pl3/tactics/tacinterp.ml coq-8.3pl3/tactics/decl_proof_instr.mli coq-8.3pl3/tactics/nbtermdn.ml coq-8.3pl3/tactics/leminv.mli coq-8.3pl3/tactics/hiddentac.ml coq-8.3pl3/tactics/auto.ml coq-8.3pl3/tactics/extratactics.ml4 coq-8.3pl3/tactics/contradiction.mli coq-8.3pl3/tactics/contradiction.ml coq-8.3pl3/tactics/rewrite.ml4 coq-8.3pl3/tactics/tacinterp.mli coq-8.3pl3/doc/ coq-8.3pl3/doc/Makefile.rt coq-8.3pl3/doc/tutorial/ coq-8.3pl3/doc/tutorial/Tutorial.tex coq-8.3pl3/doc/RecTutorial/ coq-8.3pl3/doc/RecTutorial/morebib.bib coq-8.3pl3/doc/RecTutorial/manbiblio.bib coq-8.3pl3/doc/RecTutorial/recmacros.tex coq-8.3pl3/doc/RecTutorial/RecTutorial.v coq-8.3pl3/doc/RecTutorial/coqartmacros.tex coq-8.3pl3/doc/RecTutorial/RecTutorial.tex coq-8.3pl3/doc/stdlib/ coq-8.3pl3/doc/stdlib/make-library-index coq-8.3pl3/doc/stdlib/make-library-files coq-8.3pl3/doc/stdlib/Library.tex coq-8.3pl3/doc/stdlib/index-list.html.template coq-8.3pl3/doc/rt/ coq-8.3pl3/doc/rt/Tutorial-cover.tex coq-8.3pl3/doc/rt/RefMan-cover.tex coq-8.3pl3/doc/tools/ coq-8.3pl3/doc/tools/show_latex_messages coq-8.3pl3/doc/tools/Translator.tex coq-8.3pl3/doc/tools/latex_filter coq-8.3pl3/doc/common/ coq-8.3pl3/doc/common/macros.tex coq-8.3pl3/doc/common/title.tex coq-8.3pl3/doc/common/styles/ coq-8.3pl3/doc/common/styles/html/ coq-8.3pl3/doc/common/styles/html/simple/ coq-8.3pl3/doc/common/styles/html/simple/cover.html coq-8.3pl3/doc/common/styles/html/simple/styles.hva coq-8.3pl3/doc/common/styles/html/simple/style.css coq-8.3pl3/doc/common/styles/html/simple/header.html coq-8.3pl3/doc/common/styles/html/simple/hevea.css coq-8.3pl3/doc/common/styles/html/simple/footer.html coq-8.3pl3/doc/common/styles/html/coqremote/ coq-8.3pl3/doc/common/styles/html/coqremote/cover.html coq-8.3pl3/doc/common/styles/html/coqremote/styles.hva coq-8.3pl3/doc/common/styles/html/coqremote/header.html coq-8.3pl3/doc/common/styles/html/coqremote/hevea.css coq-8.3pl3/doc/common/styles/html/coqremote/footer.html coq-8.3pl3/doc/faq/ coq-8.3pl3/doc/faq/interval_discr.v coq-8.3pl3/doc/faq/axioms.png coq-8.3pl3/doc/faq/FAQ.tex coq-8.3pl3/doc/faq/axioms.eps coq-8.3pl3/doc/faq/hevea.sty coq-8.3pl3/doc/faq/fk.bib coq-8.3pl3/doc/faq/axioms.fig coq-8.3pl3/doc/LICENSE coq-8.3pl3/doc/refman/ coq-8.3pl3/doc/refman/RefMan-ltac.tex coq-8.3pl3/doc/refman/Classes.tex coq-8.3pl3/doc/refman/RefMan-ide.tex coq-8.3pl3/doc/refman/RefMan-oth.tex coq-8.3pl3/doc/refman/Coercion.tex coq-8.3pl3/doc/refman/RefMan-int.tex coq-8.3pl3/doc/refman/RefMan-com.tex coq-8.3pl3/doc/refman/biblio.bib coq-8.3pl3/doc/refman/RefMan-ext.tex coq-8.3pl3/doc/refman/RefMan-tac.tex coq-8.3pl3/doc/refman/Setoid.tex coq-8.3pl3/doc/refman/coqdoc.tex coq-8.3pl3/doc/refman/RefMan-lib.tex coq-8.3pl3/doc/refman/Helm.tex coq-8.3pl3/doc/refman/Program.tex coq-8.3pl3/doc/refman/AddRefMan-pre.tex coq-8.3pl3/doc/refman/RefMan-cic.tex coq-8.3pl3/doc/refman/RefMan-coi.tex coq-8.3pl3/doc/refman/RefMan-tus.tex coq-8.3pl3/doc/refman/RefMan-uti.tex coq-8.3pl3/doc/refman/Polynom.tex coq-8.3pl3/doc/refman/RefMan-syn.tex coq-8.3pl3/doc/refman/RefMan-ind.tex coq-8.3pl3/doc/refman/RefMan-pre.tex coq-8.3pl3/doc/refman/menu.html coq-8.3pl3/doc/refman/Omega.tex coq-8.3pl3/doc/refman/headers.sty coq-8.3pl3/doc/refman/RefMan-mod.tex coq-8.3pl3/doc/refman/RefMan-tacex.tex coq-8.3pl3/doc/refman/RefMan-modr.tex coq-8.3pl3/doc/refman/coqide-queries.eps coq-8.3pl3/doc/refman/Natural.tex coq-8.3pl3/doc/refman/coqide.png coq-8.3pl3/doc/refman/Micromega.tex coq-8.3pl3/doc/refman/RefMan-add.tex coq-8.3pl3/doc/refman/hevea.sty coq-8.3pl3/doc/refman/RefMan-gal.tex coq-8.3pl3/doc/refman/Extraction.tex coq-8.3pl3/doc/refman/RefMan-pro.tex coq-8.3pl3/doc/refman/coqide-queries.png coq-8.3pl3/doc/refman/index.html coq-8.3pl3/doc/refman/Cases.tex coq-8.3pl3/doc/refman/coqide.eps coq-8.3pl3/doc/refman/RefMan-decl.tex coq-8.3pl3/doc/refman/Nsatz.tex coq-8.3pl3/doc/refman/headers.hva coq-8.3pl3/doc/refman/Reference-Manual.tex coq-8.3pl3/CREDITS coq-8.3pl3/theories/ coq-8.3pl3/theories/Setoids/ coq-8.3pl3/theories/Setoids/Setoid.v coq-8.3pl3/theories/Setoids/intro.tex coq-8.3pl3/theories/Setoids/vo.itarget coq-8.3pl3/theories/Wellfounded/ coq-8.3pl3/theories/Wellfounded/Wellfounded.v coq-8.3pl3/theories/Wellfounded/Disjoint_Union.v coq-8.3pl3/theories/Wellfounded/Lexicographic_Product.v coq-8.3pl3/theories/Wellfounded/Lexicographic_Exponentiation.v coq-8.3pl3/theories/Wellfounded/Inclusion.v coq-8.3pl3/theories/Wellfounded/Well_Ordering.v coq-8.3pl3/theories/Wellfounded/Transitive_Closure.v coq-8.3pl3/theories/Wellfounded/Union.v coq-8.3pl3/theories/Wellfounded/Inverse_Image.v coq-8.3pl3/theories/Wellfounded/intro.tex coq-8.3pl3/theories/Wellfounded/vo.itarget coq-8.3pl3/theories/theories.itarget coq-8.3pl3/theories/Structures/ coq-8.3pl3/theories/Structures/Equalities.v coq-8.3pl3/theories/Structures/GenericMinMax.v coq-8.3pl3/theories/Structures/OrdersTac.v coq-8.3pl3/theories/Structures/OrderedTypeEx.v coq-8.3pl3/theories/Structures/OrdersFacts.v coq-8.3pl3/theories/Structures/DecidableTypeEx.v coq-8.3pl3/theories/Structures/OrdersLists.v coq-8.3pl3/theories/Structures/DecidableType.v coq-8.3pl3/theories/Structures/OrderedTypeAlt.v coq-8.3pl3/theories/Structures/EqualitiesFacts.v coq-8.3pl3/theories/Structures/OrderedType.v coq-8.3pl3/theories/Structures/Orders.v coq-8.3pl3/theories/Structures/OrdersAlt.v coq-8.3pl3/theories/Structures/OrdersEx.v coq-8.3pl3/theories/Structures/vo.itarget coq-8.3pl3/theories/Relations/ coq-8.3pl3/theories/Relations/Relation_Operators.v coq-8.3pl3/theories/Relations/Operators_Properties.v coq-8.3pl3/theories/Relations/Relations.v coq-8.3pl3/theories/Relations/Relation_Definitions.v coq-8.3pl3/theories/Relations/intro.tex coq-8.3pl3/theories/Relations/vo.itarget coq-8.3pl3/theories/Classes/ coq-8.3pl3/theories/Classes/Morphisms.v coq-8.3pl3/theories/Classes/Equivalence.v coq-8.3pl3/theories/Classes/SetoidClass.v coq-8.3pl3/theories/Classes/SetoidDec.v coq-8.3pl3/theories/Classes/Morphisms_Relations.v coq-8.3pl3/theories/Classes/SetoidTactics.v coq-8.3pl3/theories/Classes/RelationClasses.v coq-8.3pl3/theories/Classes/RelationPairs.v coq-8.3pl3/theories/Classes/Init.v coq-8.3pl3/theories/Classes/EquivDec.v coq-8.3pl3/theories/Classes/vo.itarget coq-8.3pl3/theories/Classes/Morphisms_Prop.v coq-8.3pl3/theories/Strings/ coq-8.3pl3/theories/Strings/Ascii.v coq-8.3pl3/theories/Strings/String.v coq-8.3pl3/theories/Strings/vo.itarget coq-8.3pl3/theories/Logic/ coq-8.3pl3/theories/Logic/FunctionalExtensionality.v coq-8.3pl3/theories/Logic/ClassicalUniqueChoice.v coq-8.3pl3/theories/Logic/ClassicalFacts.v coq-8.3pl3/theories/Logic/Classical_Pred_Set.v coq-8.3pl3/theories/Logic/Classical_Pred_Type.v coq-8.3pl3/theories/Logic/Classical_Prop.v coq-8.3pl3/theories/Logic/SetIsType.v coq-8.3pl3/theories/Logic/Description.v coq-8.3pl3/theories/Logic/ProofIrrelevance.v coq-8.3pl3/theories/Logic/Epsilon.v coq-8.3pl3/theories/Logic/ClassicalChoice.v coq-8.3pl3/theories/Logic/ChoiceFacts.v coq-8.3pl3/theories/Logic/Eqdep.v coq-8.3pl3/theories/Logic/JMeq.v coq-8.3pl3/theories/Logic/RelationalChoice.v coq-8.3pl3/theories/Logic/ConstructiveEpsilon.v coq-8.3pl3/theories/Logic/Classical.v coq-8.3pl3/theories/Logic/ClassicalEpsilon.v coq-8.3pl3/theories/Logic/Eqdep_dec.v coq-8.3pl3/theories/Logic/Decidable.v coq-8.3pl3/theories/Logic/intro.tex coq-8.3pl3/theories/Logic/IndefiniteDescription.v coq-8.3pl3/theories/Logic/EqdepFacts.v coq-8.3pl3/theories/Logic/ClassicalDescription.v coq-8.3pl3/theories/Logic/vo.itarget coq-8.3pl3/theories/Logic/Diaconescu.v coq-8.3pl3/theories/Logic/ProofIrrelevanceFacts.v coq-8.3pl3/theories/Logic/Classical_Type.v coq-8.3pl3/theories/Logic/Hurkens.v coq-8.3pl3/theories/Logic/Berardi.v coq-8.3pl3/theories/Program/ coq-8.3pl3/theories/Program/Wf.v coq-8.3pl3/theories/Program/Equality.v coq-8.3pl3/theories/Program/Tactics.v coq-8.3pl3/theories/Program/Subset.v coq-8.3pl3/theories/Program/Utils.v coq-8.3pl3/theories/Program/Syntax.v coq-8.3pl3/theories/Program/Program.v coq-8.3pl3/theories/Program/Basics.v coq-8.3pl3/theories/Program/Combinators.v coq-8.3pl3/theories/Program/vo.itarget coq-8.3pl3/theories/NArith/ coq-8.3pl3/theories/NArith/Pnat.v coq-8.3pl3/theories/NArith/NOrderedType.v coq-8.3pl3/theories/NArith/BinNat.v coq-8.3pl3/theories/NArith/NArith.v coq-8.3pl3/theories/NArith/Ndec.v coq-8.3pl3/theories/NArith/Nminmax.v coq-8.3pl3/theories/NArith/Ndist.v coq-8.3pl3/theories/NArith/BinPos.v coq-8.3pl3/theories/NArith/Nnat.v coq-8.3pl3/theories/NArith/intro.tex coq-8.3pl3/theories/NArith/Ndigits.v coq-8.3pl3/theories/NArith/POrderedType.v coq-8.3pl3/theories/NArith/vo.itarget coq-8.3pl3/theories/NArith/Pminmax.v coq-8.3pl3/theories/MSets/ coq-8.3pl3/theories/MSets/MSetEqProperties.v coq-8.3pl3/theories/MSets/MSetAVL.v coq-8.3pl3/theories/MSets/MSetFacts.v coq-8.3pl3/theories/MSets/MSetPositive.v coq-8.3pl3/theories/MSets/MSetProperties.v coq-8.3pl3/theories/MSets/MSetDecide.v coq-8.3pl3/theories/MSets/MSetInterface.v coq-8.3pl3/theories/MSets/MSetToFiniteSet.v coq-8.3pl3/theories/MSets/MSets.v coq-8.3pl3/theories/MSets/vo.itarget coq-8.3pl3/theories/MSets/MSetList.v coq-8.3pl3/theories/MSets/MSetWeakList.v coq-8.3pl3/theories/Numbers/ coq-8.3pl3/theories/Numbers/BigNumPrelude.v coq-8.3pl3/theories/Numbers/Rational/ coq-8.3pl3/theories/Numbers/Rational/SpecViaQ/ coq-8.3pl3/theories/Numbers/Rational/SpecViaQ/QSig.v coq-8.3pl3/theories/Numbers/Rational/BigQ/ coq-8.3pl3/theories/Numbers/Rational/BigQ/BigQ.v coq-8.3pl3/theories/Numbers/Rational/BigQ/QMake.v coq-8.3pl3/theories/Numbers/NatInt/ coq-8.3pl3/theories/Numbers/NatInt/NZBase.v coq-8.3pl3/theories/Numbers/NatInt/NZOrder.v coq-8.3pl3/theories/Numbers/NatInt/NZAxioms.v coq-8.3pl3/theories/Numbers/NatInt/NZAddOrder.v coq-8.3pl3/theories/Numbers/NatInt/NZDomain.v coq-8.3pl3/theories/Numbers/NatInt/NZDiv.v coq-8.3pl3/theories/Numbers/NatInt/NZAdd.v coq-8.3pl3/theories/Numbers/NatInt/NZMulOrder.v coq-8.3pl3/theories/Numbers/NatInt/NZMul.v coq-8.3pl3/theories/Numbers/NatInt/NZProperties.v coq-8.3pl3/theories/Numbers/Integer/ coq-8.3pl3/theories/Numbers/Integer/SpecViaZ/ coq-8.3pl3/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v coq-8.3pl3/theories/Numbers/Integer/SpecViaZ/ZSig.v coq-8.3pl3/theories/Numbers/Integer/BigZ/ coq-8.3pl3/theories/Numbers/Integer/BigZ/BigZ.v coq-8.3pl3/theories/Numbers/Integer/BigZ/ZMake.v coq-8.3pl3/theories/Numbers/Integer/NatPairs/ coq-8.3pl3/theories/Numbers/Integer/NatPairs/ZNatPairs.v coq-8.3pl3/theories/Numbers/Integer/Binary/ coq-8.3pl3/theories/Numbers/Integer/Binary/ZBinary.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ coq-8.3pl3/theories/Numbers/Integer/Abstract/ZAxioms.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZMul.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZDivFloor.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZProperties.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZMulOrder.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZAdd.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZBase.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZDivEucl.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZDivTrunc.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZLt.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZAddOrder.v coq-8.3pl3/theories/Numbers/Integer/Abstract/ZSgnAbs.v coq-8.3pl3/theories/Numbers/NumPrelude.v coq-8.3pl3/theories/Numbers/NaryFunctions.v coq-8.3pl3/theories/Numbers/Natural/ coq-8.3pl3/theories/Numbers/Natural/SpecViaZ/ coq-8.3pl3/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v coq-8.3pl3/theories/Numbers/Natural/SpecViaZ/NSig.v coq-8.3pl3/theories/Numbers/Natural/BigN/ coq-8.3pl3/theories/Numbers/Natural/BigN/NMake_gen.ml coq-8.3pl3/theories/Numbers/Natural/BigN/BigN.v coq-8.3pl3/theories/Numbers/Natural/BigN/Nbasic.v coq-8.3pl3/theories/Numbers/Natural/BigN/NMake.v coq-8.3pl3/theories/Numbers/Natural/Peano/ coq-8.3pl3/theories/Numbers/Natural/Peano/NPeano.v coq-8.3pl3/theories/Numbers/Natural/Binary/ coq-8.3pl3/theories/Numbers/Natural/Binary/NBinary.v coq-8.3pl3/theories/Numbers/Natural/Abstract/ coq-8.3pl3/theories/Numbers/Natural/Abstract/NAddOrder.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NProperties.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NMulOrder.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NIso.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NSub.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NDefOps.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NStrongRec.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NBase.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NAdd.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NOrder.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NAxioms.v coq-8.3pl3/theories/Numbers/Natural/Abstract/NDiv.v coq-8.3pl3/theories/Numbers/vo.itarget coq-8.3pl3/theories/Numbers/Cyclic/ coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/ coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v coq-8.3pl3/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v coq-8.3pl3/theories/Numbers/Cyclic/Int31/ coq-8.3pl3/theories/Numbers/Cyclic/Int31/Cyclic31.v coq-8.3pl3/theories/Numbers/Cyclic/Int31/Ring31.v coq-8.3pl3/theories/Numbers/Cyclic/Int31/Int31.v coq-8.3pl3/theories/Numbers/Cyclic/ZModulo/ coq-8.3pl3/theories/Numbers/Cyclic/ZModulo/ZModulo.v coq-8.3pl3/theories/Numbers/Cyclic/Abstract/ coq-8.3pl3/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v coq-8.3pl3/theories/Numbers/Cyclic/Abstract/NZCyclic.v coq-8.3pl3/theories/Sets/ coq-8.3pl3/theories/Sets/Relations_1_facts.v coq-8.3pl3/theories/Sets/Finite_sets_facts.v coq-8.3pl3/theories/Sets/Powerset.v coq-8.3pl3/theories/Sets/Ensembles.v coq-8.3pl3/theories/Sets/Powerset_Classical_facts.v coq-8.3pl3/theories/Sets/Uniset.v coq-8.3pl3/theories/Sets/Infinite_sets.v coq-8.3pl3/theories/Sets/Partial_Order.v coq-8.3pl3/theories/Sets/Classical_sets.v coq-8.3pl3/theories/Sets/Relations_1.v coq-8.3pl3/theories/Sets/Cpo.v coq-8.3pl3/theories/Sets/Finite_sets.v coq-8.3pl3/theories/Sets/Relations_3_facts.v coq-8.3pl3/theories/Sets/Relations_3.v coq-8.3pl3/theories/Sets/Relations_2.v coq-8.3pl3/theories/Sets/Relations_2_facts.v coq-8.3pl3/theories/Sets/Image.v coq-8.3pl3/theories/Sets/Powerset_facts.v coq-8.3pl3/theories/Sets/Integers.v coq-8.3pl3/theories/Sets/intro.tex coq-8.3pl3/theories/Sets/Multiset.v coq-8.3pl3/theories/Sets/Constructive_sets.v coq-8.3pl3/theories/Sets/vo.itarget coq-8.3pl3/theories/Sets/Permut.v coq-8.3pl3/theories/FSets/ coq-8.3pl3/theories/FSets/FMapFacts.v coq-8.3pl3/theories/FSets/FMapFullAVL.v coq-8.3pl3/theories/FSets/FSetEqProperties.v coq-8.3pl3/theories/FSets/FSetDecide.v coq-8.3pl3/theories/FSets/FSetInterface.v coq-8.3pl3/theories/FSets/FSetCompat.v coq-8.3pl3/theories/FSets/FSetAVL.v coq-8.3pl3/theories/FSets/FSetWeakList.v coq-8.3pl3/theories/FSets/FSetFacts.v coq-8.3pl3/theories/FSets/FMapAVL.v coq-8.3pl3/theories/FSets/FMapWeakList.v coq-8.3pl3/theories/FSets/FSetProperties.v coq-8.3pl3/theories/FSets/FSetBridge.v coq-8.3pl3/theories/FSets/FSetList.v coq-8.3pl3/theories/FSets/FMapPositive.v coq-8.3pl3/theories/FSets/FSetPositive.v coq-8.3pl3/theories/FSets/FSetToFiniteSet.v coq-8.3pl3/theories/FSets/FSets.v coq-8.3pl3/theories/FSets/vo.itarget coq-8.3pl3/theories/FSets/FMaps.v coq-8.3pl3/theories/FSets/FMapInterface.v coq-8.3pl3/theories/FSets/FMapList.v coq-8.3pl3/theories/Init/ coq-8.3pl3/theories/Init/Wf.v coq-8.3pl3/theories/Init/Tactics.v coq-8.3pl3/theories/Init/Specif.v coq-8.3pl3/theories/Init/Prelude.v coq-8.3pl3/theories/Init/Datatypes.v coq-8.3pl3/theories/Init/Notations.v coq-8.3pl3/theories/Init/Peano.v coq-8.3pl3/theories/Init/Logic.v coq-8.3pl3/theories/Init/vo.itarget coq-8.3pl3/theories/Init/Logic_Type.v coq-8.3pl3/theories/Lists/ coq-8.3pl3/theories/Lists/ListSet.v coq-8.3pl3/theories/Lists/StreamMemo.v coq-8.3pl3/theories/Lists/ListTactics.v coq-8.3pl3/theories/Lists/Streams.v coq-8.3pl3/theories/Lists/List.v coq-8.3pl3/theories/Lists/SetoidList.v coq-8.3pl3/theories/Lists/TheoryList.v coq-8.3pl3/theories/Lists/intro.tex coq-8.3pl3/theories/Lists/vo.itarget coq-8.3pl3/theories/Arith/ coq-8.3pl3/theories/Arith/Mult.v coq-8.3pl3/theories/Arith/Euclid.v coq-8.3pl3/theories/Arith/Gt.v coq-8.3pl3/theories/Arith/Between.v coq-8.3pl3/theories/Arith/Wf_nat.v coq-8.3pl3/theories/Arith/Compare.v coq-8.3pl3/theories/Arith/Even.v coq-8.3pl3/theories/Arith/Peano_dec.v coq-8.3pl3/theories/Arith/Min.v coq-8.3pl3/theories/Arith/Arith_base.v coq-8.3pl3/theories/Arith/EqNat.v coq-8.3pl3/theories/Arith/MinMax.v coq-8.3pl3/theories/Arith/Bool_nat.v coq-8.3pl3/theories/Arith/NatOrderedType.v coq-8.3pl3/theories/Arith/Max.v coq-8.3pl3/theories/Arith/Lt.v coq-8.3pl3/theories/Arith/Arith.v coq-8.3pl3/theories/Arith/Plus.v coq-8.3pl3/theories/Arith/Compare_dec.v coq-8.3pl3/theories/Arith/Le.v coq-8.3pl3/theories/Arith/Minus.v coq-8.3pl3/theories/Arith/intro.tex coq-8.3pl3/theories/Arith/Div2.v coq-8.3pl3/theories/Arith/Factorial.v coq-8.3pl3/theories/Arith/vo.itarget coq-8.3pl3/theories/ZArith/ coq-8.3pl3/theories/ZArith/Zcompare.v coq-8.3pl3/theories/ZArith/Zdiv.v coq-8.3pl3/theories/ZArith/ZOrderedType.v coq-8.3pl3/theories/ZArith/Zorder.v coq-8.3pl3/theories/ZArith/Zeven.v coq-8.3pl3/theories/ZArith/Zwf.v coq-8.3pl3/theories/ZArith/Zlogarithm.v coq-8.3pl3/theories/ZArith/Zbool.v coq-8.3pl3/theories/ZArith/BinInt.v coq-8.3pl3/theories/ZArith/ZArith.v coq-8.3pl3/theories/ZArith/ZOdiv.v coq-8.3pl3/theories/ZArith/Znat.v coq-8.3pl3/theories/ZArith/Zminmax.v coq-8.3pl3/theories/ZArith/Zmax.v coq-8.3pl3/theories/ZArith/Zpow_def.v coq-8.3pl3/theories/ZArith/Zgcd_alt.v coq-8.3pl3/theories/ZArith/Int.v coq-8.3pl3/theories/ZArith/Zhints.v coq-8.3pl3/theories/ZArith/Znumtheory.v coq-8.3pl3/theories/ZArith/Zcomplements.v coq-8.3pl3/theories/ZArith/Wf_Z.v coq-8.3pl3/theories/ZArith/Zsqrt.v coq-8.3pl3/theories/ZArith/ZOdiv_def.v coq-8.3pl3/theories/ZArith/ZArith_base.v coq-8.3pl3/theories/ZArith/intro.tex coq-8.3pl3/theories/ZArith/Zpower.v coq-8.3pl3/theories/ZArith/ZArith_dec.v coq-8.3pl3/theories/ZArith/Zdigits.v coq-8.3pl3/theories/ZArith/Zmisc.v coq-8.3pl3/theories/ZArith/vo.itarget coq-8.3pl3/theories/ZArith/Zabs.v coq-8.3pl3/theories/ZArith/Zmin.v coq-8.3pl3/theories/ZArith/Zpow_facts.v coq-8.3pl3/theories/ZArith/auxiliary.v coq-8.3pl3/theories/Bool/ coq-8.3pl3/theories/Bool/Zerob.v coq-8.3pl3/theories/Bool/Bool.v coq-8.3pl3/theories/Bool/IfProp.v coq-8.3pl3/theories/Bool/Bvector.v coq-8.3pl3/theories/Bool/Sumbool.v coq-8.3pl3/theories/Bool/intro.tex coq-8.3pl3/theories/Bool/vo.itarget coq-8.3pl3/theories/Bool/DecBool.v coq-8.3pl3/theories/Bool/BoolEq.v coq-8.3pl3/theories/Unicode/ coq-8.3pl3/theories/Unicode/Utf8.v coq-8.3pl3/theories/Unicode/Utf8_core.v coq-8.3pl3/theories/Unicode/vo.itarget coq-8.3pl3/theories/QArith/ coq-8.3pl3/theories/QArith/Qring.v coq-8.3pl3/theories/QArith/QArith_base.v coq-8.3pl3/theories/QArith/Qpower.v coq-8.3pl3/theories/QArith/Qround.v coq-8.3pl3/theories/QArith/Qreduction.v coq-8.3pl3/theories/QArith/Qfield.v coq-8.3pl3/theories/QArith/Qreals.v coq-8.3pl3/theories/QArith/Qabs.v coq-8.3pl3/theories/QArith/Qcanon.v coq-8.3pl3/theories/QArith/QOrderedType.v coq-8.3pl3/theories/QArith/Qminmax.v coq-8.3pl3/theories/QArith/QArith.v coq-8.3pl3/theories/QArith/vo.itarget coq-8.3pl3/theories/Reals/ coq-8.3pl3/theories/Reals/Rlogic.v coq-8.3pl3/theories/Reals/Rminmax.v coq-8.3pl3/theories/Reals/Rtrigo_fun.v coq-8.3pl3/theories/Reals/Rtrigo.v coq-8.3pl3/theories/Reals/Ranalysis3.v coq-8.3pl3/theories/Reals/Rtrigo_alt.v coq-8.3pl3/theories/Reals/Rseries.v coq-8.3pl3/theories/Reals/R_sqrt.v coq-8.3pl3/theories/Reals/Exp_prop.v coq-8.3pl3/theories/Reals/Integration.v coq-8.3pl3/theories/Reals/ROrderedType.v coq-8.3pl3/theories/Reals/SplitRmult.v coq-8.3pl3/theories/Reals/Rpow_def.v coq-8.3pl3/theories/Reals/Cos_plus.v coq-8.3pl3/theories/Reals/Ranalysis4.v coq-8.3pl3/theories/Reals/LegacyRfield.v coq-8.3pl3/theories/Reals/Rprod.v coq-8.3pl3/theories/Reals/Rbase.v coq-8.3pl3/theories/Reals/AltSeries.v coq-8.3pl3/theories/Reals/RIneq.v coq-8.3pl3/theories/Reals/Rdefinitions.v coq-8.3pl3/theories/Reals/RiemannInt.v coq-8.3pl3/theories/Reals/Cos_rel.v coq-8.3pl3/theories/Reals/SeqProp.v coq-8.3pl3/theories/Reals/Rtopology.v coq-8.3pl3/theories/Reals/Rgeom.v coq-8.3pl3/theories/Reals/NewtonInt.v coq-8.3pl3/theories/Reals/Cauchy_prod.v coq-8.3pl3/theories/Reals/Rfunctions.v coq-8.3pl3/theories/Reals/PartSum.v coq-8.3pl3/theories/Reals/SeqSeries.v coq-8.3pl3/theories/Reals/Raxioms.v coq-8.3pl3/theories/Reals/R_Ifp.v coq-8.3pl3/theories/Reals/Rderiv.v coq-8.3pl3/theories/Reals/RiemannInt_SF.v coq-8.3pl3/theories/Reals/MVT.v coq-8.3pl3/theories/Reals/Ranalysis.v coq-8.3pl3/theories/Reals/Ranalysis1.v coq-8.3pl3/theories/Reals/Sqrt_reg.v coq-8.3pl3/theories/Reals/Rsqrt_def.v coq-8.3pl3/theories/Reals/Rtrigo_reg.v coq-8.3pl3/theories/Reals/Binomial.v coq-8.3pl3/theories/Reals/PSeries_reg.v coq-8.3pl3/theories/Reals/ArithProp.v coq-8.3pl3/theories/Reals/Rtrigo_calc.v coq-8.3pl3/theories/Reals/Rlimit.v coq-8.3pl3/theories/Reals/intro.tex coq-8.3pl3/theories/Reals/R_sqr.v coq-8.3pl3/theories/Reals/Rpower.v coq-8.3pl3/theories/Reals/Alembert.v coq-8.3pl3/theories/Reals/Rbasic_fun.v coq-8.3pl3/theories/Reals/DiscrR.v coq-8.3pl3/theories/Reals/Rcomplete.v coq-8.3pl3/theories/Reals/vo.itarget coq-8.3pl3/theories/Reals/Rsigma.v coq-8.3pl3/theories/Reals/Ranalysis2.v coq-8.3pl3/theories/Reals/RList.v coq-8.3pl3/theories/Reals/Rtrigo_def.v coq-8.3pl3/theories/Reals/Reals.v coq-8.3pl3/theories/Reals/SplitAbsolu.v coq-8.3pl3/theories/Sorting/ coq-8.3pl3/theories/Sorting/PermutEq.v coq-8.3pl3/theories/Sorting/Sorted.v coq-8.3pl3/theories/Sorting/Sorting.v coq-8.3pl3/theories/Sorting/Heap.v coq-8.3pl3/theories/Sorting/Permutation.v coq-8.3pl3/theories/Sorting/Mergesort.v coq-8.3pl3/theories/Sorting/PermutSetoid.v coq-8.3pl3/theories/Sorting/intro.tex coq-8.3pl3/theories/Sorting/vo.itarget coq-8.3pl3/pretyping/ coq-8.3pl3/pretyping/classops.mli coq-8.3pl3/pretyping/reductionops.ml coq-8.3pl3/pretyping/tacred.ml coq-8.3pl3/pretyping/detyping.ml coq-8.3pl3/pretyping/doc.tex coq-8.3pl3/pretyping/indrec.ml coq-8.3pl3/pretyping/clenv.ml coq-8.3pl3/pretyping/rawterm.ml coq-8.3pl3/pretyping/termops.ml coq-8.3pl3/pretyping/typing.ml coq-8.3pl3/pretyping/vnorm.mli coq-8.3pl3/pretyping/matching.ml coq-8.3pl3/pretyping/evarutil.ml coq-8.3pl3/pretyping/reductionops.mli coq-8.3pl3/pretyping/evd.ml coq-8.3pl3/pretyping/cases.mli coq-8.3pl3/pretyping/retyping.ml coq-8.3pl3/pretyping/termops.mli coq-8.3pl3/pretyping/inductiveops.ml coq-8.3pl3/pretyping/unification.ml coq-8.3pl3/pretyping/vnorm.ml coq-8.3pl3/pretyping/pretyping.mllib coq-8.3pl3/pretyping/typeclasses.mli coq-8.3pl3/pretyping/cbv.mli coq-8.3pl3/pretyping/typeclasses.ml coq-8.3pl3/pretyping/pretype_errors.mli coq-8.3pl3/pretyping/coercion.mli coq-8.3pl3/pretyping/typeclasses_errors.ml coq-8.3pl3/pretyping/pattern.ml coq-8.3pl3/pretyping/evarutil.mli coq-8.3pl3/pretyping/typeclasses_errors.mli coq-8.3pl3/pretyping/pattern.mli coq-8.3pl3/pretyping/pretype_errors.ml coq-8.3pl3/pretyping/typing.mli coq-8.3pl3/pretyping/coercion.ml coq-8.3pl3/pretyping/indrec.mli coq-8.3pl3/pretyping/classops.ml coq-8.3pl3/pretyping/term_dnet.mli coq-8.3pl3/pretyping/inductiveops.mli coq-8.3pl3/pretyping/cbv.ml coq-8.3pl3/pretyping/evarconv.mli coq-8.3pl3/pretyping/pretyping.ml coq-8.3pl3/pretyping/evd.mli coq-8.3pl3/pretyping/tacred.mli coq-8.3pl3/pretyping/retyping.mli coq-8.3pl3/pretyping/namegen.mli coq-8.3pl3/pretyping/recordops.mli coq-8.3pl3/pretyping/evarconv.ml coq-8.3pl3/pretyping/term_dnet.ml coq-8.3pl3/pretyping/recordops.ml coq-8.3pl3/pretyping/detyping.mli coq-8.3pl3/pretyping/namegen.ml coq-8.3pl3/pretyping/pretyping.mli coq-8.3pl3/pretyping/matching.mli coq-8.3pl3/pretyping/unification.mli coq-8.3pl3/pretyping/clenv.mli coq-8.3pl3/pretyping/cases.ml coq-8.3pl3/pretyping/rawterm.mli coq-8.3pl3/proofs/ coq-8.3pl3/proofs/decl_mode.mli coq-8.3pl3/proofs/doc.tex coq-8.3pl3/proofs/redexpr.mli coq-8.3pl3/proofs/refiner.mli coq-8.3pl3/proofs/evar_refiner.mli coq-8.3pl3/proofs/tmp-src coq-8.3pl3/proofs/proof_type.ml coq-8.3pl3/proofs/proofs.mllib coq-8.3pl3/proofs/pfedit.ml coq-8.3pl3/proofs/tacexpr.ml coq-8.3pl3/proofs/proof_trees.mli coq-8.3pl3/proofs/redexpr.ml coq-8.3pl3/proofs/tactic_debug.ml coq-8.3pl3/proofs/proof_trees.ml coq-8.3pl3/proofs/clenvtac.mli coq-8.3pl3/proofs/pfedit.mli coq-8.3pl3/proofs/logic.ml coq-8.3pl3/proofs/clenvtac.ml coq-8.3pl3/proofs/decl_expr.mli coq-8.3pl3/proofs/tactic_debug.mli coq-8.3pl3/proofs/tacmach.mli coq-8.3pl3/proofs/tacmach.ml coq-8.3pl3/proofs/refiner.ml coq-8.3pl3/proofs/evar_refiner.ml coq-8.3pl3/proofs/logic.mli coq-8.3pl3/proofs/proof_type.mli coq-8.3pl3/proofs/decl_mode.ml coq-8.3pl3/CHANGES coq-8.3pl3/man/ coq-8.3pl3/man/coqtop.byte.1 coq-8.3pl3/man/coqdoc.1 coq-8.3pl3/man/coqchk.1 coq-8.3pl3/man/coqide.1 coq-8.3pl3/man/coq-tex.1 coq-8.3pl3/man/coqmktop.1 coq-8.3pl3/man/coqdep.1 coq-8.3pl3/man/coqtop.1 coq-8.3pl3/man/coqwc.1 coq-8.3pl3/man/coq_makefile.1 coq-8.3pl3/man/coqc.1 coq-8.3pl3/man/coq-parser.1 coq-8.3pl3/man/coqtop.opt.1 coq-8.3pl3/man/gallina.1 coq-8.3pl3/man/coq-interface.1 coq-8.3pl3/coq.itarget coq-8.3pl3/coq-win32.itarget coq-8.3pl3/configure coq-8.3pl3/ide/ coq-8.3pl3/ide/.coqide-gtk2rc coq-8.3pl3/ide/ide.mllib coq-8.3pl3/ide/undo_lablgtk_ge212.mli coq-8.3pl3/ide/coqide.ml coq-8.3pl3/ide/typed_notebook.ml coq-8.3pl3/ide/utils/ coq-8.3pl3/ide/utils/editable_cells.ml coq-8.3pl3/ide/utils/configwin.ml coq-8.3pl3/ide/utils/configwin_ihm.ml coq-8.3pl3/ide/utils/config_file.ml coq-8.3pl3/ide/utils/configwin_keys.ml coq-8.3pl3/ide/utils/configwin_types.ml coq-8.3pl3/ide/utils/configwin.mli coq-8.3pl3/ide/utils/config_file.mli coq-8.3pl3/ide/utils/okey.ml coq-8.3pl3/ide/utils/okey.mli coq-8.3pl3/ide/utils/configwin_messages.ml coq-8.3pl3/ide/coq_tactics.mli coq-8.3pl3/ide/config_parser.mly coq-8.3pl3/ide/config_lexer.mll coq-8.3pl3/ide/coq.mli coq-8.3pl3/ide/coq_tactics.ml coq-8.3pl3/ide/command_windows.mli coq-8.3pl3/ide/gtk_parsing.ml coq-8.3pl3/ide/preferences.ml coq-8.3pl3/ide/utf8_convert.mll coq-8.3pl3/ide/ideutils.mli coq-8.3pl3/ide/coq.png coq-8.3pl3/ide/ideutils.ml coq-8.3pl3/ide/undo.ml coq-8.3pl3/ide/coq.ml coq-8.3pl3/ide/FAQ coq-8.3pl3/ide/undo_lablgtk_ge26.mli coq-8.3pl3/ide/coq_commands.ml coq-8.3pl3/ide/undo_lablgtk_lt26.mli coq-8.3pl3/ide/coq.ico coq-8.3pl3/ide/coq2.ico coq-8.3pl3/ide/coq_lex.mll coq-8.3pl3/ide/preferences.mli coq-8.3pl3/ide/coq_icon.rc coq-8.3pl3/ide/tags.ml coq-8.3pl3/ide/command_windows.ml coq-8.3pl3/ide/highlight.mll coq-8.3pl3/ide/uim/ coq-8.3pl3/ide/uim/coqide-rules.scm coq-8.3pl3/ide/uim/coqide.scm coq-8.3pl3/ide/uim/coqide-custom.scm coq-8.3pl3/ide/coqide.mli coq-8.3pl3/README coq-8.3pl3/dev/ coq-8.3pl3/dev/ocamldebug-coq.template coq-8.3pl3/dev/tools/ coq-8.3pl3/dev/tools/Makefile.subdir coq-8.3pl3/dev/tools/Makefile.common coq-8.3pl3/dev/tools/Makefile.devel coq-8.3pl3/dev/tools/Makefile.dir coq-8.3pl3/dev/tools/univdot coq-8.3pl3/dev/tools/objects.el coq-8.3pl3/dev/include coq-8.3pl3/dev/ocamlopt_shared_os5fix.sh coq-8.3pl3/dev/base_include coq-8.3pl3/dev/ocamlweb-doc/ coq-8.3pl3/dev/ocamlweb-doc/pretyping.dep.ps coq-8.3pl3/dev/ocamlweb-doc/preamble.tex coq-8.3pl3/dev/ocamlweb-doc/library.dep.ps coq-8.3pl3/dev/ocamlweb-doc/tactics.dep.ps coq-8.3pl3/dev/ocamlweb-doc/Makefile coq-8.3pl3/dev/ocamlweb-doc/parsing.dep.ps coq-8.3pl3/dev/ocamlweb-doc/kernel.dep.ps coq-8.3pl3/dev/ocamlweb-doc/parse.ml coq-8.3pl3/dev/ocamlweb-doc/macros.tex coq-8.3pl3/dev/ocamlweb-doc/lex.mll coq-8.3pl3/dev/ocamlweb-doc/ast.ml coq-8.3pl3/dev/ocamlweb-doc/syntax.mly coq-8.3pl3/dev/ocamlweb-doc/interp.dep.ps coq-8.3pl3/dev/ocamlweb-doc/proofs.dep.ps coq-8.3pl3/dev/ocamlweb-doc/intro.tex coq-8.3pl3/dev/ocamlweb-doc/toplevel.dep.ps coq-8.3pl3/dev/base_db coq-8.3pl3/dev/vm_printers.ml coq-8.3pl3/dev/TODO coq-8.3pl3/dev/db coq-8.3pl3/dev/doc/ coq-8.3pl3/dev/doc/changes.txt coq-8.3pl3/dev/doc/naming-conventions.tex coq-8.3pl3/dev/doc/versions-history.tex coq-8.3pl3/dev/doc/patch.ocaml-3.10.drop.rectypes coq-8.3pl3/dev/doc/minicoq.tex coq-8.3pl3/dev/doc/build-system.dev.txt coq-8.3pl3/dev/doc/universes.txt coq-8.3pl3/dev/doc/translate.txt coq-8.3pl3/dev/doc/build-system.txt coq-8.3pl3/dev/doc/extensions.txt coq-8.3pl3/dev/doc/newsyntax.tex coq-8.3pl3/dev/doc/perf-analysis coq-8.3pl3/dev/doc/debugging.txt coq-8.3pl3/dev/doc/notes-on-conversion coq-8.3pl3/dev/doc/style.txt coq-8.3pl3/dev/doc/cic.dtd coq-8.3pl3/dev/v8-syntax/ coq-8.3pl3/dev/v8-syntax/memo-v8.tex coq-8.3pl3/dev/v8-syntax/syntax-v8.tex coq-8.3pl3/dev/v8-syntax/check-grammar coq-8.3pl3/dev/db_printers.ml coq-8.3pl3/dev/header coq-8.3pl3/dev/set_raw_db coq-8.3pl3/dev/README coq-8.3pl3/dev/top_printers.ml coq-8.3pl3/dev/printers.mllib coq-8.3pl3/parsing/ coq-8.3pl3/parsing/printmod.mli coq-8.3pl3/parsing/doc.tex coq-8.3pl3/parsing/tacextend.ml4 coq-8.3pl3/parsing/printer.mli coq-8.3pl3/parsing/q_constr.ml4 coq-8.3pl3/parsing/g_ltac.ml4 coq-8.3pl3/parsing/printmod.ml coq-8.3pl3/parsing/ppvernac.mli coq-8.3pl3/parsing/g_prim.ml4 coq-8.3pl3/parsing/ppconstr.mli coq-8.3pl3/parsing/grammar.mllib coq-8.3pl3/parsing/tactic_printer.ml coq-8.3pl3/parsing/ppconstr.ml coq-8.3pl3/parsing/printer.ml coq-8.3pl3/parsing/g_decl_mode.ml4 coq-8.3pl3/parsing/g_proofs.ml4 coq-8.3pl3/parsing/pptactic.mli coq-8.3pl3/parsing/pcoq.ml4 coq-8.3pl3/parsing/vernacextend.ml4 coq-8.3pl3/parsing/pcoq.mli coq-8.3pl3/parsing/highparsing.mllib coq-8.3pl3/parsing/prettyp.mli coq-8.3pl3/parsing/tactic_printer.mli coq-8.3pl3/parsing/prettyp.ml coq-8.3pl3/parsing/pptactic.ml coq-8.3pl3/parsing/extend.mli coq-8.3pl3/parsing/lexer.mli coq-8.3pl3/parsing/g_xml.ml4 coq-8.3pl3/parsing/q_util.ml4 coq-8.3pl3/parsing/g_natsyntax.mli coq-8.3pl3/parsing/ppdecl_proof.ml coq-8.3pl3/parsing/ppvernac.ml coq-8.3pl3/parsing/lexer.ml4 coq-8.3pl3/parsing/g_vernac.ml4 coq-8.3pl3/parsing/parsing.mllib coq-8.3pl3/parsing/extrawit.mli coq-8.3pl3/parsing/g_intsyntax.mli coq-8.3pl3/parsing/q_util.mli coq-8.3pl3/parsing/extrawit.ml coq-8.3pl3/parsing/extend.ml coq-8.3pl3/parsing/egrammar.mli coq-8.3pl3/parsing/ppdecl_proof.mli coq-8.3pl3/parsing/g_tactic.ml4 coq-8.3pl3/parsing/q_coqast.ml4 coq-8.3pl3/parsing/g_constr.ml4 coq-8.3pl3/parsing/egrammar.ml coq-8.3pl3/parsing/g_zsyntax.mli coq-8.3pl3/parsing/argextend.ml4 sudo -u fink-bld [ENV] sh -c /tmp/fink.AK52L [ -r /sw/fink/dists/stable/main/finkinfo/sci/coqide.patch ] sudo -u fink-bld [ENV] sh -c /tmp/fink.pSvdU patch -p1 < /sw/fink/dists/stable/main/finkinfo/sci/coqide.patch patching file README.fink sudo -u fink-bld [ENV] sh -c /tmp/fink.HxM2j /tmp/fink.dycuK #!/bin/sh -ev export PKG_CONFIG_PATH="/sw/lib/pango-ft219/lib/pkgconfig:/sw/lib/fontconfig2/lib/pkgconfig:/sw/lib/freetype219/lib/pkgconfig:$PKG_CONFIG_PATH" FREETYPE_CONFIG=/sw/lib/freetype219/bin/freetype-config ./configure -prefix /sw -coqdocdir /sw/share/doc/coq -mandir /sw/share/man -emacslib /sw/share/emacs/site-lisp/coq -opt -with-doc no -browser 'open %s' You have GNU Make 3.81. Good! You have Objective-Caml 4.01.0. Good! Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3, only the bytecode version of Coq will be available. LablGtk2 found, bytecode CoqIde will be used as requested. Coq top directory : /sw/build.build/coqide-8.3pl3-1/coq-8.3pl3 Architecture : i386 Coq VM bytecode link flags : -custom Coq tools bytecode link flags : -custom OS dependent libraries : -cclib -lunix Objective-Caml/Camlp4 version : 4.01.0 Objective-Caml/Camlp4 binaries in : /sw/bin Objective-Caml library in : /sw/lib/ocaml Camlp4 library in : +camlp4 Lablgtk2 library in : +lablgtk2 Documentation : None CoqIde : byte Web browser : open %s Coq web site : http://coq.inria.fr/ Paths for true installation: binaries will be copied in /sw/bin library will be copied in /sw/lib/coq man pages will be copied in /sw/share/man documentation will be copied in /sw/share/doc/coq emacs mode will be copied in /sw/share/emacs/site-lisp/coq If anything in the above is wrong, please restart './configure'. *Warning* To compile the system for a new architecture don't forget to do a 'make archclean' before './configure'. make coqide ***************************************************** ***************************************************** ****************** Entering stage1 ****************** ***************************************************** ***************************************************** /Applications/Xcode.app/Contents/Developer/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage1 "stage1" 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} ) OCAMLLEX dev/ocamlweb-doc/lex.mll OCAMLLEX ide/config_lexer.mll OCAMLLEX ide/coq_lex.mll OCAMLLEX ide/highlight.mll OCAMLLEX ide/utf8_convert.mll OCAMLLEX plugins/dp/dp_zenon.mll OCAMLLEX tools/coqdep_lexer.mll OCAMLLEX tools/coqdoc/cpretty.mll 13 states, 332 transitions, table size 1406 bytes 15 states, 827 transitions, table size 3398 bytes OCAMLLEX tools/coqwc.mll OCAMLLEX tools/gallina_lexer.mll 85 states, 637 transitions, table size 3058 bytes 1881 additional bytes used for bindings OCAMLYACC dev/ocamlweb-doc/syntax.mly 3 shift/reduce conflicts. 99 states, 6415 transitions, table size 26254 bytes 190 states, 498 transitions, table size 3132 bytes 230 states, 833 transitions, table size 4712 bytes OCAMLYACC ide/config_parser.mly 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} ) ECHO... > scripts/tolink.ml 200 states, 5470 transitions, table size 23080 bytes 2243 additional bytes used for bindings "ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > theories/Numbers/Natural/BigN/NMake_gen.v TOUCH lib/compat.ml TOUCH lib/pp.ml TOUCH lib/refutpat.ml TOUCH parsing/argextend.ml TOUCH parsing/g_constr.ml TOUCH parsing/g_decl_mode.ml TOUCH parsing/g_ltac.ml TOUCH parsing/g_prim.ml TOUCH parsing/g_proofs.ml TOUCH parsing/g_tactic.ml TOUCH parsing/g_vernac.ml TOUCH parsing/g_xml.ml TOUCH parsing/lexer.ml TOUCH parsing/pcoq.ml TOUCH parsing/q_constr.ml TOUCH parsing/q_coqast.ml TOUCH parsing/q_util.ml TOUCH parsing/tacextend.ml TOUCH parsing/vernacextend.ml TOUCH plugins/cc/g_congruence.ml TOUCH plugins/dp/g_dp.ml TOUCH plugins/extraction/g_extraction.ml TOUCH plugins/field/field.ml TOUCH plugins/firstorder/g_ground.ml TOUCH plugins/fourier/g_fourier.ml TOUCH plugins/funind/g_indfun.ml TOUCH plugins/micromega/g_micromega.ml TOUCH plugins/nsatz/nsatz.ml TOUCH plugins/omega/g_omega.ml TOUCH plugins/quote/g_quote.ml TOUCH plugins/ring/g_ring.ml TOUCH plugins/romega/g_romega.ml TOUCH plugins/rtauto/g_rtauto.ml TOUCH plugins/setoid_ring/newring.ml TOUCH plugins/subtac/g_subtac.ml TOUCH plugins/xml/acic2Xml.ml TOUCH plugins/xml/dumptree.ml TOUCH plugins/xml/proofTree2Xml.ml TOUCH plugins/xml/xml.ml TOUCH plugins/xml/xmlentries.ml TOUCH tactics/class_tactics.ml TOUCH tactics/eauto.ml TOUCH tactics/eqdecide.ml TOUCH tactics/extraargs.ml 457 states, 31161 transitions, table size 127386 bytes TOUCH tactics/extratactics.ml TOUCH tactics/hipattern.ml 455 states, 31494 transitions, table size 128706 bytes TOUCH tactics/rewrite.ml 2130 states, 6900 transitions, table size 40380 bytes TOUCH tactics/tauto.ml TOUCH tools/coq_makefile.ml TOUCH tools/coq_tex.ml TOUCH toplevel/mltop.ml TOUCH toplevel/whelp.ml CAMLP4DEPS parsing/q_constr.ml4 CAMLP4DEPS parsing/q_coqast.ml4 CAMLP4DEPS parsing/lexer.ml4 CAMLP4DEPS parsing/g_constr.ml4 CAMLP4DEPS parsing/g_ltac.ml4 CAMLP4DEPS parsing/g_tactic.ml4 CAMLP4DEPS parsing/g_prim.ml4 CAMLP4DEPS parsing/vernacextend.ml4 CAMLP4DEPS parsing/tacextend.ml4 CAMLP4DEPS parsing/argextend.ml4 CAMLP4DEPS parsing/pcoq.ml4 CAMLP4DEPS parsing/q_util.ml4 CAMLP4DEPS lib/pp.ml4 CAMLP4DEPS lib/compat.ml4 OCAMLDEP ide/config_parser.mli OCAMLDEP dev/ocamlweb-doc/syntax.mli OCAMLDEP toplevel/whelp.mli OCAMLDEP toplevel/vernacinterp.mli OCAMLDEP toplevel/vernacentries.mli OCAMLDEP toplevel/vernac.mli OCAMLDEP toplevel/usage.mli OCAMLDEP toplevel/toplevel.mli OCAMLDEP toplevel/search.mli OCAMLDEP toplevel/record.mli OCAMLDEP toplevel/mltop.mli OCAMLDEP toplevel/metasyntax.mli OCAMLDEP toplevel/libtypes.mli OCAMLDEP toplevel/lemmas.mli OCAMLDEP toplevel/indschemes.mli OCAMLDEP toplevel/ind_tables.mli OCAMLDEP toplevel/himsg.mli OCAMLDEP toplevel/discharge.mli OCAMLDEP toplevel/coqtop.mli OCAMLDEP toplevel/coqinit.mli OCAMLDEP toplevel/command.mli OCAMLDEP toplevel/classes.mli OCAMLDEP toplevel/class.mli OCAMLDEP toplevel/cerrors.mli OCAMLDEP toplevel/autoinstance.mli OCAMLDEP toplevel/auto_ind_decl.mli OCAMLDEP tools/coqdoc/tokens.mli OCAMLDEP tools/coqdoc/output.mli OCAMLDEP tools/coqdoc/index.mli OCAMLDEP tools/coqdoc/cpretty.mli OCAMLDEP tools/coqdoc/alpha.mli OCAMLDEP tactics/termdn.mli OCAMLDEP tactics/tactics.mli OCAMLDEP tactics/tacticals.mli OCAMLDEP tactics/tactic_option.mli OCAMLDEP tactics/tacinterp.mli OCAMLDEP tactics/refine.mli OCAMLDEP tactics/nbtermdn.mli OCAMLDEP tactics/leminv.mli OCAMLDEP tactics/inv.mli OCAMLDEP tactics/hipattern.mli OCAMLDEP tactics/hiddentac.mli OCAMLDEP tactics/extratactics.mli OCAMLDEP tactics/extraargs.mli OCAMLDEP tactics/evar_tactics.mli OCAMLDEP tactics/equality.mli OCAMLDEP tactics/eqschemes.mli OCAMLDEP tactics/elimschemes.mli OCAMLDEP tactics/elim.mli OCAMLDEP tactics/eauto.mli OCAMLDEP tactics/dn.mli OCAMLDEP tactics/dhyp.mli OCAMLDEP tactics/decl_proof_instr.mli OCAMLDEP tactics/decl_interp.mli OCAMLDEP tactics/contradiction.mli OCAMLDEP tactics/btermdn.mli OCAMLDEP tactics/autorewrite.mli OCAMLDEP tactics/auto.mli OCAMLDEP proofs/tactic_debug.mli OCAMLDEP proofs/tacmach.mli OCAMLDEP proofs/refiner.mli OCAMLDEP proofs/redexpr.mli OCAMLDEP proofs/proof_type.mli OCAMLDEP proofs/proof_trees.mli OCAMLDEP proofs/pfedit.mli OCAMLDEP proofs/logic.mli OCAMLDEP proofs/evar_refiner.mli OCAMLDEP proofs/decl_mode.mli OCAMLDEP proofs/decl_expr.mli OCAMLDEP proofs/clenvtac.mli OCAMLDEP pretyping/vnorm.mli OCAMLDEP pretyping/unification.mli OCAMLDEP pretyping/typing.mli OCAMLDEP pretyping/typeclasses_errors.mli OCAMLDEP pretyping/typeclasses.mli OCAMLDEP pretyping/termops.mli OCAMLDEP pretyping/term_dnet.mli OCAMLDEP pretyping/tacred.mli OCAMLDEP pretyping/retyping.mli OCAMLDEP pretyping/reductionops.mli OCAMLDEP pretyping/recordops.mli OCAMLDEP pretyping/rawterm.mli OCAMLDEP pretyping/pretyping.mli OCAMLDEP pretyping/pretype_errors.mli OCAMLDEP pretyping/pattern.mli OCAMLDEP pretyping/namegen.mli OCAMLDEP pretyping/matching.mli OCAMLDEP pretyping/inductiveops.mli OCAMLDEP pretyping/indrec.mli OCAMLDEP pretyping/evd.mli OCAMLDEP pretyping/evarutil.mli OCAMLDEP pretyping/evarconv.mli OCAMLDEP pretyping/detyping.mli OCAMLDEP pretyping/coercion.mli OCAMLDEP pretyping/clenv.mli OCAMLDEP pretyping/classops.mli OCAMLDEP pretyping/cbv.mli OCAMLDEP pretyping/cases.mli OCAMLDEP plugins/xml/xmlcommand.mli OCAMLDEP plugins/xml/xml.mli OCAMLDEP plugins/xml/unshare.mli OCAMLDEP plugins/xml/doubleTypeInference.mli OCAMLDEP plugins/subtac/subtac_utils.mli OCAMLDEP plugins/subtac/subtac_pretyping.mli OCAMLDEP plugins/subtac/subtac_obligations.mli OCAMLDEP plugins/subtac/subtac_errors.mli OCAMLDEP plugins/subtac/subtac_command.mli OCAMLDEP plugins/subtac/subtac_coercion.mli OCAMLDEP plugins/subtac/subtac_classes.mli OCAMLDEP plugins/subtac/subtac_cases.mli OCAMLDEP plugins/subtac/subtac.mli OCAMLDEP plugins/subtac/eterm.mli OCAMLDEP plugins/rtauto/refl_tauto.mli OCAMLDEP plugins/rtauto/proof_search.mli OCAMLDEP plugins/romega/const_omega.mli OCAMLDEP plugins/nsatz/utile.mli OCAMLDEP plugins/nsatz/polynom.mli OCAMLDEP plugins/micromega/sos.mli OCAMLDEP plugins/micromega/micromega.mli OCAMLDEP plugins/funind/rawtermops.mli OCAMLDEP plugins/funind/rawterm_to_relation.mli OCAMLDEP plugins/funind/indfun_common.mli OCAMLDEP plugins/funind/functional_principles_types.mli OCAMLDEP plugins/funind/functional_principles_proofs.mli OCAMLDEP plugins/firstorder/unify.mli OCAMLDEP plugins/firstorder/sequent.mli OCAMLDEP plugins/firstorder/rules.mli OCAMLDEP plugins/firstorder/instances.mli OCAMLDEP plugins/firstorder/ground.mli OCAMLDEP plugins/firstorder/formula.mli OCAMLDEP plugins/extraction/table.mli OCAMLDEP plugins/extraction/scheme.mli OCAMLDEP plugins/extraction/ocaml.mli OCAMLDEP plugins/extraction/modutil.mli OCAMLDEP plugins/extraction/mlutil.mli OCAMLDEP plugins/extraction/miniml.mli OCAMLDEP plugins/extraction/haskell.mli OCAMLDEP plugins/extraction/extraction.mli OCAMLDEP plugins/extraction/extract_env.mli OCAMLDEP plugins/extraction/common.mli OCAMLDEP plugins/dp/fol.mli OCAMLDEP plugins/dp/dp_zenon.mli OCAMLDEP plugins/dp/dp_why.mli OCAMLDEP plugins/dp/dp.mli OCAMLDEP plugins/cc/cctac.mli OCAMLDEP plugins/cc/ccproof.mli OCAMLDEP plugins/cc/ccalgo.mli OCAMLDEP parsing/tactic_printer.mli OCAMLDEP parsing/q_util.mli OCAMLDEP parsing/printmod.mli OCAMLDEP parsing/printer.mli OCAMLDEP parsing/prettyp.mli OCAMLDEP parsing/ppvernac.mli OCAMLDEP parsing/pptactic.mli OCAMLDEP parsing/ppdecl_proof.mli OCAMLDEP parsing/ppconstr.mli OCAMLDEP parsing/pcoq.mli OCAMLDEP parsing/lexer.mli OCAMLDEP parsing/g_zsyntax.mli OCAMLDEP parsing/g_natsyntax.mli OCAMLDEP parsing/g_intsyntax.mli OCAMLDEP parsing/extrawit.mli OCAMLDEP parsing/extend.mli OCAMLDEP parsing/egrammar.mli OCAMLDEP library/summary.mli OCAMLDEP library/states.mli OCAMLDEP library/nametab.mli OCAMLDEP library/nameops.mli OCAMLDEP library/library.mli OCAMLDEP library/libobject.mli OCAMLDEP library/libnames.mli OCAMLDEP library/lib.mli OCAMLDEP library/impargs.mli OCAMLDEP library/heads.mli OCAMLDEP library/goptions.mli OCAMLDEP library/global.mli OCAMLDEP library/dischargedhypsmap.mli OCAMLDEP library/decls.mli OCAMLDEP library/declaremods.mli OCAMLDEP library/declare.mli OCAMLDEP library/decl_kinds.mli OCAMLDEP library/assumptions.mli OCAMLDEP lib/util.mli OCAMLDEP lib/tries.mli OCAMLDEP lib/tlm.mli OCAMLDEP lib/system.mli OCAMLDEP lib/segmenttree.mli OCAMLDEP lib/rtree.mli OCAMLDEP lib/profile.mli OCAMLDEP lib/predicate.mli OCAMLDEP lib/pp_control.mli OCAMLDEP lib/pp.mli OCAMLDEP lib/option.mli OCAMLDEP lib/heap.mli OCAMLDEP lib/hashcons.mli OCAMLDEP lib/gset.mli OCAMLDEP lib/gmapl.mli OCAMLDEP lib/gmap.mli OCAMLDEP lib/fset.mli OCAMLDEP lib/fmap.mli OCAMLDEP lib/flags.mli OCAMLDEP lib/explore.mli OCAMLDEP lib/envars.mli OCAMLDEP lib/edit.mli OCAMLDEP lib/dyn.mli OCAMLDEP lib/dnet.mli OCAMLDEP lib/bstack.mli OCAMLDEP lib/bigint.mli OCAMLDEP kernel/vm.mli OCAMLDEP kernel/vconv.mli OCAMLDEP kernel/univ.mli OCAMLDEP kernel/typeops.mli OCAMLDEP kernel/type_errors.mli OCAMLDEP kernel/term_typing.mli OCAMLDEP kernel/term.mli OCAMLDEP kernel/subtyping.mli OCAMLDEP kernel/sign.mli OCAMLDEP kernel/safe_typing.mli OCAMLDEP kernel/retroknowledge.mli OCAMLDEP kernel/reduction.mli OCAMLDEP kernel/pre_env.mli OCAMLDEP kernel/names.mli OCAMLDEP kernel/modops.mli OCAMLDEP kernel/mod_typing.mli OCAMLDEP kernel/mod_subst.mli OCAMLDEP kernel/inductive.mli OCAMLDEP kernel/indtypes.mli OCAMLDEP kernel/esubst.mli OCAMLDEP kernel/environ.mli OCAMLDEP kernel/entries.mli OCAMLDEP kernel/declarations.mli OCAMLDEP kernel/csymtable.mli OCAMLDEP kernel/cooking.mli OCAMLDEP kernel/conv_oracle.mli OCAMLDEP kernel/closure.mli OCAMLDEP kernel/cemitcodes.mli OCAMLDEP kernel/cbytegen.mli OCAMLDEP kernel/cbytecodes.mli OCAMLDEP interp/topconstr.mli OCAMLDEP interp/syntax_def.mli OCAMLDEP interp/smartlocate.mli OCAMLDEP interp/reserve.mli OCAMLDEP interp/ppextend.mli OCAMLDEP interp/notation.mli OCAMLDEP interp/modintern.mli OCAMLDEP interp/implicit_quantifiers.mli OCAMLDEP interp/genarg.mli OCAMLDEP interp/dumpglob.mli OCAMLDEP interp/coqlib.mli OCAMLDEP interp/constrintern.mli OCAMLDEP interp/constrextern.mli OCAMLDEP ide/utils/okey.mli OCAMLDEP ide/utils/configwin.mli OCAMLDEP ide/utils/config_file.mli OCAMLDEP ide/undo_lablgtk_lt26.mli OCAMLDEP ide/undo_lablgtk_ge26.mli OCAMLDEP ide/undo_lablgtk_ge212.mli OCAMLDEP ide/undo.mli OCAMLDEP ide/preferences.mli OCAMLDEP ide/ideutils.mli OCAMLDEP ide/coqide.mli OCAMLDEP ide/coq_tactics.mli OCAMLDEP ide/coq.mli OCAMLDEP ide/command_windows.mli OCAMLDEP config/coq_config.mli OCAMLDEP checker/typeops.mli OCAMLDEP checker/type_errors.mli OCAMLDEP checker/term.mli OCAMLDEP checker/subtyping.mli OCAMLDEP checker/safe_typing.mli OCAMLDEP checker/reduction.mli OCAMLDEP checker/modops.mli OCAMLDEP checker/inductive.mli OCAMLDEP checker/indtypes.mli OCAMLDEP checker/environ.mli OCAMLDEP checker/declarations.mli OCAMLDEP checker/closure.mli OCAMLDEP checker/check_stat.mli OCAMLDEP kernel/copcodes.ml OCAMLDEP scripts/tolink.ml OCAMLDEP ide/config_parser.ml OCAMLDEP dev/ocamlweb-doc/syntax.ml OCAMLDEP tools/gallina_lexer.ml OCAMLDEP tools/coqwc.ml OCAMLDEP tools/coqdoc/cpretty.ml OCAMLDEP tools/coqdep_lexer.ml OCAMLDEP plugins/dp/dp_zenon.ml OCAMLDEP ide/utf8_convert.ml OCAMLDEP ide/highlight.ml OCAMLDEP ide/coq_lex.ml OCAMLDEP ide/config_lexer.ml OCAMLDEP dev/ocamlweb-doc/lex.ml OCAMLDEP toplevel/vernacinterp.ml OCAMLDEP toplevel/vernacexpr.ml OCAMLDEP toplevel/vernacentries.ml OCAMLDEP toplevel/vernac.ml OCAMLDEP toplevel/usage.ml OCAMLDEP toplevel/toplevel.ml OCAMLDEP toplevel/search.ml OCAMLDEP toplevel/record.ml OCAMLDEP toplevel/metasyntax.ml OCAMLDEP toplevel/libtypes.ml OCAMLDEP toplevel/lemmas.ml OCAMLDEP toplevel/indschemes.ml OCAMLDEP toplevel/ind_tables.ml OCAMLDEP toplevel/himsg.ml OCAMLDEP toplevel/discharge.ml OCAMLDEP toplevel/coqtop.ml OCAMLDEP toplevel/coqinit.ml OCAMLDEP toplevel/command.ml OCAMLDEP toplevel/classes.ml OCAMLDEP toplevel/class.ml OCAMLDEP toplevel/cerrors.ml OCAMLDEP toplevel/autoinstance.ml OCAMLDEP toplevel/auto_ind_decl.ml OCAMLDEP tools/mkwinapp.ml OCAMLDEP tools/gallina.ml OCAMLDEP tools/coqdoc/tokens.ml OCAMLDEP tools/coqdoc/output.ml OCAMLDEP tools/coqdoc/main.ml OCAMLDEP tools/coqdoc/index.ml OCAMLDEP tools/coqdoc/cdglobals.ml OCAMLDEP tools/coqdoc/alpha.ml OCAMLDEP tools/coqdep_common.ml OCAMLDEP tools/coqdep_boot.ml OCAMLDEP tools/coqdep.ml OCAMLDEP theories/Numbers/Natural/BigN/NMake_gen.ml OCAMLDEP tactics/termdn.ml OCAMLDEP tactics/tactics.ml OCAMLDEP tactics/tacticals.ml OCAMLDEP tactics/tactic_option.ml OCAMLDEP tactics/tacinterp.ml OCAMLDEP tactics/refine.ml OCAMLDEP tactics/nbtermdn.ml OCAMLDEP tactics/leminv.ml OCAMLDEP tactics/inv.ml OCAMLDEP tactics/hiddentac.ml OCAMLDEP tactics/evar_tactics.ml OCAMLDEP tactics/equality.ml OCAMLDEP tactics/eqschemes.ml OCAMLDEP tactics/elimschemes.ml OCAMLDEP tactics/elim.ml OCAMLDEP tactics/dn.ml OCAMLDEP tactics/dhyp.ml OCAMLDEP tactics/decl_proof_instr.ml OCAMLDEP tactics/decl_interp.ml OCAMLDEP tactics/contradiction.ml OCAMLDEP tactics/btermdn.ml OCAMLDEP tactics/autorewrite.ml OCAMLDEP tactics/auto.ml OCAMLDEP scripts/coqmktop.ml OCAMLDEP scripts/coqc.ml OCAMLDEP proofs/tactic_debug.ml OCAMLDEP proofs/tacmach.ml OCAMLDEP proofs/tacexpr.ml OCAMLDEP proofs/refiner.ml OCAMLDEP proofs/redexpr.ml OCAMLDEP proofs/proof_type.ml OCAMLDEP proofs/proof_trees.ml OCAMLDEP proofs/pfedit.ml OCAMLDEP proofs/logic.ml OCAMLDEP proofs/evar_refiner.ml OCAMLDEP proofs/decl_mode.ml OCAMLDEP proofs/clenvtac.ml OCAMLDEP pretyping/vnorm.ml OCAMLDEP pretyping/unification.ml OCAMLDEP pretyping/typing.ml OCAMLDEP pretyping/typeclasses_errors.ml OCAMLDEP pretyping/typeclasses.ml OCAMLDEP pretyping/termops.ml OCAMLDEP pretyping/term_dnet.ml OCAMLDEP pretyping/tacred.ml OCAMLDEP pretyping/retyping.ml OCAMLDEP pretyping/reductionops.ml OCAMLDEP pretyping/recordops.ml OCAMLDEP pretyping/rawterm.ml OCAMLDEP pretyping/pretyping.ml OCAMLDEP pretyping/pretype_errors.ml OCAMLDEP pretyping/pattern.ml OCAMLDEP pretyping/namegen.ml OCAMLDEP pretyping/matching.ml OCAMLDEP pretyping/inductiveops.ml OCAMLDEP pretyping/indrec.ml OCAMLDEP pretyping/evd.ml OCAMLDEP pretyping/evarutil.ml OCAMLDEP pretyping/evarconv.ml OCAMLDEP pretyping/detyping.ml OCAMLDEP pretyping/coercion.ml OCAMLDEP pretyping/clenv.ml OCAMLDEP pretyping/classops.ml OCAMLDEP pretyping/cbv.ml OCAMLDEP pretyping/cases.ml OCAMLDEP plugins/xml/xmlcommand.ml OCAMLDEP plugins/xml/unshare.ml OCAMLDEP plugins/xml/proof2aproof.ml OCAMLDEP plugins/xml/doubleTypeInference.ml OCAMLDEP plugins/xml/cic2Xml.ml OCAMLDEP plugins/xml/cic2acic.ml OCAMLDEP plugins/xml/acic.ml OCAMLDEP plugins/syntax/z_syntax.ml OCAMLDEP plugins/syntax/string_syntax.ml OCAMLDEP plugins/syntax/r_syntax.ml OCAMLDEP plugins/syntax/numbers_syntax.ml OCAMLDEP plugins/syntax/nat_syntax.ml OCAMLDEP plugins/syntax/ascii_syntax.ml OCAMLDEP plugins/subtac/subtac_utils.ml OCAMLDEP plugins/subtac/subtac_pretyping_F.ml OCAMLDEP plugins/subtac/subtac_pretyping.ml OCAMLDEP plugins/subtac/subtac_obligations.ml OCAMLDEP plugins/subtac/subtac_errors.ml OCAMLDEP plugins/subtac/subtac_command.ml OCAMLDEP plugins/subtac/subtac_coercion.ml OCAMLDEP plugins/subtac/subtac_classes.ml OCAMLDEP plugins/subtac/subtac_cases.ml OCAMLDEP plugins/subtac/subtac.ml OCAMLDEP plugins/subtac/eterm.ml OCAMLDEP plugins/rtauto/refl_tauto.ml OCAMLDEP plugins/rtauto/proof_search.ml OCAMLDEP plugins/romega/refl_omega.ml OCAMLDEP plugins/romega/const_omega.ml OCAMLDEP plugins/ring/ring.ml OCAMLDEP plugins/quote/quote.ml OCAMLDEP plugins/omega/omega.ml OCAMLDEP plugins/omega/coq_omega.ml OCAMLDEP plugins/nsatz/utile.ml OCAMLDEP plugins/nsatz/polynom.ml OCAMLDEP plugins/nsatz/ideal.ml OCAMLDEP plugins/micromega/sos_types.ml OCAMLDEP plugins/micromega/sos_lib.ml OCAMLDEP plugins/micromega/sos.ml OCAMLDEP plugins/micromega/persistent_cache.ml OCAMLDEP plugins/micromega/mutils.ml OCAMLDEP plugins/micromega/micromega.ml OCAMLDEP plugins/micromega/mfourier.ml OCAMLDEP plugins/micromega/csdpcert.ml OCAMLDEP plugins/micromega/coq_micromega.ml OCAMLDEP plugins/micromega/certificate.ml OCAMLDEP plugins/funind/recdef.ml OCAMLDEP plugins/funind/rawtermops.ml OCAMLDEP plugins/funind/rawterm_to_relation.ml OCAMLDEP plugins/funind/merge.ml OCAMLDEP plugins/funind/invfun.ml OCAMLDEP plugins/funind/indfun_common.ml OCAMLDEP plugins/funind/indfun.ml OCAMLDEP plugins/funind/functional_principles_types.ml OCAMLDEP plugins/funind/functional_principles_proofs.ml OCAMLDEP plugins/fourier/fourierR.ml OCAMLDEP plugins/fourier/fourier.ml OCAMLDEP plugins/firstorder/unify.ml OCAMLDEP plugins/firstorder/sequent.ml OCAMLDEP plugins/firstorder/rules.ml OCAMLDEP plugins/firstorder/instances.ml OCAMLDEP plugins/firstorder/ground.ml OCAMLDEP plugins/firstorder/formula.ml OCAMLDEP plugins/extraction/table.ml OCAMLDEP plugins/extraction/scheme.ml OCAMLDEP plugins/extraction/ocaml.ml OCAMLDEP plugins/extraction/modutil.ml OCAMLDEP plugins/extraction/mlutil.ml OCAMLDEP plugins/extraction/haskell.ml OCAMLDEP plugins/extraction/extraction.ml OCAMLDEP plugins/extraction/extract_env.ml OCAMLDEP plugins/extraction/common.ml OCAMLDEP plugins/extraction/big.ml OCAMLDEP plugins/dp/dp_why.ml OCAMLDEP plugins/dp/dp.ml OCAMLDEP plugins/cc/cctac.ml OCAMLDEP plugins/cc/ccproof.ml OCAMLDEP plugins/cc/ccalgo.ml OCAMLDEP parsing/tactic_printer.ml OCAMLDEP parsing/printmod.ml OCAMLDEP parsing/printer.ml OCAMLDEP parsing/prettyp.ml OCAMLDEP parsing/ppvernac.ml OCAMLDEP parsing/pptactic.ml OCAMLDEP parsing/ppdecl_proof.ml OCAMLDEP parsing/ppconstr.ml OCAMLDEP parsing/extrawit.ml OCAMLDEP parsing/extend.ml OCAMLDEP parsing/egrammar.ml OCAMLDEP myocamlbuild.ml OCAMLDEP library/summary.ml OCAMLDEP library/states.ml OCAMLDEP library/nametab.ml OCAMLDEP library/nameops.ml OCAMLDEP library/library.ml OCAMLDEP library/libobject.ml OCAMLDEP library/libnames.ml OCAMLDEP library/lib.ml OCAMLDEP library/impargs.ml OCAMLDEP library/heads.ml OCAMLDEP library/goptions.ml OCAMLDEP library/global.ml OCAMLDEP library/dischargedhypsmap.ml OCAMLDEP library/decls.ml OCAMLDEP library/declaremods.ml OCAMLDEP library/declare.ml OCAMLDEP library/decl_kinds.ml OCAMLDEP library/assumptions.ml OCAMLDEP lib/util.ml OCAMLDEP lib/unicodetable.ml OCAMLDEP lib/tries.ml OCAMLDEP lib/tlm.ml OCAMLDEP lib/system.ml OCAMLDEP lib/segmenttree.ml OCAMLDEP lib/rtree.ml OCAMLDEP lib/profile.ml OCAMLDEP lib/predicate.ml OCAMLDEP lib/pp_control.ml OCAMLDEP lib/option.ml OCAMLDEP lib/heap.ml OCAMLDEP lib/hashcons.ml OCAMLDEP lib/gset.ml OCAMLDEP lib/gmapl.ml OCAMLDEP lib/gmap.ml OCAMLDEP lib/fset.ml OCAMLDEP lib/fmap.ml OCAMLDEP lib/flags.ml OCAMLDEP lib/explore.ml OCAMLDEP lib/envars.ml OCAMLDEP lib/edit.ml OCAMLDEP lib/dyn.ml OCAMLDEP lib/dnet.ml OCAMLDEP lib/bstack.ml OCAMLDEP lib/bigint.ml OCAMLDEP kernel/vm.ml OCAMLDEP kernel/vconv.ml OCAMLDEP kernel/univ.ml OCAMLDEP kernel/typeops.ml OCAMLDEP kernel/type_errors.ml OCAMLDEP kernel/term_typing.ml OCAMLDEP kernel/term.ml OCAMLDEP kernel/subtyping.ml OCAMLDEP kernel/sign.ml OCAMLDEP kernel/safe_typing.ml OCAMLDEP kernel/retroknowledge.ml OCAMLDEP kernel/reduction.ml OCAMLDEP kernel/pre_env.ml OCAMLDEP kernel/names.ml OCAMLDEP kernel/modops.ml OCAMLDEP kernel/mod_typing.ml OCAMLDEP kernel/mod_subst.ml OCAMLDEP kernel/inductive.ml OCAMLDEP kernel/indtypes.ml OCAMLDEP kernel/esubst.ml OCAMLDEP kernel/environ.ml OCAMLDEP kernel/entries.ml OCAMLDEP kernel/declarations.ml OCAMLDEP kernel/csymtable.ml OCAMLDEP kernel/cooking.ml OCAMLDEP kernel/conv_oracle.ml OCAMLDEP kernel/closure.ml OCAMLDEP kernel/cemitcodes.ml OCAMLDEP kernel/cbytegen.ml OCAMLDEP kernel/cbytecodes.ml OCAMLDEP interp/topconstr.ml OCAMLDEP interp/syntax_def.ml OCAMLDEP interp/smartlocate.ml OCAMLDEP interp/reserve.ml OCAMLDEP interp/ppextend.ml OCAMLDEP interp/notation.ml OCAMLDEP interp/modintern.ml OCAMLDEP interp/implicit_quantifiers.ml OCAMLDEP interp/genarg.ml OCAMLDEP interp/dumpglob.ml OCAMLDEP interp/coqlib.ml OCAMLDEP interp/constrintern.ml OCAMLDEP interp/constrextern.ml OCAMLDEP ide/utils/okey.ml OCAMLDEP ide/utils/editable_cells.ml OCAMLDEP ide/utils/configwin_types.ml OCAMLDEP ide/utils/configwin_messages.ml OCAMLDEP ide/utils/configwin_keys.ml OCAMLDEP ide/utils/configwin_ihm.ml OCAMLDEP ide/utils/configwin.ml OCAMLDEP ide/utils/config_file.ml OCAMLDEP ide/undo.ml OCAMLDEP ide/typed_notebook.ml OCAMLDEP ide/tags.ml OCAMLDEP ide/preferences.ml OCAMLDEP ide/ideutils.ml OCAMLDEP ide/gtk_parsing.ml OCAMLDEP ide/coqide.ml OCAMLDEP ide/coq_tactics.ml OCAMLDEP ide/coq_commands.ml OCAMLDEP ide/coq.ml OCAMLDEP ide/command_windows.ml OCAMLDEP dev/vm_printers.ml OCAMLDEP dev/top_printers.ml OCAMLDEP dev/ocamlweb-doc/parse.ml OCAMLDEP dev/ocamlweb-doc/ast.ml OCAMLDEP dev/db_printers.ml OCAMLDEP config/coq_config.ml OCAMLDEP checker/validate.ml OCAMLDEP checker/typeops.ml OCAMLDEP checker/type_errors.ml OCAMLDEP checker/term.ml OCAMLDEP checker/subtyping.ml OCAMLDEP checker/safe_typing.ml OCAMLDEP checker/reduction.ml OCAMLDEP checker/modops.ml OCAMLDEP checker/mod_checking.ml OCAMLDEP checker/main.ml OCAMLDEP checker/inductive.ml OCAMLDEP checker/indtypes.ml OCAMLDEP checker/environ.ml OCAMLDEP checker/declarations.ml OCAMLDEP checker/closure.ml OCAMLDEP checker/checker.ml OCAMLDEP checker/check_stat.ml OCAMLDEP checker/check.ml CAMLP4DEPS toplevel/whelp.ml4 CAMLP4DEPS toplevel/mltop.ml4 CAMLP4DEPS tools/coq_tex.ml4 CAMLP4DEPS tools/coq_makefile.ml4 CAMLP4DEPS tactics/tauto.ml4 CAMLP4DEPS tactics/rewrite.ml4 CAMLP4DEPS tactics/hipattern.ml4 CAMLP4DEPS tactics/extratactics.ml4 CAMLP4DEPS tactics/extraargs.ml4 CAMLP4DEPS tactics/eqdecide.ml4 CAMLP4DEPS tactics/eauto.ml4 CAMLP4DEPS tactics/class_tactics.ml4 CAMLP4DEPS plugins/xml/xmlentries.ml4 CAMLP4DEPS plugins/xml/xml.ml4 CAMLP4DEPS plugins/xml/proofTree2Xml.ml4 CAMLP4DEPS plugins/xml/dumptree.ml4 CAMLP4DEPS plugins/xml/acic2Xml.ml4 CAMLP4DEPS plugins/subtac/g_subtac.ml4 CAMLP4DEPS plugins/setoid_ring/newring.ml4 CAMLP4DEPS plugins/rtauto/g_rtauto.ml4 CAMLP4DEPS plugins/romega/g_romega.ml4 CAMLP4DEPS plugins/ring/g_ring.ml4 CAMLP4DEPS plugins/quote/g_quote.ml4 CAMLP4DEPS plugins/omega/g_omega.ml4 CAMLP4DEPS plugins/nsatz/nsatz.ml4 CAMLP4DEPS plugins/micromega/g_micromega.ml4 CAMLP4DEPS plugins/funind/g_indfun.ml4 CAMLP4DEPS plugins/fourier/g_fourier.ml4 CAMLP4DEPS plugins/firstorder/g_ground.ml4 CAMLP4DEPS plugins/field/field.ml4 CAMLP4DEPS plugins/extraction/g_extraction.ml4 CAMLP4DEPS plugins/dp/g_dp.ml4 CAMLP4DEPS plugins/cc/g_congruence.ml4 CAMLP4DEPS parsing/g_xml.ml4 CAMLP4DEPS parsing/g_vernac.ml4 CAMLP4DEPS parsing/g_proofs.ml4 CAMLP4DEPS parsing/g_decl_mode.ml4 CAMLP4DEPS lib/refutpat.ml4 CCDEP kernel/byterun/coq_values.c CCDEP kernel/byterun/coq_memory.c CCDEP kernel/byterun/coq_interp.c CCDEP kernel/byterun/coq_fix_code.c OCAMLDEP4 parsing/q_constr.ml4 OCAMLDEP4 parsing/q_coqast.ml4 OCAMLDEP4 parsing/lexer.ml4 OCAMLDEP4 parsing/g_constr.ml4 clang: warning: unknown argument: '-fno-defer-pop' [-Wunused-command-line-argument-hard-error-in-future] clang: note: this will be a hard error (cannot be downgraded to a warning) in the future clang: warning: unknown argument: '-fno-defer-pop' [-Wunused-command-line-argument-hard-error-in-future] clang: note: this will be a hard error (cannot be downgraded to a warning) in the future clang: warning: argument unused during compilation: '-fno-defer-pop' clang: warning: argument unused during compilation: '-fno-defer-pop' clang: warning: unknown argument: '-fno-defer-pop' [-Wunused-command-line-argument-hard-error-in-future] clang: note: this will be a hard error (cannot be downgraded to a warning) in the future clang: warning: argument unused during compilation: '-fno-defer-pop' clang: warning: unknown argument: '-fno-defer-pop' [-Wunused-command-line-argument-hard-error-in-future] clang: note: this will be a hard error (cannot be downgraded to a warning) in the future clang: warning: argument unused during compilation: '-fno-defer-pop' OCAMLDEP4 parsing/g_ltac.ml4 OCAMLDEP4 parsing/g_tactic.ml4 OCAMLDEP4 parsing/g_prim.ml4 OCAMLDEP4 parsing/vernacextend.ml4 File "parsing/q_constr.ml4", line 30, characters 2-8: Parse error: Deprecated syntax, the grammar module is expected OCAMLDEP4 parsing/tacextend.ml4 File "parsing/g_ltac.ml4", line 31, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/g_prim.ml4", line 36, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 parsing/argextend.ml4 OCAMLDEP4 parsing/pcoq.ml4 File "parsing/g_constr.ml4", line 126, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/vernacextend.ml4", line 34, characters 8-16: While finding quotation "vala" in a position of "expr": Available quotation expanders are: direction_flag (in a position of str_item) direction_flag (in a position of patt) direction_flag (in a position of expr) override_flag (in a position of str_item) override_flag (in a position of patt) override_flag (in a position of expr) virtual_flag (in a position of str_item) virtual_flag (in a position of patt) virtual_flag (in a position of expr) mutable_flag (in a position of str_item) mutable_flag (in a position of patt) mutable_flag (in a position of expr) row_var_flag (in a position of str_item) row_var_flag (in a position of patt) row_var_flag (in a position of expr) private_flag (in a position of str_item) private_flag (in a position of patt) private_flag (in a position of expr) rec_flag (in a position of str_item) rec_flag (in a position of patt) rec_flag (in a position of expr) ident (in a position of str_item) ident (in a position of patt) ident (in a position of expr) module_binding (in a position of str_item) module_binding (in a position of patt) module_binding (in a position of expr) match_case (in a position of str_item) match_case (in a position of patt) match_case (in a position of expr) rec_binding (in a position of str_item) rec_binding (in a position of patt) rec_binding (in a position of expr) binding (in a position of str_item) binding (in a position of patt) binding (in a position of expr) with_constr (in a position of str_item) with_constr (in a position of patt) with_constr (in a position of expr) class_str_item (in a position of str_item) class_str_item (in a position of patt) class_str_item (in a position of expr) class_sig_item (in a position of str_item) class_sig_item (in a position of patt) class_sig_item (in a position of expr) class_expr (in a position of str_item) class_expr (in a position of patt) class_expr (in a position of expr) class_type (in a position of str_item) class_type (in a position of patt) class_type (in a position of expr) module_expr (in a position of str_item) module_expr (in a position of patt) module_expr (in a position of expr) module_type (in a position of str_item) module_type (in a position of patt) module_type (in a position of expr) expr (in a position of str_item) expr (in a position of patt) expr (in a position of expr) patt (in a position of str_item) patt (in a position of patt) patt (in a position of expr) ctyp (in a position of str_item) ctyp (in a position of patt) ctyp (in a position of expr) str_item (in a position of str_item) str_item (in a position of patt) str_item (in a position of expr) sig_item (in a position of str_item) sig_item (in a position of patt) sig_item (in a position of expr) Camlp4: Uncaught exception: Not_found OCAMLDEP4 parsing/q_util.ml4 OCAMLDEP4 lib/pp.ml4 File "parsing/tacextend.ml4", line 58, characters 8-18: While finding quotation "vala" in a position of "expr": Available quotation expanders are: direction_flag (in a position of str_item) direction_flag (in a position of patt) direction_flag (in a position of expr) override_flag (in a position of str_item) override_flag (in a position of patt) override_flag (in a position of expr) virtual_flag (in a position of str_item) virtual_flag (in a position of patt) virtual_flag (in a position of expr) mutable_flag (in a position of str_item) mutable_flag (in a position of patt) mutable_flag (in a position of expr) row_var_flag (in a position of str_item) row_var_flag (in a position of patt) row_var_flag (in a position of expr) private_flag (in a position of str_item) private_flag (in a position of patt) private_flag (in a position of expr) rec_flag (in a position of str_item) rec_flag (in a position of patt) rec_flag (in a position of expr) ident (in a position of str_item) ident (in a position of patt) ident (in a position of expr) module_binding (in a position of str_item) module_binding (in a position of patt) module_binding (in a position of expr) match_case (in a position of str_item) match_case (in a position of patt) match_case (in a position of expr) rec_binding (in a position of str_item) rec_binding (in a position of patt) rec_binding (in a position of expr) binding (in a position of str_item) binding (in a position of patt) binding (in a position of expr) with_constr (in a position of str_item) with_constr (in a position of patt) with_constr (in a position of expr) class_str_item (in a position of str_item) class_str_item (in a position of patt) class_str_item (in a position of expr) class_sig_item (in a position of str_item) class_sig_item (in a position of patt) class_sig_item (in a position of expr) class_expr (in a position of str_item) class_expr (in a position of patt) class_expr (in a position of expr) class_type (in a position of str_item) class_type (in a position of patt) class_type (in a position of expr) module_expr (in a position of str_item) module_expr (in a position of patt) module_expr (in a position of expr) module_type (in a position of str_item) module_type (in a position of patt) module_type (in a position of expr) expr (in a position of str_item) expr (in a position of patt) expr (in a position of expr) patt (in a position of str_item) patt (in a position of patt) patt (in a position of expr) ctyp (in a position of str_item) ctyp (in a position of patt) ctyp (in a position of expr) str_item (in a position of str_item) str_item (in a position of patt) str_item (in a position of expr) sig_item (in a position of str_item) sig_item (in a position of patt) sig_item (in a position of expr) Camlp4: Uncaught exception: Not_found OCAMLDEP4 lib/compat.ml4 File "parsing/q_util.ml4", line 31, characters 38-55: While expanding quotation "patt" in a position of "expr": Parse error: EOI expected after [quotation of pattern] (in [quotation of pattern]) File "parsing/g_tactic.ml4", line 219, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/pcoq.ml4", line 186, characters 2-9: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/argextend.ml4", line 153, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) rm tactics/class_tactics.ml parsing/q_coqast.ml plugins/micromega/g_micromega.ml plugins/field/field.ml toplevel/whelp.ml plugins/firstorder/g_ground.ml plugins/xml/xmlentries.ml lib/refutpat.ml tactics/eauto.ml parsing/g_decl_mode.ml lib/compat.ml plugins/extraction/g_extraction.ml tactics/tauto.ml tactics/rewrite.ml plugins/romega/g_romega.ml tactics/hipattern.ml plugins/fourier/g_fourier.ml parsing/lexer.ml parsing/g_vernac.ml plugins/funind/g_indfun.ml toplevel/mltop.ml plugins/xml/xml.ml plugins/xml/acic2Xml.ml plugins/ring/g_ring.ml plugins/quote/g_quote.ml plugins/rtauto/g_rtauto.ml lib/pp.ml plugins/dp/g_dp.ml plugins/omega/g_omega.ml plugins/xml/dumptree.ml tactics/extraargs.ml tactics/extratactics.ml plugins/xml/proofTree2Xml.ml parsing/g_proofs.ml plugins/setoid_ring/newring.ml plugins/cc/g_congruence.ml parsing/g_xml.ml plugins/nsatz/nsatz.ml plugins/subtac/g_subtac.ml tools/coq_makefile.ml tactics/eqdecide.ml tools/coq_tex.ml TOUCH lib/pp.ml TOUCH lib/compat.ml TOUCH lib/refutpat.ml TOUCH parsing/argextend.ml TOUCH parsing/g_constr.ml TOUCH parsing/g_decl_mode.ml TOUCH parsing/g_ltac.ml TOUCH parsing/g_prim.ml TOUCH parsing/g_proofs.ml TOUCH parsing/g_tactic.ml TOUCH parsing/g_vernac.ml TOUCH parsing/g_xml.ml TOUCH parsing/lexer.ml TOUCH parsing/pcoq.ml TOUCH parsing/q_constr.ml TOUCH parsing/q_coqast.ml TOUCH parsing/q_util.ml TOUCH parsing/tacextend.ml TOUCH parsing/vernacextend.ml TOUCH plugins/cc/g_congruence.ml TOUCH plugins/dp/g_dp.ml TOUCH plugins/extraction/g_extraction.ml TOUCH plugins/field/field.ml TOUCH plugins/firstorder/g_ground.ml TOUCH plugins/fourier/g_fourier.ml TOUCH plugins/funind/g_indfun.ml TOUCH plugins/micromega/g_micromega.ml TOUCH plugins/nsatz/nsatz.ml TOUCH plugins/omega/g_omega.ml TOUCH plugins/quote/g_quote.ml TOUCH plugins/ring/g_ring.ml TOUCH plugins/romega/g_romega.ml TOUCH plugins/rtauto/g_rtauto.ml TOUCH plugins/setoid_ring/newring.ml TOUCH plugins/subtac/g_subtac.ml TOUCH plugins/xml/acic2Xml.ml TOUCH plugins/xml/dumptree.ml TOUCH plugins/xml/proofTree2Xml.ml TOUCH plugins/xml/xml.ml TOUCH plugins/xml/xmlentries.ml TOUCH tactics/class_tactics.ml TOUCH tactics/eauto.ml TOUCH tactics/eqdecide.ml TOUCH tactics/extraargs.ml TOUCH tactics/extratactics.ml TOUCH tactics/hipattern.ml TOUCH tactics/rewrite.ml TOUCH tactics/tauto.ml TOUCH tools/coq_makefile.ml TOUCH tools/coq_tex.ml TOUCH toplevel/mltop.ml TOUCH toplevel/whelp.ml OCAMLDEP4 parsing/q_constr.ml4 OCAMLDEP4 parsing/g_constr.ml4 OCAMLDEP4 parsing/g_ltac.ml4 OCAMLDEP4 parsing/g_tactic.ml4 OCAMLDEP4 parsing/g_prim.ml4 OCAMLDEP4 parsing/vernacextend.ml4 OCAMLDEP4 parsing/tacextend.ml4 OCAMLDEP4 parsing/argextend.ml4 File "parsing/g_ltac.ml4", line 31, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/g_prim.ml4", line 36, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 parsing/pcoq.ml4 File "parsing/q_constr.ml4", line 30, characters 2-8: Parse error: Deprecated syntax, the grammar module is expected File "parsing/vernacextend.ml4", line 34, characters 8-16: OCAMLDEP4 parsing/q_util.ml4 While finding quotation "vala" in a position of "expr": Available quotation expanders are: direction_flag (in a position of str_item) direction_flag (in a position of patt) direction_flag (in a position of expr) override_flag (in a position of str_item) override_flag (in a position of patt) override_flag (in a position of expr) virtual_flag (in a position of str_item) virtual_flag (in a position of patt) virtual_flag (in a position of expr) mutable_flag (in a position of str_item) mutable_flag (in a position of patt) mutable_flag (in a position of expr) row_var_flag (in a position of str_item) row_var_flag (in a position of patt) row_var_flag (in a position of expr) private_flag (in a position of str_item) private_flag (in a position of patt) private_flag (in a position of expr) rec_flag (in a position of str_item) rec_flag (in a position of patt) rec_flag (in a position of expr) ident (in a position of str_item) ident (in a position of patt) ident (in a position of expr) module_binding (in a position of str_item) module_binding (in a position of patt) module_binding (in a position of expr) match_case (in a position of str_item) match_case (in a position of patt) match_case (in a position of expr) rec_binding (in a position of str_item) rec_binding (in a position of patt) rec_binding (in a position of expr) binding (in a position of str_item) binding (in a position of patt) binding (in a position of expr) with_constr (in a position of str_item) with_constr (in a position of patt) with_constr (in a position of expr) class_str_item (in a position of str_item) class_str_item (in a position of patt) class_str_item (in a position of expr) class_sig_item (in a position of str_item) class_sig_item (in a position of patt) class_sig_item (in a position of expr) class_expr (in a position of str_item) class_expr (in a position of patt) class_expr (in a position of expr) class_type (in a position of str_item) class_type (in a position of patt) class_type (in a position of expr) module_expr (in a position of str_item) module_expr (in a position of patt) module_expr (in a position of expr) module_type (in a position of str_item) module_type (in a position of patt) module_type (in a position of expr) expr (in a position of str_item) expr (in a position of patt) expr (in a position of expr) patt (in a position of str_item) patt (in a position of patt) patt (in a position of expr) ctyp (in a position of str_item) ctyp (in a position of patt) ctyp (in a position of expr) str_item (in a position of str_item) str_item (in a position of patt) str_item (in a position of expr) sig_item (in a position of str_item) sig_item (in a position of patt) sig_item (in a position of expr) Camlp4: Uncaught exception: Not_found File "parsing/tacextend.ml4", line 58, characters 8-18: While finding quotation "vala" in a position of "expr": Available quotation expanders are: direction_flag (in a position of str_item) direction_flag (in a position of patt) direction_flag (in a position of expr) override_flag (in a position of str_item) override_flag (in a position of patt) override_flag (in a position of expr) virtual_flag (in a position of str_item) virtual_flag (in a position of patt) virtual_flag (in a position of expr) mutable_flag (in a position of str_item) mutable_flag (in a position of patt) mutable_flag (in a position of expr) row_var_flag (in a position of str_item) row_var_flag (in a position of patt) row_var_flag (in a position of expr) private_flag (in a position of str_item) private_flag (in a position of patt) private_flag (in a position of expr) rec_flag (in a position of str_item) rec_flag (in a position of patt) rec_flag (in a position of expr) ident (in a position of str_item) ident (in a position of patt) ident (in a position of expr) module_binding (in a position of str_item) module_binding (in a position of patt) module_binding (in a position of expr) match_case (in a position of str_item) match_case (in a position of patt) match_case (in a position of expr) rec_binding (in a position of str_item) rec_binding (in a position of patt) rec_binding (in a position of expr) binding (in a position of str_item) binding (in a position of patt) binding (in a position of expr) with_constr (in a position of str_item) with_constr (in a position of patt) with_constr (in a position of expr) class_str_item (in a position of str_item) class_str_item (in a position of patt) class_str_item (in a position of expr) class_sig_item (in a position of str_item) class_sig_item (in a position of patt) class_sig_item (in a position of expr) class_expr (in a position of str_item) class_expr (in a position of patt) class_expr (in a position of expr) class_type (in a position of str_item) class_type (in a position of patt) class_type (in a position of expr) module_expr (in a position of str_item) module_expr (in a position of patt) module_expr (in a position of expr) module_type (in a position of str_item) module_type (in a position of patt) module_type (in a position of expr) expr (in a position of str_item) expr (in a position of patt) expr (in a position of expr) patt (in a position of str_item) patt (in a position of patt) patt (in a position of expr) ctyp (in a position of str_item) ctyp (in a position of patt) ctyp (in a position of expr) str_item (in a position of str_item) str_item (in a position of patt) str_item (in a position of expr) sig_item (in a position of str_item) sig_item (in a position of patt) sig_item (in a position of expr) Camlp4: Uncaught exception: Not_found File "parsing/g_constr.ml4", line 126, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/q_util.ml4", line 31, characters 38-55: While expanding quotation "patt" in a position of "expr": Parse error: EOI expected after [quotation of pattern] (in [quotation of pattern]) File "parsing/g_tactic.ml4", line 219, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/argextend.ml4", line 153, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) File "parsing/pcoq.ml4", line 186, characters 2-9: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead make[1]: *** No rule to make target `parsing/q_constr.ml4.ml.d', needed by `parsing/q_constr.cmo'. Stop. make[1]: *** Waiting for unfinished jobs.... OCAMLC -o bin/coqdep_boot File "tools/coqdep_common.ml", line 239, characters 1-3: Warning 3: deprecated feature: operator (or); you should use (||) instead File "tools/coqdep_common.ml", line 238, characters 34-36: Warning 3: deprecated feature: operator (or); you should use (||) instead File "tools/coqdep_common.ml", line 238, characters 23-25: Warning 3: deprecated feature: operator (or); you should use (||) instead File "tools/coqdep_common.ml", line 238, characters 12-14: Warning 3: deprecated feature: operator (or); you should use (||) instead File "tools/coqdep_common.ml", line 238, characters 1-3: Warning 3: deprecated feature: operator (or); you should use (||) instead File "tools/coqdep_common.ml", line 237, characters 1-3: Warning 3: deprecated feature: operator (or); you should use (||) instead File "tools/coqdep_common.ml", line 236, characters 28-30: Warning 3: deprecated feature: operator (or); you should use (||) instead File "tools/coqdep_common.ml", line 236, characters 17-19: Warning 3: deprecated feature: operator (or); you should use (||) instead rm toplevel/mltop.ml lib/refutpat.ml tactics/class_tactics.ml parsing/g_vernac.ml tools/coq_tex.ml plugins/quote/g_quote.ml parsing/q_coqast.ml plugins/romega/g_romega.ml tools/coq_makefile.ml toplevel/whelp.ml plugins/firstorder/g_ground.ml lib/compat.ml plugins/xml/dumptree.ml parsing/g_xml.ml tactics/extraargs.ml plugins/extraction/g_extraction.ml plugins/fourier/g_fourier.ml tactics/tauto.ml plugins/micromega/g_micromega.ml tactics/hipattern.ml plugins/field/field.ml plugins/dp/g_dp.ml plugins/xml/xml.ml plugins/xml/xmlentries.ml plugins/funind/g_indfun.ml plugins/ring/g_ring.ml tactics/rewrite.ml plugins/rtauto/g_rtauto.ml lib/pp.ml tactics/eauto.ml tactics/extratactics.ml parsing/g_decl_mode.ml plugins/xml/proofTree2Xml.ml parsing/lexer.ml parsing/g_proofs.ml plugins/setoid_ring/newring.ml plugins/cc/g_congruence.ml plugins/nsatz/nsatz.ml plugins/subtac/g_subtac.ml plugins/xml/acic2Xml.ml tactics/eqdecide.ml plugins/omega/g_omega.ml make: *** [stage1] Error 2 ### execution of /tmp/fink.dycuK failed, exit code 2 ### execution of /tmp/fink.HxM2j failed, exit code 2 Removing runtime build-lock... Removing build-lock package... /sw/bin/dpkg-lockwait -r fink-buildlock-coqide-8.3pl3-1 (Reading database ... 14806 files and directories currently installed.) Removing fink-buildlock-coqide-8.3pl3-1 ... Failed: phase compiling: coqide-8.3pl3-1 failed Before reporting any errors, please run "fink selfupdate" and try again. Also try using "fink configure" to set your maximum build jobs to 1 and attempt to build the package again. If you continue to have issues, please check to see if the FAQ on Fink's website solves the problem. If not, ask on one (not both, please) of these mailing lists: The Fink Users List The Fink Beginners List , with a carbon copy to the maintainer: Bruno De Fraine Note that this is preferable to emailing just the maintainer directly, since most fink package maintainers do not have access to all possible hardware and software configurations. Please try to include the complete error message in your report. This generally consists of a compiler line starting with e.g. "gcc" or "g++" followed by the actual error output from the compiler. Also include the following system information: Package manager version: 0.37.0 Distribution version: selfupdate-cvs Thu Jul 24 20:26:24 2014, 10.9, x86_64 Trees: local/main stable/main Xcode.app: 5.1.1 Xcode command-line tools: 6.0.0.0.1.1405597879 Max. Fink build jobs: 8