=> Bootstrap dependency digest>=20010302: found digest-20121220 ===> Skipping vulnerability checks. WARNING: No /var/db/pkg/pkg-vulnerabilities file found. WARNING: To fix run: `/usr/sbin/pkg_admin -K /var/db/pkg fetch-pkg-vulnerabilities'. ===> Building for coq-8.4pl1nb3 /usr/pkg/bin/gmake --warn-undefined-variable --no-builtin-rules -f Makefile.build "world" gmake[1]: Entering directory `/scratch/lang/coq/work/coq-8.4pl1' "ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > "theories/Numbers/Natural/BigN/NMake_gen.v" || (RV=$?; rm -f "theories/Numbers/Natural/BigN/NMake_gen.v"; exit ${RV}) OCAMLLEX tools/coqdep_lexer.mll OCAMLLEX lib/xml_lexer.mll 78 states, 800 transitions, table size 3668 bytes 348 states, 7127 transitions, table size 30596 bytes 3131 additional bytes used for bindings OCAMLLEX tools/gallina_lexer.mll 190 states, 498 transitions, table size 3132 bytes OCAMLLEX tools/coqwc.mll OCAMLLEX tools/coqdoc/cpretty.mll 230 states, 833 transitions, table size 4712 bytes OCAMLLEX ide/config_lexer.mll 30 states, 1657 transitions, table size 6808 bytes 6096 additional bytes used for bindings OCAMLLEX ide/coq_lex.mll 2461 states, 7373 transitions, table size 44258 bytes OCAMLLEX ide/utf8_convert.mll 15 states, 827 transitions, table size 3398 bytes ECHO... > scripts/tolink.ml 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}) 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}) ECHO... > plugins/extraction/extraction_plugin_mod.ml ECHO... > plugins/cc/cc_plugin_mod.ml ECHO... > plugins/subtac/subtac_plugin_mod.ml ECHO... > plugins/field/field_plugin_mod.ml ECHO... > plugins/firstorder/ground_plugin_mod.ml ECHO... > plugins/funind/recdef_plugin_mod.ml ECHO... > plugins/syntax/r_syntax_plugin_mod.ml ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml ECHO... > plugins/syntax/string_syntax_plugin_mod.ml ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml ECHO... > plugins/syntax/z_syntax_plugin_mod.ml ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml ECHO... > plugins/omega/omega_plugin_mod.ml ECHO... > plugins/quote/quote_plugin_mod.ml ECHO... > plugins/ring/ring_plugin_mod.ml ECHO... > plugins/nsatz/nsatz_plugin_mod.ml ECHO... > plugins/xml/xml_plugin_mod.ml ECHO... > plugins/micromega/micromega_plugin_mod.ml ECHO... > plugins/romega/romega_plugin_mod.ml ECHO... > plugins/setoid_ring/newring_plugin_mod.ml ECHO... > plugins/fourier/fourier_plugin_mod.ml ECHO... > plugins/decl_mode/decl_mode_plugin_mod.ml ECHO... > plugins/rtauto/rtauto_plugin_mod.ml CCDEP ide/ide_win32_stubs.c CCDEP kernel/byterun/coq_memory.c 454 states, 31913 transitions, table size 130376 bytes CCDEP kernel/byterun/coq_interp.c CCDEP kernel/byterun/coq_fix_code.c CCDEP kernel/byterun/coq_values.c "ocamlc" -rectypes -c tools/compat5.ml "ocamlc" -rectypes -c tools/compat5b.ml CAMLP4DEPS parsing/g_prim.ml4 CAMLP4DEPS parsing/q_util.ml4 CAMLP4DEPS parsing/g_ltac.ml4 CAMLP4DEPS parsing/q_constr.ml4 CAMLP4DEPS parsing/tacextend.ml4 CAMLP4DEPS parsing/lexer.ml4 CAMLP4DEPS parsing/g_constr.ml4 CAMLP4DEPS parsing/g_proofs.ml4 CAMLP4DEPS parsing/g_tactic.ml4 CAMLP4DEPS parsing/q_coqast.ml4 CAMLP4DEPS parsing/g_xml.ml4 CAMLP4DEPS parsing/argextend.ml4 CAMLP4DEPS parsing/pcoq.ml4 CAMLP4DEPS parsing/g_vernac.ml4 CAMLP4DEPS parsing/vernacextend.ml4 CAMLP4DEPS tactics/eauto.ml4 CAMLP4DEPS tactics/eqdecide.ml4 CAMLP4DEPS tactics/rewrite.ml4 CAMLP4DEPS tactics/extraargs.ml4 CAMLP4DEPS tactics/hipattern.ml4 CAMLP4DEPS tactics/extratactics.ml4 CAMLP4DEPS tactics/class_tactics.ml4 CAMLP4DEPS tactics/tauto.ml4 CAMLP4DEPS ide/project_file.ml4 CAMLP4O ide/coqide_main.ml4 CAMLP4DEPS toplevel/whelp.ml4 CAMLP4O toplevel/mltop.ml4 CAMLP4DEPS plugins/rtauto/g_rtauto.ml4 CAMLP4DEPS plugins/decl_mode/g_decl_mode.ml4 CAMLP4DEPS plugins/fourier/g_fourier.ml4 CAMLP4DEPS plugins/setoid_ring/newring.ml4 CAMLP4DEPS plugins/romega/g_romega.ml4 CAMLP4DEPS plugins/micromega/g_micromega.ml4 CAMLP4DEPS plugins/xml/proofTree2Xml.ml4 CAMLP4DEPS plugins/xml/acic2Xml.ml4 CAMLP4DEPS plugins/xml/xml.ml4 CAMLP4DEPS plugins/xml/xmlentries.ml4 CAMLP4DEPS plugins/xml/dumptree.ml4 CAMLP4DEPS plugins/nsatz/nsatz.ml4 CAMLP4DEPS plugins/ring/g_ring.ml4 CAMLP4DEPS plugins/quote/g_quote.ml4 CAMLP4DEPS plugins/omega/g_omega.ml4 CAMLP4DEPS plugins/funind/g_indfun.ml4 CAMLP4DEPS plugins/firstorder/g_ground.ml4 CAMLP4DEPS plugins/field/field.ml4 CAMLP4DEPS plugins/subtac/g_subtac.ml4 CAMLP4DEPS plugins/cc/g_congruence.ml4 CAMLP4DEPS plugins/extraction/g_extraction.ml4 CAMLP4DEPS lib/compat.ml4 CAMLP4DEPS lib/pp.ml4 CAMLP4DEPS ide/coqide_main.ml4 CAMLP4DEPS toplevel/mltop.ml4 OCAMLBEST -o bin/coqdep_boot OCAMLDEP toplevel/vernacinterp.mli OCAMLDEP toplevel/whelp.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/interface.mli OCAMLDEP toplevel/indschemes.mli OCAMLDEP toplevel/ind_tables.mli OCAMLDEP toplevel/ide_slave.mli OCAMLDEP toplevel/ide_intf.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/backtrack.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 tools/coqdep_lexer.mli OCAMLDEP tools/coqdep_common.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/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/proofview.mli OCAMLDEP proofs/proof_type.mli OCAMLDEP proofs/proof_global.mli OCAMLDEP proofs/proof.mli OCAMLDEP proofs/pfedit.mli OCAMLDEP proofs/logic.mli OCAMLDEP proofs/goal.mli OCAMLDEP proofs/evar_refiner.mli OCAMLDEP proofs/clenvtac.mli OCAMLDEP proofs/clenv.mli OCAMLDEP 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/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/glob_term.mli OCAMLDEP pretyping/evd.mli OCAMLDEP pretyping/evarutil.mli OCAMLDEP pretyping/evarconv.mli OCAMLDEP pretyping/detyping.mli OCAMLDEP pretyping/coercion.mli OCAMLDEP pretyping/classops.mli OCAMLDEP pretyping/cbv.mli OCAMLDEP pretyping/cases.mli OCAMLDEP pretyping/arguments_renaming.mli OCAMLDEP plugins/xml/xmlcommand.mli OCAMLDEP plugins/xml/xml.mli OCAMLDEP plugins/xml/unshare.mli OCAMLDEP plugins/subtac/subtac_utils.mli OCAMLDEP plugins/xml/doubleTypeInference.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/indfun_common.mli OCAMLDEP plugins/funind/indfun.mli OCAMLDEP plugins/funind/glob_termops.mli OCAMLDEP plugins/funind/glob_term_to_relation.mli OCAMLDEP plugins/funind/functional_principles_types.mli OCAMLDEP plugins/funind/functional_principles_proofs.mli OCAMLDEP plugins/firstorder/unify.mli OCAMLDEP plugins/firstorder/sequent.mli OCAMLDEP plugins/firstorder/rules.mli OCAMLDEP plugins/firstorder/instances.mli OCAMLDEP plugins/firstorder/ground.mli OCAMLDEP plugins/firstorder/formula.mli OCAMLDEP plugins/extraction/table.mli OCAMLDEP plugins/extraction/ocaml.mli OCAMLDEP plugins/extraction/scheme.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/decl_mode/ppdecl_proof.mli OCAMLDEP plugins/decl_mode/decl_proof_instr.mli OCAMLDEP plugins/decl_mode/decl_mode.mli OCAMLDEP plugins/decl_mode/decl_interp.mli OCAMLDEP plugins/decl_mode/decl_expr.mli OCAMLDEP plugins/cc/cctac.mli OCAMLDEP plugins/cc/ccproof.mli OCAMLDEP plugins/cc/ccalgo.mli OCAMLDEP parsing/tok.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/ppconstr.mli OCAMLDEP parsing/pcoq.mli OCAMLDEP parsing/lexer.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/goptionstyp.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/xml_utils.mli OCAMLDEP lib/xml_parser.mli OCAMLDEP lib/xml_lexer.mli OCAMLDEP lib/util.mli OCAMLDEP lib/unionfind.mli OCAMLDEP lib/tries.mli OCAMLDEP lib/system.mli OCAMLDEP lib/store.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/hashtbl_alt.mli OCAMLDEP lib/hashcons.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/errors.mli OCAMLDEP lib/envars.mli OCAMLDEP lib/dyn.mli OCAMLDEP lib/dnet.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/conv_oracle.mli OCAMLDEP kernel/cooking.mli OCAMLDEP kernel/closure.mli OCAMLDEP kernel/cbytegen.mli OCAMLDEP kernel/cemitcodes.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/tags.mli OCAMLDEP ide/preferences.mli OCAMLDEP ide/minilib.mli OCAMLDEP ide/ideutils.mli OCAMLDEP ide/coqide.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/mod_checking.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 plugins/rtauto/rtauto_plugin_mod.ml OCAMLDEP plugins/decl_mode/decl_mode_plugin_mod.ml OCAMLDEP plugins/fourier/fourier_plugin_mod.ml OCAMLDEP plugins/setoid_ring/newring_plugin_mod.ml OCAMLDEP plugins/romega/romega_plugin_mod.ml OCAMLDEP plugins/micromega/micromega_plugin_mod.ml OCAMLDEP plugins/xml/xml_plugin_mod.ml OCAMLDEP plugins/nsatz/nsatz_plugin_mod.ml OCAMLDEP plugins/ring/ring_plugin_mod.ml OCAMLDEP plugins/quote/quote_plugin_mod.ml OCAMLDEP plugins/omega/omega_plugin_mod.ml OCAMLDEP plugins/syntax/numbers_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/z_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/ascii_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/string_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/nat_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/r_syntax_plugin_mod.ml OCAMLDEP plugins/funind/recdef_plugin_mod.ml OCAMLDEP plugins/firstorder/ground_plugin_mod.ml OCAMLDEP plugins/field/field_plugin_mod.ml OCAMLDEP plugins/subtac/subtac_plugin_mod.ml OCAMLDEP plugins/cc/cc_plugin_mod.ml OCAMLDEP plugins/extraction/extraction_plugin_mod.ml CAMLP4O parsing/g_prim.ml4 CAMLP4O parsing/q_util.ml4 CAMLP4O parsing/g_ltac.ml4 CAMLP4O parsing/q_constr.ml4 CAMLP4O parsing/tacextend.ml4 CAMLP4O parsing/lexer.ml4 CAMLP4O parsing/g_constr.ml4 CAMLP4O parsing/g_proofs.ml4 CAMLP4O parsing/g_tactic.ml4 CAMLP4O parsing/q_coqast.ml4 CAMLP4O parsing/g_xml.ml4 CAMLP4O parsing/argextend.ml4 CAMLP4O parsing/pcoq.ml4 CAMLP4O parsing/g_vernac.ml4 CAMLP4O parsing/vernacextend.ml4 CAMLP4O tactics/eauto.ml4 tactics/eauto.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O tactics/eqdecide.ml4 tactics/eqdecide.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O tactics/rewrite.ml4 tactics/rewrite.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O tactics/extraargs.ml4 tactics/extraargs.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O tactics/hipattern.ml4 tactics/hipattern.ml4 : Dependency parsing/grammar.cma parsing/q_constr.cmo not ready yet CAMLP4O tactics/extratactics.ml4 tactics/extratactics.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O tactics/class_tactics.ml4 tactics/class_tactics.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O tactics/tauto.ml4 tactics/tauto.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O ide/project_file.ml4 OCAMLDEP ide/coqide_main.ml CAMLP4O toplevel/whelp.ml4 toplevel/whelp.ml4 : Dependency parsing/grammar.cma not ready yet OCAMLDEP toplevel/mltop.ml CAMLP4O plugins/rtauto/g_rtauto.ml4 CAMLP4O plugins/decl_mode/g_decl_mode.ml4 plugins/rtauto/g_rtauto.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/fourier/g_fourier.ml4 plugins/decl_mode/g_decl_mode.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/setoid_ring/newring.ml4 plugins/fourier/g_fourier.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/romega/g_romega.ml4 plugins/setoid_ring/newring.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/micromega/g_micromega.ml4 plugins/romega/g_romega.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/xml/proofTree2Xml.ml4 plugins/micromega/g_micromega.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/xml/acic2Xml.ml4 CAMLP4O plugins/xml/xml.ml4 CAMLP4O plugins/xml/xmlentries.ml4 plugins/xml/xmlentries.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/xml/dumptree.ml4 plugins/xml/dumptree.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/nsatz/nsatz.ml4 CAMLP4O plugins/ring/g_ring.ml4 plugins/nsatz/nsatz.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/quote/g_quote.ml4 plugins/ring/g_ring.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/omega/g_omega.ml4 plugins/quote/g_quote.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/funind/g_indfun.ml4 plugins/omega/g_omega.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/firstorder/g_ground.ml4 plugins/funind/g_indfun.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/field/field.ml4 plugins/firstorder/g_ground.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/subtac/g_subtac.ml4 plugins/field/field.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/cc/g_congruence.ml4 plugins/subtac/g_subtac.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O plugins/extraction/g_extraction.ml4 plugins/cc/g_congruence.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O lib/compat.ml4 plugins/extraction/g_extraction.ml4 : Dependency parsing/grammar.cma not ready yet CAMLP4O lib/pp.ml4 OCAMLDEP kernel/copcodes.ml OCAMLDEP scripts/tolink.ml OCAMLDEP ide/utf8_convert.ml OCAMLDEP ide/coq_lex.ml OCAMLDEP ide/config_lexer.ml OCAMLDEP tools/coqdep_lexer.ml OCAMLDEP tools/coqdoc/cpretty.ml OCAMLDEP tools/coqwc.ml OCAMLDEP tools/gallina_lexer.ml OCAMLDEP lib/xml_lexer.ml OCAMLDEP proofs/clenv.ml OCAMLDEP proofs/tacexpr.ml OCAMLDEP proofs/evar_refiner.ml OCAMLDEP proofs/tacmach.ml OCAMLDEP proofs/proof_global.ml OCAMLDEP proofs/clenvtac.ml OCAMLDEP proofs/logic.ml OCAMLDEP proofs/refiner.ml OCAMLDEP proofs/proof_type.ml OCAMLDEP proofs/proof.ml OCAMLDEP proofs/goal.ml OCAMLDEP proofs/proofview.ml OCAMLDEP proofs/pfedit.ml OCAMLDEP proofs/redexpr.ml OCAMLDEP proofs/tactic_debug.ml OCAMLDEP config/coq_config.ml OCAMLDEP parsing/extrawit.ml OCAMLDEP parsing/pptactic.ml OCAMLDEP parsing/printmod.ml OCAMLDEP parsing/ppconstr.ml OCAMLDEP parsing/prettyp.ml OCAMLDEP parsing/tactic_printer.ml OCAMLDEP parsing/tok.ml OCAMLDEP parsing/egrammar.ml OCAMLDEP parsing/extend.ml OCAMLDEP parsing/printer.ml OCAMLDEP parsing/ppvernac.ml OCAMLDEP interp/genarg.ml OCAMLDEP interp/syntax_def.ml OCAMLDEP interp/constrextern.ml OCAMLDEP interp/modintern.ml OCAMLDEP interp/topconstr.ml OCAMLDEP interp/notation.ml OCAMLDEP interp/constrintern.ml OCAMLDEP interp/ppextend.ml OCAMLDEP interp/smartlocate.ml OCAMLDEP interp/reserve.ml OCAMLDEP interp/dumpglob.ml OCAMLDEP interp/coqlib.ml OCAMLDEP interp/implicit_quantifiers.ml OCAMLDEP tactics/evar_tactics.ml OCAMLDEP tactics/dn.ml OCAMLDEP tactics/contradiction.ml OCAMLDEP tactics/tactics.ml OCAMLDEP tactics/leminv.ml OCAMLDEP tactics/termdn.ml OCAMLDEP tactics/tacinterp.ml OCAMLDEP tactics/elim.ml OCAMLDEP tactics/eqschemes.ml OCAMLDEP tactics/auto.ml OCAMLDEP tactics/autorewrite.ml OCAMLDEP tactics/tacticals.ml OCAMLDEP tactics/tactic_option.ml OCAMLDEP tactics/elimschemes.ml OCAMLDEP tactics/equality.ml OCAMLDEP tactics/inv.ml OCAMLDEP tactics/btermdn.ml OCAMLDEP tactics/hiddentac.ml OCAMLDEP tactics/nbtermdn.ml OCAMLDEP tactics/refine.ml OCAMLDEP myocamlbuild.ml OCAMLDEP ide/coq_commands.ml OCAMLDEP ide/undo.ml OCAMLDEP ide/coqide.ml OCAMLDEP ide/command_windows.ml OCAMLDEP ide/utils/configwin_types.ml OCAMLDEP ide/utils/config_file.ml OCAMLDEP ide/utils/configwin.ml OCAMLDEP ide/utils/configwin_ihm.ml OCAMLDEP ide/utils/configwin_keys.ml OCAMLDEP ide/utils/editable_cells.ml OCAMLDEP ide/utils/configwin_messages.ml OCAMLDEP ide/utils/okey.ml OCAMLDEP ide/minilib.ml OCAMLDEP ide/typed_notebook.ml OCAMLDEP ide/ideutils.ml OCAMLDEP ide/coq.ml OCAMLDEP ide/ideproof.ml OCAMLDEP ide/coqide_ui.ml OCAMLDEP ide/preferences.ml OCAMLDEP ide/tags.ml OCAMLDEP ide/gtk_parsing.ml OCAMLDEP toplevel/himsg.ml OCAMLDEP toplevel/search.ml OCAMLDEP toplevel/ide_slave.ml OCAMLDEP toplevel/toplevel.ml OCAMLDEP toplevel/auto_ind_decl.ml OCAMLDEP toplevel/backtrack.ml OCAMLDEP toplevel/indschemes.ml OCAMLDEP toplevel/vernac.ml OCAMLDEP toplevel/record.ml OCAMLDEP toplevel/command.ml OCAMLDEP toplevel/vernacexpr.ml OCAMLDEP toplevel/vernacentries.ml OCAMLDEP toplevel/coqinit.ml OCAMLDEP toplevel/class.ml OCAMLDEP toplevel/coqtop.ml OCAMLDEP toplevel/ind_tables.ml OCAMLDEP toplevel/usage.ml OCAMLDEP toplevel/vernacinterp.ml OCAMLDEP toplevel/autoinstance.ml OCAMLDEP toplevel/classes.ml OCAMLDEP toplevel/metasyntax.ml OCAMLDEP toplevel/libtypes.ml OCAMLDEP toplevel/discharge.ml OCAMLDEP toplevel/ide_intf.ml OCAMLDEP toplevel/cerrors.ml OCAMLDEP toplevel/lemmas.ml OCAMLDEP theories/Numbers/Natural/BigN/NMake_gen.ml OCAMLDEP plugins/rtauto/refl_tauto.ml OCAMLDEP plugins/rtauto/proof_search.ml OCAMLDEP plugins/decl_mode/ppdecl_proof.ml OCAMLDEP plugins/decl_mode/decl_mode.ml OCAMLDEP plugins/decl_mode/decl_interp.ml OCAMLDEP plugins/decl_mode/decl_proof_instr.ml OCAMLDEP plugins/fourier/fourierR.ml OCAMLDEP plugins/fourier/fourier.ml OCAMLDEP plugins/romega/refl_omega.ml OCAMLDEP plugins/romega/const_omega.ml OCAMLDEP plugins/micromega/csdpcert.ml OCAMLDEP plugins/micromega/sos.ml OCAMLDEP plugins/micromega/micromega.ml OCAMLDEP plugins/micromega/coq_micromega.ml OCAMLDEP plugins/micromega/sos_lib.ml OCAMLDEP plugins/micromega/sos_types.ml OCAMLDEP plugins/micromega/mfourier.ml OCAMLDEP plugins/micromega/polynomial.ml OCAMLDEP plugins/micromega/certificate.ml OCAMLDEP plugins/micromega/persistent_cache.ml OCAMLDEP plugins/micromega/mutils.ml OCAMLDEP plugins/xml/unshare.ml OCAMLDEP plugins/xml/cic2Xml.ml OCAMLDEP plugins/xml/cic2acic.ml OCAMLDEP plugins/xml/acic.ml OCAMLDEP plugins/xml/xmlcommand.ml OCAMLDEP plugins/xml/proof2aproof.ml OCAMLDEP plugins/xml/doubleTypeInference.ml OCAMLDEP plugins/nsatz/utile.ml OCAMLDEP plugins/nsatz/ideal.ml OCAMLDEP plugins/nsatz/polynom.ml OCAMLDEP plugins/ring/ring.ml OCAMLDEP plugins/quote/quote.ml OCAMLDEP plugins/omega/omega.ml OCAMLDEP plugins/omega/coq_omega.ml OCAMLDEP plugins/syntax/r_syntax.ml OCAMLDEP plugins/syntax/z_syntax.ml OCAMLDEP plugins/syntax/ascii_syntax.ml OCAMLDEP plugins/syntax/numbers_syntax.ml OCAMLDEP plugins/syntax/string_syntax.ml OCAMLDEP plugins/syntax/nat_syntax.ml OCAMLDEP plugins/funind/merge.ml OCAMLDEP plugins/funind/invfun.ml OCAMLDEP plugins/funind/glob_termops.ml OCAMLDEP plugins/funind/recdef.ml OCAMLDEP plugins/funind/functional_principles_proofs.ml OCAMLDEP plugins/funind/indfun.ml OCAMLDEP plugins/funind/indfun_common.ml OCAMLDEP plugins/funind/glob_term_to_relation.ml OCAMLDEP plugins/firstorder/instances.ml OCAMLDEP plugins/funind/functional_principles_types.ml OCAMLDEP plugins/firstorder/formula.ml OCAMLDEP plugins/firstorder/sequent.ml OCAMLDEP plugins/firstorder/ground.ml OCAMLDEP plugins/firstorder/unify.ml OCAMLDEP plugins/firstorder/rules.ml OCAMLDEP plugins/subtac/subtac_coercion.ml OCAMLDEP plugins/subtac/subtac_utils.ml OCAMLDEP plugins/subtac/subtac_cases.ml OCAMLDEP plugins/subtac/subtac_classes.ml OCAMLDEP plugins/subtac/subtac_pretyping_F.ml OCAMLDEP plugins/subtac/subtac_pretyping.ml OCAMLDEP plugins/subtac/subtac.ml OCAMLDEP plugins/subtac/subtac_command.ml OCAMLDEP plugins/subtac/subtac_errors.ml OCAMLDEP plugins/subtac/eterm.ml OCAMLDEP plugins/subtac/subtac_obligations.ml OCAMLDEP plugins/cc/cctac.ml OCAMLDEP plugins/cc/ccproof.ml OCAMLDEP plugins/cc/ccalgo.ml OCAMLDEP plugins/extraction/mlutil.ml OCAMLDEP plugins/extraction/scheme.ml OCAMLDEP plugins/extraction/big.ml OCAMLDEP plugins/extraction/ocaml.ml OCAMLDEP plugins/extraction/common.ml OCAMLDEP plugins/extraction/extract_env.ml OCAMLDEP plugins/extraction/extraction.ml OCAMLDEP plugins/extraction/table.ml OCAMLDEP plugins/extraction/haskell.ml OCAMLDEP plugins/extraction/modutil.ml OCAMLDEP pretyping/indrec.ml OCAMLDEP pretyping/tacred.ml OCAMLDEP pretyping/coercion.ml OCAMLDEP pretyping/matching.ml OCAMLDEP pretyping/termops.ml OCAMLDEP pretyping/classops.ml OCAMLDEP pretyping/evarconv.ml OCAMLDEP pretyping/reductionops.ml OCAMLDEP pretyping/inductiveops.ml OCAMLDEP pretyping/typing.ml OCAMLDEP pretyping/unification.ml OCAMLDEP pretyping/retyping.ml OCAMLDEP pretyping/vnorm.ml OCAMLDEP pretyping/typeclasses.ml OCAMLDEP pretyping/recordops.ml OCAMLDEP pretyping/typeclasses_errors.ml OCAMLDEP pretyping/cases.ml OCAMLDEP pretyping/evarutil.ml OCAMLDEP pretyping/arguments_renaming.ml OCAMLDEP pretyping/detyping.ml OCAMLDEP pretyping/term_dnet.ml OCAMLDEP pretyping/pretyping.ml OCAMLDEP pretyping/evd.ml OCAMLDEP pretyping/pattern.ml OCAMLDEP pretyping/cbv.ml OCAMLDEP pretyping/glob_term.ml OCAMLDEP pretyping/namegen.ml OCAMLDEP pretyping/pretype_errors.ml OCAMLDEP dev/top_printers.ml OCAMLDEP dev/db_printers.ml OCAMLDEP dev/vm_printers.ml OCAMLDEP library/goptions.ml OCAMLDEP library/nameops.ml OCAMLDEP library/summary.ml OCAMLDEP library/libobject.ml OCAMLDEP library/decls.ml OCAMLDEP library/heads.ml OCAMLDEP library/nametab.ml OCAMLDEP library/lib.ml OCAMLDEP library/library.ml OCAMLDEP library/states.ml OCAMLDEP library/impargs.ml OCAMLDEP library/global.ml OCAMLDEP library/declare.ml OCAMLDEP library/decl_kinds.ml OCAMLDEP library/libnames.ml OCAMLDEP library/assumptions.ml OCAMLDEP library/declaremods.ml OCAMLDEP library/dischargedhypsmap.ml OCAMLDEP checker/typeops.ml OCAMLDEP checker/indtypes.ml OCAMLDEP checker/reduction.ml OCAMLDEP checker/inductive.ml OCAMLDEP checker/validate.ml OCAMLDEP checker/main.ml OCAMLDEP checker/closure.ml OCAMLDEP checker/mod_checking.ml OCAMLDEP checker/safe_typing.ml OCAMLDEP checker/term.ml OCAMLDEP checker/checker.ml OCAMLDEP checker/modops.ml OCAMLDEP checker/subtyping.ml OCAMLDEP checker/environ.ml OCAMLDEP checker/check.ml OCAMLDEP checker/type_errors.ml OCAMLDEP checker/declarations.ml OCAMLDEP checker/check_stat.ml OCAMLDEP tools/mkwinapp.ml OCAMLDEP tools/escape_string.ml OCAMLDEP tools/compat5b.ml OCAMLDEP tools/gallina.ml OCAMLDEP tools/coq_tex.ml OCAMLDEP tools/compat5.ml OCAMLDEP tools/coqdoc/index.ml OCAMLDEP tools/coqdoc/alpha.ml OCAMLDEP tools/coqdoc/main.ml OCAMLDEP tools/coqdoc/tokens.ml OCAMLDEP tools/coqdoc/output.ml OCAMLDEP tools/coqdoc/cdglobals.ml OCAMLDEP tools/mingwpath.ml OCAMLDEP tools/coqdep_boot.ml OCAMLDEP tools/fake_ide.ml OCAMLDEP tools/coqdep_common.ml OCAMLDEP tools/win32hack_filename.ml OCAMLDEP tools/coqdep.ml OCAMLDEP tools/coq_makefile.ml OCAMLDEP lib/fset.ml OCAMLDEP lib/profile.ml OCAMLDEP lib/gmapl.ml OCAMLDEP lib/envars.ml OCAMLDEP lib/store.ml OCAMLDEP lib/flags.ml OCAMLDEP lib/dyn.ml OCAMLDEP lib/hashtbl_alt.ml OCAMLDEP lib/gmap.ml OCAMLDEP lib/fmap.ml OCAMLDEP lib/rtree.ml OCAMLDEP lib/xml_utils.ml OCAMLDEP lib/util.ml OCAMLDEP lib/heap.ml OCAMLDEP lib/xml_parser.ml OCAMLDEP lib/bigint.ml OCAMLDEP lib/option.ml OCAMLDEP lib/hashcons.ml OCAMLDEP lib/predicate.ml OCAMLDEP lib/unicodetable.ml OCAMLDEP lib/dnet.ml OCAMLDEP lib/unionfind.ml OCAMLDEP lib/tries.ml OCAMLDEP lib/segmenttree.ml OCAMLDEP lib/pp_control.ml OCAMLDEP lib/system.ml OCAMLDEP lib/explore.ml OCAMLDEP lib/errors.ml OCAMLDEP scripts/coqc.ml OCAMLDEP scripts/coqmktop.ml OCAMLDEP kernel/typeops.ml OCAMLDEP kernel/names.ml OCAMLDEP kernel/sign.ml OCAMLDEP kernel/indtypes.ml OCAMLDEP kernel/reduction.ml OCAMLDEP kernel/vconv.ml OCAMLDEP kernel/conv_oracle.ml OCAMLDEP kernel/inductive.ml OCAMLDEP kernel/vm.ml OCAMLDEP kernel/closure.ml OCAMLDEP kernel/term.ml OCAMLDEP kernel/esubst.ml OCAMLDEP kernel/term_typing.ml OCAMLDEP kernel/modops.ml OCAMLDEP kernel/subtyping.ml OCAMLDEP kernel/cbytecodes.ml OCAMLDEP kernel/csymtable.ml OCAMLDEP kernel/environ.ml OCAMLDEP kernel/type_errors.ml OCAMLDEP kernel/mod_subst.ml OCAMLDEP kernel/retroknowledge.ml OCAMLDEP kernel/univ.ml OCAMLDEP kernel/cbytegen.ml OCAMLDEP kernel/safe_typing.ml OCAMLDEP kernel/pre_env.ml OCAMLDEP kernel/cooking.ml OCAMLDEP kernel/cemitcodes.ml OCAMLDEP kernel/mod_typing.ml OCAMLDEP kernel/entries.ml OCAMLDEP kernel/declarations.ml COQDEP plugins/extraction/ExtrOcamlString.v COQDEP plugins/extraction/ExtrOcamlZBigInt.v COQDEP plugins/extraction/ExtrOcamlZInt.v COQDEP plugins/extraction/ExtrOcamlNatBigInt.v COQDEP plugins/extraction/ExtrOcamlNatInt.v COQDEP plugins/extraction/ExtrOcamlBigIntConv.v COQDEP plugins/extraction/ExtrOcamlIntConv.v COQDEP plugins/extraction/ExtrOcamlBasic.v COQDEP plugins/nsatz/Nsatz.v COQDEP plugins/quote/Quote.v COQDEP plugins/setoid_ring/Integral_domain.v COQDEP plugins/setoid_ring/Rings_Q.v COQDEP plugins/setoid_ring/Rings_R.v COQDEP plugins/setoid_ring/Rings_Z.v COQDEP plugins/setoid_ring/Ncring_tac.v COQDEP plugins/setoid_ring/Ncring_initial.v COQDEP plugins/setoid_ring/Ncring_polynom.v COQDEP plugins/setoid_ring/Ncring.v COQDEP plugins/setoid_ring/Cring.v COQDEP plugins/setoid_ring/Algebra_syntax.v COQDEP plugins/setoid_ring/ZArithRing.v COQDEP plugins/setoid_ring/Ring.v COQDEP plugins/setoid_ring/Ring_theory.v COQDEP plugins/setoid_ring/Ring_tac.v COQDEP plugins/setoid_ring/Ring_polynom.v COQDEP plugins/setoid_ring/Ring_equiv.v COQDEP plugins/setoid_ring/Ring_base.v COQDEP plugins/setoid_ring/RealField.v COQDEP plugins/setoid_ring/NArithRing.v COQDEP plugins/setoid_ring/InitialRing.v COQDEP plugins/setoid_ring/Field.v COQDEP plugins/setoid_ring/Field_theory.v COQDEP plugins/setoid_ring/Field_tac.v COQDEP plugins/setoid_ring/BinList.v COQDEP plugins/setoid_ring/ArithRing.v COQDEP plugins/rtauto/Rtauto.v COQDEP plugins/rtauto/Bintree.v COQDEP plugins/funind/Recdef.v COQDEP plugins/fourier/Fourier.v COQDEP plugins/fourier/Fourier_util.v COQDEP plugins/field/LegacyField.v COQDEP plugins/field/LegacyField_Theory.v COQDEP plugins/field/LegacyField_Tactic.v COQDEP plugins/field/LegacyField_Compl.v COQDEP plugins/ring/Setoid_ring.v COQDEP plugins/ring/Setoid_ring_theory.v COQDEP plugins/ring/Setoid_ring_normalize.v COQDEP plugins/ring/Ring_normalize.v COQDEP plugins/ring/Ring_abstract.v COQDEP plugins/ring/LegacyZArithRing.v COQDEP plugins/ring/LegacyRing.v COQDEP plugins/ring/LegacyRing_theory.v COQDEP plugins/ring/LegacyNArithRing.v COQDEP plugins/ring/LegacyArithRing.v COQDEP plugins/micromega/ZMicromega.v COQDEP plugins/micromega/ZCoeff.v COQDEP plugins/micromega/VarMap.v COQDEP plugins/micromega/Tauto.v COQDEP plugins/micromega/RMicromega.v COQDEP plugins/micromega/RingMicromega.v COQDEP plugins/micromega/Refl.v COQDEP plugins/micromega/QMicromega.v COQDEP plugins/micromega/Psatz.v COQDEP plugins/micromega/OrderedRing.v COQDEP plugins/micromega/Env.v COQDEP plugins/micromega/EnvRing.v COQDEP plugins/micromega/CheckerMaker.v COQDEP plugins/romega/ROmega.v COQDEP plugins/romega/ReflOmegaCore.v COQDEP plugins/omega/PreOmega.v COQDEP plugins/omega/Omega.v COQDEP plugins/omega/OmegaPlugin.v COQDEP plugins/omega/OmegaLemmas.v COQDEP theories/Vectors/Vector.v COQDEP theories/Vectors/VectorSpec.v COQDEP theories/Vectors/VectorDef.v COQDEP theories/Vectors/Fin.v COQDEP theories/Structures/OrderedType.v COQDEP theories/Structures/OrderedTypeEx.v COQDEP theories/Structures/OrderedTypeAlt.v COQDEP theories/Structures/DecidableTypeEx.v COQDEP theories/Structures/DecidableType.v COQDEP theories/Structures/GenericMinMax.v COQDEP theories/Structures/OrdersAlt.v COQDEP theories/Structures/OrdersTac.v COQDEP theories/Structures/OrdersLists.v COQDEP theories/Structures/OrdersFacts.v COQDEP theories/Structures/OrdersEx.v COQDEP theories/Structures/Orders.v COQDEP theories/Structures/EqualitiesFacts.v COQDEP theories/Structures/Equalities.v COQDEP theories/Program/Wf.v COQDEP theories/Program/Utils.v COQDEP theories/Program/Tactics.v COQDEP theories/Program/Syntax.v COQDEP theories/Program/Subset.v COQDEP theories/Program/Program.v COQDEP theories/Program/Equality.v COQDEP theories/Program/Combinators.v COQDEP theories/Program/Basics.v COQDEP theories/Classes/RelationPairs.v COQDEP theories/Classes/SetoidTactics.v COQDEP theories/Classes/SetoidDec.v COQDEP theories/Classes/SetoidClass.v COQDEP theories/Classes/RelationClasses.v COQDEP theories/Classes/Morphisms.v COQDEP theories/Classes/Morphisms_Relations.v COQDEP theories/Classes/Morphisms_Prop.v COQDEP theories/Classes/Init.v COQDEP theories/Classes/EquivDec.v COQDEP theories/Classes/Equivalence.v COQDEP theories/Unicode/Utf8_core.v COQDEP theories/Unicode/Utf8.v COQDEP theories/Numbers/Rational/SpecViaQ/QSig.v COQDEP theories/Numbers/Rational/BigQ/QMake.v COQDEP theories/Numbers/Rational/BigQ/BigQ.v COQDEP theories/Numbers/NumPrelude.v COQDEP theories/Numbers/Natural/SpecViaZ/NSig.v COQDEP theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v COQDEP theories/Numbers/Natural/Peano/NPeano.v COQDEP theories/Numbers/Natural/Binary/NBinary.v COQDEP theories/Numbers/Natural/BigN/NMake.v COQDEP theories/Numbers/Natural/BigN/NMake_gen.v COQDEP theories/Numbers/Natural/BigN/Nbasic.v COQDEP theories/Numbers/Natural/BigN/BigN.v COQDEP theories/Numbers/Natural/Abstract/NBits.v COQDEP theories/Numbers/Natural/Abstract/NLcm.v COQDEP theories/Numbers/Natural/Abstract/NGcd.v COQDEP theories/Numbers/Natural/Abstract/NLog.v COQDEP theories/Numbers/Natural/Abstract/NSqrt.v COQDEP theories/Numbers/Natural/Abstract/NPow.v COQDEP theories/Numbers/Natural/Abstract/NParity.v COQDEP theories/Numbers/Natural/Abstract/NMaxMin.v COQDEP theories/Numbers/Natural/Abstract/NDiv.v COQDEP theories/Numbers/Natural/Abstract/NProperties.v COQDEP theories/Numbers/Natural/Abstract/NSub.v COQDEP theories/Numbers/Natural/Abstract/NStrongRec.v COQDEP theories/Numbers/Natural/Abstract/NOrder.v COQDEP theories/Numbers/Natural/Abstract/NMulOrder.v COQDEP theories/Numbers/Natural/Abstract/NIso.v COQDEP theories/Numbers/Natural/Abstract/NDefOps.v COQDEP theories/Numbers/Natural/Abstract/NBase.v COQDEP theories/Numbers/Natural/Abstract/NAxioms.v COQDEP theories/Numbers/Natural/Abstract/NAdd.v COQDEP theories/Numbers/Natural/Abstract/NAddOrder.v COQDEP theories/Numbers/NatInt/NZBits.v COQDEP theories/Numbers/NatInt/NZGcd.v COQDEP theories/Numbers/NatInt/NZLog.v COQDEP theories/Numbers/NatInt/NZSqrt.v COQDEP theories/Numbers/NatInt/NZPow.v COQDEP theories/Numbers/NatInt/NZDiv.v COQDEP theories/Numbers/NatInt/NZParity.v COQDEP theories/Numbers/NatInt/NZDomain.v COQDEP theories/Numbers/NatInt/NZProperties.v COQDEP theories/Numbers/NatInt/NZOrder.v COQDEP theories/Numbers/NatInt/NZMul.v COQDEP theories/Numbers/NatInt/NZMulOrder.v COQDEP theories/Numbers/NatInt/NZBase.v COQDEP theories/Numbers/NatInt/NZAxioms.v COQDEP theories/Numbers/NatInt/NZAdd.v COQDEP theories/Numbers/NatInt/NZAddOrder.v COQDEP theories/Numbers/NaryFunctions.v COQDEP theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v COQDEP theories/Numbers/Integer/SpecViaZ/ZSig.v COQDEP theories/Numbers/Integer/NatPairs/ZNatPairs.v COQDEP theories/Numbers/Integer/Binary/ZBinary.v COQDEP theories/Numbers/Integer/BigZ/ZMake.v COQDEP theories/Numbers/Integer/BigZ/BigZ.v COQDEP theories/Numbers/Integer/Abstract/ZProperties.v COQDEP theories/Numbers/Integer/Abstract/ZBits.v COQDEP theories/Numbers/Integer/Abstract/ZLcm.v COQDEP theories/Numbers/Integer/Abstract/ZGcd.v COQDEP theories/Numbers/Integer/Abstract/ZPow.v COQDEP theories/Numbers/Integer/Abstract/ZParity.v COQDEP theories/Numbers/Integer/Abstract/ZMaxMin.v COQDEP theories/Numbers/Integer/Abstract/ZDivEucl.v COQDEP theories/Numbers/Integer/Abstract/ZDivTrunc.v COQDEP theories/Numbers/Integer/Abstract/ZDivFloor.v COQDEP theories/Numbers/Integer/Abstract/ZSgnAbs.v COQDEP theories/Numbers/Integer/Abstract/ZMul.v COQDEP theories/Numbers/Integer/Abstract/ZMulOrder.v COQDEP theories/Numbers/Integer/Abstract/ZLt.v COQDEP theories/Numbers/Integer/Abstract/ZBase.v COQDEP theories/Numbers/Integer/Abstract/ZAdd.v COQDEP theories/Numbers/Integer/Abstract/ZAxioms.v COQDEP theories/Numbers/Integer/Abstract/ZAddOrder.v COQDEP theories/Numbers/Cyclic/ZModulo/ZModulo.v COQDEP theories/Numbers/Cyclic/Int31/Ring31.v COQDEP theories/Numbers/Cyclic/Int31/Cyclic31.v COQDEP theories/Numbers/Cyclic/Int31/Int31.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v COQDEP theories/Numbers/Cyclic/Abstract/NZCyclic.v COQDEP theories/Numbers/Cyclic/Abstract/CyclicAxioms.v COQDEP theories/Numbers/BigNumPrelude.v COQDEP theories/Numbers/BinNums.v COQDEP theories/QArith/Qminmax.v COQDEP theories/QArith/QOrderedType.v COQDEP theories/QArith/Qround.v COQDEP theories/QArith/Qring.v COQDEP theories/QArith/Qreduction.v COQDEP theories/QArith/Qreals.v COQDEP theories/QArith/Qpower.v COQDEP theories/QArith/Qfield.v COQDEP theories/QArith/Qcanon.v COQDEP theories/QArith/QArith.v COQDEP theories/QArith/QArith_base.v COQDEP theories/QArith/Qabs.v COQDEP theories/Sorting/Mergesort.v COQDEP theories/Sorting/Sorting.v COQDEP theories/Sorting/Sorted.v COQDEP theories/Sorting/PermutEq.v COQDEP theories/Sorting/PermutSetoid.v COQDEP theories/Sorting/Permutation.v COQDEP theories/Sorting/Heap.v COQDEP theories/Reals/Rminmax.v COQDEP theories/Reals/ROrderedType.v COQDEP theories/Reals/Sqrt_reg.v COQDEP theories/Reals/SplitRmult.v COQDEP theories/Reals/SplitAbsolu.v COQDEP theories/Reals/SeqSeries.v COQDEP theories/Reals/SeqProp.v COQDEP theories/Reals/Rtrigo.v COQDEP theories/Reals/Rtrigo1.v COQDEP theories/Reals/Rtrigo_reg.v COQDEP theories/Reals/Rtrigo_fun.v COQDEP theories/Reals/Rtrigo_def.v COQDEP theories/Reals/Rtrigo_calc.v COQDEP theories/Reals/Rtrigo_alt.v COQDEP theories/Reals/Rtopology.v COQDEP theories/Reals/R_sqr.v COQDEP theories/Reals/R_sqrt.v COQDEP theories/Reals/Rsqrt_def.v COQDEP theories/Reals/Rsigma.v COQDEP theories/Reals/Rseries.v COQDEP theories/Reals/Rprod.v COQDEP theories/Reals/Rpower.v COQDEP theories/Reals/Rpow_def.v COQDEP theories/Reals/Rlogic.v COQDEP theories/Reals/RList.v COQDEP theories/Reals/Rlimit.v COQDEP theories/Reals/RIneq.v COQDEP theories/Reals/R_Ifp.v COQDEP theories/Reals/RiemannInt.v COQDEP theories/Reals/RiemannInt_SF.v COQDEP theories/Reals/Rgeom.v COQDEP theories/Reals/Rfunctions.v COQDEP theories/Reals/Reals.v COQDEP theories/Reals/Rderiv.v COQDEP theories/Reals/Rdefinitions.v COQDEP theories/Reals/Rcomplete.v COQDEP theories/Reals/Rbasic_fun.v COQDEP theories/Reals/Rbase.v COQDEP theories/Reals/Raxioms.v COQDEP theories/Reals/Ratan.v COQDEP theories/Reals/Ranalysis_reg.v COQDEP theories/Reals/Ranalysis.v COQDEP theories/Reals/Ranalysis5.v COQDEP theories/Reals/Ranalysis4.v COQDEP theories/Reals/Ranalysis3.v COQDEP theories/Reals/Ranalysis2.v COQDEP theories/Reals/Ranalysis1.v COQDEP theories/Reals/PSeries_reg.v COQDEP theories/Reals/PartSum.v COQDEP theories/Reals/NewtonInt.v COQDEP theories/Reals/MVT.v COQDEP theories/Reals/Machin.v COQDEP theories/Reals/LegacyRfield.v COQDEP theories/Reals/Integration.v COQDEP theories/Reals/Exp_prop.v COQDEP theories/Reals/DiscrR.v COQDEP theories/Reals/Cos_rel.v COQDEP theories/Reals/Cos_plus.v COQDEP theories/Reals/Cauchy_prod.v COQDEP theories/Reals/Binomial.v COQDEP theories/Reals/ArithProp.v COQDEP theories/Reals/AltSeries.v COQDEP theories/Reals/Alembert.v COQDEP theories/Wellfounded/Well_Ordering.v COQDEP theories/Wellfounded/Wellfounded.v COQDEP theories/Wellfounded/Union.v COQDEP theories/Wellfounded/Transitive_Closure.v COQDEP theories/Wellfounded/Lexicographic_Product.v COQDEP theories/Wellfounded/Lexicographic_Exponentiation.v COQDEP theories/Wellfounded/Inverse_Image.v COQDEP theories/Wellfounded/Inclusion.v COQDEP theories/Wellfounded/Disjoint_Union.v COQDEP theories/Relations/Relations.v COQDEP theories/Relations/Relation_Operators.v COQDEP theories/Relations/Relation_Definitions.v COQDEP theories/Relations/Operators_Properties.v COQDEP theories/MSets/MSetPositive.v COQDEP theories/MSets/MSetWeakList.v COQDEP theories/MSets/MSetToFiniteSet.v COQDEP theories/MSets/MSets.v COQDEP theories/MSets/MSetProperties.v COQDEP theories/MSets/MSetInterface.v COQDEP theories/MSets/MSetFacts.v COQDEP theories/MSets/MSetList.v COQDEP theories/MSets/MSetEqProperties.v COQDEP theories/MSets/MSetDecide.v COQDEP theories/MSets/MSetRBT.v COQDEP theories/MSets/MSetAVL.v COQDEP theories/MSets/MSetGenTree.v COQDEP theories/FSets/FSetWeakList.v COQDEP theories/FSets/FSetToFiniteSet.v COQDEP theories/FSets/FSets.v COQDEP theories/FSets/FSetProperties.v COQDEP theories/FSets/FSetList.v COQDEP theories/FSets/FSetInterface.v COQDEP theories/FSets/FSetFacts.v COQDEP theories/FSets/FSetEqProperties.v COQDEP theories/FSets/FSetDecide.v COQDEP theories/FSets/FSetBridge.v COQDEP theories/FSets/FSetPositive.v COQDEP theories/FSets/FSetAVL.v COQDEP theories/FSets/FSetCompat.v COQDEP theories/FSets/FMapWeakList.v COQDEP theories/FSets/FMaps.v COQDEP theories/FSets/FMapPositive.v COQDEP theories/FSets/FMapList.v COQDEP theories/FSets/FMapInterface.v COQDEP theories/FSets/FMapFullAVL.v COQDEP theories/FSets/FMapFacts.v COQDEP theories/FSets/FMapAVL.v COQDEP theories/Sets/Uniset.v COQDEP theories/Sets/Relations_3.v COQDEP theories/Sets/Relations_3_facts.v COQDEP theories/Sets/Relations_2.v COQDEP theories/Sets/Relations_2_facts.v COQDEP theories/Sets/Relations_1.v COQDEP theories/Sets/Relations_1_facts.v COQDEP theories/Sets/Powerset.v COQDEP theories/Sets/Powerset_facts.v COQDEP theories/Sets/Powerset_Classical_facts.v COQDEP theories/Sets/Permut.v COQDEP theories/Sets/Partial_Order.v COQDEP theories/Sets/Multiset.v COQDEP theories/Sets/Integers.v COQDEP theories/Sets/Infinite_sets.v COQDEP theories/Sets/Image.v COQDEP theories/Sets/Finite_sets.v COQDEP theories/Sets/Finite_sets_facts.v COQDEP theories/Sets/Ensembles.v COQDEP theories/Sets/Cpo.v COQDEP theories/Sets/Constructive_sets.v COQDEP theories/Sets/Classical_sets.v COQDEP theories/Strings/String.v COQDEP theories/Strings/Ascii.v COQDEP theories/Lists/Streams.v COQDEP theories/Lists/StreamMemo.v COQDEP theories/Lists/SetoidPermutation.v COQDEP theories/Lists/SetoidList.v COQDEP theories/Lists/List.v COQDEP theories/Lists/ListTactics.v COQDEP theories/Lists/ListSet.v COQDEP theories/Setoids/Setoid.v COQDEP theories/ZArith/Zeuclid.v COQDEP theories/ZArith/Zwf.v COQDEP theories/ZArith/Zsqrt_compat.v COQDEP theories/ZArith/Zpow_facts.v COQDEP theories/ZArith/Zpower.v COQDEP theories/ZArith/Zpow_def.v COQDEP theories/ZArith/Zorder.v COQDEP theories/ZArith/Zquot.v COQDEP theories/ZArith/ZOdiv.v COQDEP theories/ZArith/ZOdiv_def.v COQDEP theories/ZArith/Znumtheory.v COQDEP theories/ZArith/Znat.v COQDEP theories/ZArith/Zmisc.v COQDEP theories/ZArith/Zmin.v COQDEP theories/ZArith/Zminmax.v COQDEP theories/ZArith/Zmax.v COQDEP theories/ZArith/Zlogarithm.v COQDEP theories/ZArith/Zhints.v COQDEP theories/ZArith/Zpow_alt.v COQDEP theories/ZArith/Zgcd_alt.v COQDEP theories/ZArith/Zeven.v COQDEP theories/ZArith/Zdiv.v COQDEP theories/ZArith/Zcomplements.v COQDEP theories/ZArith/Zcompare.v COQDEP theories/ZArith/Zbool.v COQDEP theories/ZArith/Zdigits.v COQDEP theories/ZArith/ZArith.v COQDEP theories/ZArith/ZArith_dec.v COQDEP theories/ZArith/ZArith_base.v COQDEP theories/ZArith/Zabs.v COQDEP theories/ZArith/Wf_Z.v COQDEP theories/ZArith/Int.v COQDEP theories/ZArith/BinInt.v COQDEP theories/ZArith/BinIntDef.v COQDEP theories/ZArith/auxiliary.v COQDEP theories/NArith/Ngcd_def.v COQDEP theories/NArith/Nsqrt_def.v COQDEP theories/NArith/Ndiv_def.v COQDEP theories/NArith/Nnat.v COQDEP theories/NArith/Ndist.v COQDEP theories/NArith/Ndigits.v COQDEP theories/NArith/Ndec.v COQDEP theories/NArith/NArith.v COQDEP theories/NArith/BinNat.v COQDEP theories/NArith/BinNatDef.v COQDEP theories/PArith/PArith.v COQDEP theories/PArith/POrderedType.v COQDEP theories/PArith/Pnat.v COQDEP theories/PArith/BinPos.v COQDEP theories/PArith/BinPosDef.v COQDEP theories/Bool/Zerob.v COQDEP theories/Bool/Sumbool.v COQDEP theories/Bool/IfProp.v COQDEP theories/Bool/DecBool.v COQDEP theories/Bool/Bvector.v COQDEP theories/Bool/Bool.v COQDEP theories/Bool/BoolEq.v COQDEP theories/Arith/Wf_nat.v COQDEP theories/Arith/Plus.v COQDEP theories/Arith/Peano_dec.v COQDEP theories/Arith/Mult.v COQDEP theories/Arith/Min.v COQDEP theories/Arith/Minus.v COQDEP theories/Arith/Max.v COQDEP theories/Arith/Lt.v COQDEP theories/Arith/Le.v COQDEP theories/Arith/Gt.v COQDEP theories/Arith/Factorial.v COQDEP theories/Arith/Even.v COQDEP theories/Arith/Euclid.v COQDEP theories/Arith/EqNat.v COQDEP theories/Arith/Div2.v COQDEP theories/Arith/Compare.v COQDEP theories/Arith/Compare_dec.v COQDEP theories/Arith/Bool_nat.v COQDEP theories/Arith/Between.v COQDEP theories/Arith/Arith.v COQDEP theories/Arith/Arith_base.v COQDEP theories/Logic/SetIsType.v COQDEP theories/Logic/RelationalChoice.v COQDEP theories/Logic/ProofIrrelevance.v COQDEP theories/Logic/ProofIrrelevanceFacts.v COQDEP theories/Logic/JMeq.v COQDEP theories/Logic/IndefiniteDescription.v COQDEP theories/Logic/Hurkens.v COQDEP theories/Logic/FunctionalExtensionality.v COQDEP theories/Logic/Eqdep.v COQDEP theories/Logic/EqdepFacts.v COQDEP theories/Logic/Eqdep_dec.v COQDEP theories/Logic/Epsilon.v COQDEP theories/Logic/Diaconescu.v COQDEP theories/Logic/Description.v COQDEP theories/Logic/Decidable.v COQDEP theories/Logic/ConstructiveEpsilon.v COQDEP theories/Logic/Classical.v COQDEP theories/Logic/ClassicalUniqueChoice.v COQDEP theories/Logic/Classical_Type.v COQDEP theories/Logic/Classical_Prop.v COQDEP theories/Logic/Classical_Pred_Type.v COQDEP theories/Logic/Classical_Pred_Set.v COQDEP theories/Logic/ClassicalFacts.v COQDEP theories/Logic/ClassicalEpsilon.v COQDEP theories/Logic/ClassicalDescription.v COQDEP theories/Logic/ClassicalChoice.v COQDEP theories/Logic/ChoiceFacts.v COQDEP theories/Logic/Berardi.v COQDEP theories/Init/Wf.v COQDEP theories/Init/Tactics.v COQDEP theories/Init/Specif.v COQDEP theories/Init/Prelude.v COQDEP theories/Init/Peano.v COQDEP theories/Init/Notations.v COQDEP theories/Init/Logic.v COQDEP theories/Init/Logic_Type.v COQDEP theories/Init/Datatypes.v COQDEP proofs/proofs.mllib COQDEP parsing/highparsing.mllib COQDEP parsing/parsing.mllib COQDEP parsing/grammar.mllib COQDEP interp/interp.mllib COQDEP tactics/tactics.mllib COQDEP tactics/hightactics.mllib COQDEP ide/ide.mllib COQDEP toplevel/toplevel.mllib COQDEP plugins/rtauto/rtauto_plugin.mllib COQDEP plugins/decl_mode/decl_mode_plugin.mllib COQDEP plugins/fourier/fourier_plugin.mllib COQDEP plugins/setoid_ring/newring_plugin.mllib COQDEP plugins/romega/romega_plugin.mllib COQDEP plugins/micromega/micromega_plugin.mllib COQDEP plugins/xml/xml_plugin.mllib COQDEP plugins/nsatz/nsatz_plugin.mllib COQDEP plugins/ring/ring_plugin.mllib COQDEP plugins/quote/quote_plugin.mllib COQDEP plugins/omega/omega_plugin.mllib COQDEP plugins/syntax/z_syntax_plugin.mllib COQDEP plugins/syntax/numbers_syntax_plugin.mllib COQDEP plugins/syntax/ascii_syntax_plugin.mllib COQDEP plugins/syntax/string_syntax_plugin.mllib COQDEP plugins/syntax/nat_syntax_plugin.mllib COQDEP plugins/syntax/r_syntax_plugin.mllib COQDEP plugins/funind/recdef_plugin.mllib COQDEP plugins/firstorder/ground_plugin.mllib COQDEP plugins/field/field_plugin.mllib COQDEP plugins/subtac/subtac_plugin.mllib COQDEP plugins/cc/cc_plugin.mllib COQDEP plugins/extraction/extraction_plugin.mllib COQDEP pretyping/pretyping.mllib COQDEP dev/printers.mllib COQDEP library/library.mllib COQDEP checker/check.mllib COQDEP tools/win32hack.mllib COQDEP lib/lib.mllib COQDEP kernel/kernel.mllib OCAMLDEP parsing/g_prim.ml OCAMLDEP parsing/q_util.ml OCAMLDEP parsing/g_ltac.ml OCAMLDEP parsing/q_constr.ml OCAMLDEP parsing/tacextend.ml OCAMLDEP parsing/lexer.ml OCAMLDEP parsing/g_constr.ml OCAMLDEP parsing/g_proofs.ml OCAMLDEP parsing/g_tactic.ml OCAMLDEP parsing/q_coqast.ml OCAMLDEP parsing/g_xml.ml OCAMLDEP parsing/argextend.ml OCAMLDEP parsing/pcoq.ml OCAMLDEP parsing/g_vernac.ml OCAMLDEP parsing/vernacextend.ml OCAMLDEP ide/project_file.ml OCAMLDEP plugins/xml/proofTree2Xml.ml OCAMLDEP plugins/xml/acic2Xml.ml OCAMLDEP plugins/xml/xml.ml OCAMLDEP lib/compat.ml OCAMLDEP lib/pp.ml gmake[1]: Leaving directory `/scratch/lang/coq/work/coq-8.4pl1' gmake[1]: Entering directory `/scratch/lang/coq/work/coq-8.4pl1' OCAMLC config/coq_config.mli OCAMLC lib/profile.mli OCAMLC parsing/tok.mli OCAMLC lib/pp_control.mli OCAMLC lib/flags.mli OCAMLC lib/segmenttree.mli OCAMLC lib/unicodetable.ml OCAMLC lib/bigint.mli OCAMLC lib/dyn.mli OCAMLC lib/hashcons.mli OCAMLC lib/predicate.mli OCAMLC lib/option.mli OCAMLC lib/store.mli OCAMLC lib/hashtbl_alt.mli OCAMLC kernel/copcodes.ml OCAMLC library/summary.mli OCAMLC library/goptionstyp.mli OCAMLC parsing/tok.ml OCAMLC config/coq_config.ml OCAMLC lib/profile.ml OCAMLC lib/pp_control.ml OCAMLC lib/pp.mli OCAMLC lib/compat.ml OCAMLC lib/flags.ml OCAMLC lib/segmenttree.ml OCAMLC lib/errors.mli OCAMLC lib/bigint.ml OCAMLC lib/hashcons.ml OCAMLC lib/predicate.ml OCAMLC lib/rtree.mli OCAMLC lib/option.ml OCAMLC lib/hashtbl_alt.ml OCAMLC kernel/names.mli OCAMLC parsing/extend.mli OCAMLC lib/pp.ml OCAMLC lib/util.mli OCAMLC kernel/univ.mli OCAMLC kernel/esubst.mli OCAMLC kernel/conv_oracle.mli OCAMLC library/summary.ml OCAMLC interp/ppextend.mli OCAMLC parsing/lexer.mli OCAMLC parsing/extend.ml OCAMLC lib/util.ml OCAMLC lib/errors.ml OCAMLC lib/dyn.ml OCAMLC lib/rtree.ml OCAMLC lib/store.ml OCAMLC kernel/names.ml OCAMLC kernel/univ.ml OCAMLC kernel/esubst.ml OCAMLC kernel/term.mli OCAMLC kernel/conv_oracle.ml OCAMLC interp/ppextend.ml OCAMLC parsing/lexer.ml OCAMLC kernel/term.ml OCAMLC kernel/mod_subst.mli OCAMLC kernel/sign.mli OCAMLC kernel/cbytecodes.mli OCAMLC library/nameops.mli OCAMLC kernel/mod_subst.ml OCAMLC library/libnames.mli OCAMLC kernel/sign.ml OCAMLC kernel/cbytecodes.ml OCAMLC kernel/cemitcodes.mli OCAMLC kernel/retroknowledge.mli OCAMLC kernel/entries.mli OCAMLC library/nameops.ml OCAMLC library/libnames.ml OCAMLC library/nametab.mli OCAMLC library/libobject.mli OCAMLC library/goptions.mli OCAMLC library/decl_kinds.mli OCAMLC kernel/cemitcodes.ml OCAMLC kernel/declarations.mli OCAMLC kernel/retroknowledge.ml OCAMLC kernel/pre_env.mli OCAMLC kernel/entries.ml OCAMLC library/nametab.ml OCAMLC library/libobject.ml OCAMLC library/lib.mli OCAMLC library/decl_kinds.ml OCAMLC kernel/declarations.ml OCAMLC kernel/pre_env.ml OCAMLC kernel/cbytegen.mli OCAMLC kernel/environ.mli OCAMLC library/goptions.ml OCAMLC kernel/cbytegen.ml OCAMLC kernel/environ.ml OCAMLC kernel/closure.mli OCAMLC kernel/type_errors.mli OCAMLC kernel/modops.mli OCAMLC kernel/inductive.mli OCAMLC kernel/typeops.mli OCAMLC kernel/cooking.mli OCAMLC kernel/subtyping.mli OCAMLC kernel/mod_typing.mli OCAMLC kernel/safe_typing.mli OCAMLC library/lib.ml OCAMLC pretyping/namegen.mli OCAMLC library/declaremods.mli OCAMLC kernel/closure.ml OCAMLC kernel/reduction.mli OCAMLC kernel/modops.ml OCAMLC kernel/inductive.ml OCAMLC kernel/typeops.ml OCAMLC kernel/indtypes.mli OCAMLC kernel/cooking.ml OCAMLC kernel/term_typing.mli OCAMLC kernel/subtyping.ml OCAMLC kernel/mod_typing.ml OCAMLC kernel/safe_typing.ml OCAMLC library/global.mli OCAMLC pretyping/termops.mli OCAMLC kernel/reduction.ml OCAMLC kernel/type_errors.ml OCAMLC kernel/indtypes.ml OCAMLC kernel/term_typing.ml OCAMLC library/global.ml OCAMLC pretyping/termops.ml OCAMLC pretyping/namegen.ml OCAMLC pretyping/evd.mli OCAMLC pretyping/evd.ml OCAMLC pretyping/reductionops.mli OCAMLC pretyping/inductiveops.mli OCAMLC pretyping/glob_term.mli OCAMLC pretyping/classops.mli OCAMLC pretyping/reductionops.ml OCAMLC pretyping/inductiveops.ml OCAMLC pretyping/glob_term.ml OCAMLC pretyping/detyping.mli OCAMLC pretyping/pattern.mli OCAMLC interp/topconstr.mli OCAMLC pretyping/detyping.ml OCAMLC pretyping/pattern.ml OCAMLC interp/topconstr.ml OCAMLC interp/notation.mli OCAMLC interp/genarg.mli OCAMLC interp/genarg.ml OCAMLC proofs/tacexpr.ml OCAMLC parsing/extrawit.mli OCAMLC toplevel/vernacexpr.ml OCAMLC parsing/extrawit.ml OCAMLC parsing/pcoq.mli OCAMLC parsing/pcoq.ml OCAMLC parsing/q_util.mli OCAMLC parsing/egrammar.mli OCAMLC parsing/g_prim.ml OCAMLC parsing/g_tactic.ml OCAMLC parsing/g_ltac.ml OCAMLC parsing/g_constr.ml OCAMLC parsing/q_constr.ml OCAMLC parsing/q_util.ml OCAMLC parsing/q_coqast.ml OCAMLC parsing/egrammar.ml OCAMLC parsing/argextend.ml OCAMLC parsing/tacextend.ml OCAMLC parsing/vernacextend.ml Testing parsing/grammar.cma OCAMLC -a parsing/grammar.cma CAMLP4O tactics/eauto.ml4 CAMLP4O tactics/eqdecide.ml4 CAMLP4O tactics/rewrite.ml4 CAMLP4O tactics/extraargs.ml4 CAMLP4O tactics/hipattern.ml4 CAMLP4O tactics/extratactics.ml4 CAMLP4O tactics/class_tactics.ml4 CAMLP4O tactics/tauto.ml4 CAMLP4O toplevel/whelp.ml4 CAMLP4O plugins/rtauto/g_rtauto.ml4 CAMLP4O plugins/decl_mode/g_decl_mode.ml4 CAMLP4O plugins/fourier/g_fourier.ml4 CAMLP4O plugins/setoid_ring/newring.ml4 CAMLP4O plugins/romega/g_romega.ml4 CAMLP4O plugins/micromega/g_micromega.ml4 CAMLP4O plugins/xml/xmlentries.ml4 CAMLP4O plugins/xml/dumptree.ml4 CAMLP4O plugins/nsatz/nsatz.ml4 CAMLP4O plugins/ring/g_ring.ml4 CAMLP4O plugins/quote/g_quote.ml4 CAMLP4O plugins/omega/g_omega.ml4 CAMLP4O plugins/funind/g_indfun.ml4 CAMLP4O plugins/firstorder/g_ground.ml4 CAMLP4O plugins/field/field.ml4 CAMLP4O plugins/subtac/g_subtac.ml4 CAMLP4O plugins/cc/g_congruence.ml4 CAMLP4O plugins/extraction/g_extraction.ml4 OCAMLDEP tactics/eauto.ml OCAMLDEP tactics/eqdecide.ml OCAMLDEP tactics/rewrite.ml OCAMLDEP tactics/extraargs.ml OCAMLDEP tactics/hipattern.ml OCAMLDEP tactics/extratactics.ml OCAMLDEP tactics/class_tactics.ml OCAMLDEP tactics/tauto.ml OCAMLDEP toplevel/whelp.ml OCAMLDEP plugins/rtauto/g_rtauto.ml OCAMLDEP plugins/decl_mode/g_decl_mode.ml OCAMLDEP plugins/fourier/g_fourier.ml OCAMLDEP plugins/setoid_ring/newring.ml OCAMLDEP plugins/romega/g_romega.ml OCAMLDEP plugins/micromega/g_micromega.ml OCAMLDEP plugins/xml/xmlentries.ml OCAMLDEP plugins/xml/dumptree.ml OCAMLDEP plugins/nsatz/nsatz.ml OCAMLDEP plugins/ring/g_ring.ml OCAMLDEP plugins/quote/g_quote.ml OCAMLDEP plugins/omega/g_omega.ml OCAMLDEP plugins/funind/g_indfun.ml OCAMLDEP plugins/firstorder/g_ground.ml OCAMLDEP plugins/field/field.ml OCAMLDEP plugins/subtac/g_subtac.ml OCAMLDEP plugins/cc/g_congruence.ml OCAMLDEP plugins/extraction/g_extraction.ml gmake[1]: Leaving directory `/scratch/lang/coq/work/coq-8.4pl1' gmake[1]: Entering directory `/scratch/lang/coq/work/coq-8.4pl1' CHECK revision OCAMLOPT config/coq_config.ml OCAMLOPT lib/pp_control.ml OCAMLOPT parsing/tok.ml OCAMLOPT lib/flags.ml OCAMLOPT lib/segmenttree.ml OCAMLOPT lib/unicodetable.ml OCAMLC lib/system.mli OCAMLC lib/envars.mli OCAMLC scripts/tolink.ml OCAMLC lib/xml_lexer.mli OCAMLC lib/xml_parser.mli OCAMLOPT lib/bigint.ml OCAMLOPT lib/hashcons.ml OCAMLC lib/gmap.mli OCAMLC lib/fset.mli OCAMLC lib/fmap.mli OCAMLC lib/tries.mli OCAMLC lib/gmapl.mli OCAMLOPT lib/profile.ml OCAMLC lib/explore.mli OCAMLOPT lib/predicate.ml OCAMLC lib/heap.mli OCAMLOPT lib/option.ml OCAMLC lib/dnet.mli OCAMLC lib/unionfind.mli OCAMLOPT lib/hashtbl_alt.ml OCAMLOPT kernel/copcodes.ml OCAMLC kernel/vm.mli OCAMLC kernel/csymtable.mli OCAMLC kernel/vconv.mli OCAMLC library/library.mli OCAMLC library/states.mli OCAMLC library/dischargedhypsmap.mli OCAMLC library/decls.mli OCAMLC library/heads.mli OCAMLC library/assumptions.mli OCAMLC pretyping/vnorm.mli OCAMLC pretyping/retyping.mli OCAMLC pretyping/cbv.mli OCAMLC pretyping/pretype_errors.mli OCAMLC pretyping/evarutil.mli OCAMLC pretyping/term_dnet.mli OCAMLC pretyping/recordops.mli OCAMLC pretyping/evarconv.mli OCAMLC pretyping/arguments_renaming.mli OCAMLC pretyping/typing.mli OCAMLC pretyping/matching.mli OCAMLC pretyping/tacred.mli OCAMLC pretyping/typeclasses_errors.mli OCAMLC pretyping/typeclasses.mli OCAMLC pretyping/coercion.mli OCAMLC pretyping/unification.mli OCAMLC pretyping/indrec.mli OCAMLC pretyping/cases.mli OCAMLC interp/dumpglob.mli OCAMLC interp/syntax_def.mli OCAMLC interp/smartlocate.mli OCAMLC interp/reserve.mli OCAMLC library/impargs.mli OCAMLC interp/modintern.mli OCAMLC interp/constrextern.mli OCAMLC interp/coqlib.mli OCAMLC toplevel/discharge.mli OCAMLC library/declare.mli OCAMLC proofs/goal.mli OCAMLC proofs/redexpr.mli OCAMLC proofs/clenv.mli OCAMLC parsing/g_xml.ml OCAMLC parsing/ppconstr.mli OCAMLC parsing/printmod.mli OCAMLC parsing/prettyp.mli OCAMLC tactics/dn.mli OCAMLC tactics/termdn.mli OCAMLC tactics/btermdn.mli OCAMLC toplevel/ind_tables.mli OCAMLC toplevel/vernacinterp.mli OCAMLC toplevel/cerrors.mli OCAMLC toplevel/class.mli OCAMLC toplevel/libtypes.mli OCAMLC toplevel/search.mli OCAMLC toplevel/autoinstance.mli OCAMLC toplevel/indschemes.mli OCAMLC toplevel/record.mli OCAMLC toplevel/backtrack.mli CAMLP4O toplevel/mltop.ml4 OCAMLC toplevel/mltop.mli OCAMLC toplevel/vernacentries.mli OCAMLC toplevel/whelp.mli OCAMLC toplevel/vernac.mli OCAMLC toplevel/interface.mli OCAMLC toplevel/ide_slave.mli OCAMLC toplevel/toplevel.mli OCAMLC toplevel/usage.mli OCAMLC toplevel/coqinit.mli OCAMLC toplevel/coqtop.mli OCAMLC kernel/byterun/coq_fix_code.c OCAMLC kernel/byterun/coq_memory.c OCAMLC kernel/byterun/coq_values.c OCAMLC kernel/byterun/coq_interp.c OCAMLC plugins/syntax/nat_syntax.ml OCAMLC plugins/syntax/nat_syntax_plugin_mod.ml OCAMLC plugins/extraction/miniml.mli OCAMLC plugins/extraction/extraction_plugin_mod.ml OCAMLC plugins/decl_mode/decl_expr.mli OCAMLC plugins/decl_mode/decl_mode_plugin_mod.ml OCAMLC plugins/cc/cc_plugin_mod.ml OCAMLC plugins/firstorder/unify.mli OCAMLC plugins/firstorder/ground_plugin_mod.ml OCAMLC plugins/funind/indfun_common.mli OCAMLC plugins/funind/glob_termops.mli OCAMLC plugins/funind/glob_term_to_relation.mli OCAMLC plugins/funind/recdef_plugin_mod.ml OCAMLC plugins/subtac/subtac_errors.mli OCAMLC plugins/subtac/subtac_coercion.mli OCAMLC plugins/subtac/subtac_cases.mli OCAMLC plugins/subtac/subtac.mli OCAMLC plugins/subtac/subtac_plugin_mod.ml OCAMLC plugins/xml/unshare.mli OCAMLC plugins/xml/xml.mli OCAMLC plugins/xml/acic.ml OCAMLC plugins/xml/xml_plugin_mod.ml OCAMLOPT plugins/xml/unshare.ml OCAMLOPT plugins/xml/xml.ml COQDEP states/MakeInitial.v OCAMLC plugins/syntax/z_syntax.ml OCAMLC plugins/syntax/z_syntax_plugin_mod.ml OCAMLC plugins/quote/quote_plugin_mod.ml OCAMLC plugins/setoid_ring/newring_plugin_mod.ml OCAMLC plugins/omega/omega.ml OCAMLC plugins/omega/omega_plugin_mod.ml OCAMLC plugins/romega/romega_plugin_mod.ml OCAMLC plugins/syntax/ascii_syntax.ml OCAMLC plugins/syntax/ascii_syntax_plugin_mod.ml OCAMLC plugins/syntax/string_syntax.ml OCAMLC plugins/syntax/string_syntax_plugin_mod.ml OCAMLC plugins/syntax/r_syntax.ml OCAMLC plugins/syntax/r_syntax_plugin_mod.ml OCAMLC plugins/ring/ring_plugin_mod.ml OCAMLC plugins/field/field_plugin_mod.ml OCAMLC plugins/fourier/fourier.ml OCAMLC plugins/fourier/fourier_plugin_mod.ml OCAMLOPT plugins/fourier/fourier.ml OCAMLC plugins/syntax/numbers_syntax.ml OCAMLC plugins/syntax/numbers_syntax_plugin_mod.ml OCAMLC plugins/micromega/sos_types.ml OCAMLC plugins/micromega/micromega.mli OCAMLC plugins/micromega/persistent_cache.ml OCAMLC plugins/micromega/micromega_plugin_mod.ml OCAMLOPT plugins/micromega/sos_types.ml OCAMLOPT plugins/micromega/micromega.ml OCAMLOPT plugins/micromega/persistent_cache.ml OCAMLC plugins/rtauto/proof_search.mli OCAMLC plugins/rtauto/rtauto_plugin_mod.ml OCAMLC plugins/nsatz/utile.mli OCAMLC plugins/nsatz/polynom.mli OCAMLC plugins/nsatz/nsatz_plugin_mod.ml OCAMLOPT plugins/nsatz/utile.ml OCAMLC tools/coqdep.ml OCAMLC ide/minilib.mli OCAMLC tools/gallina_lexer.ml OCAMLC tools/coq_tex.ml OCAMLC tools/coqwc.ml OCAMLC tools/coqdoc/cdglobals.ml OCAMLC tools/coqdoc/alpha.mli OCAMLC tools/coqdoc/index.mli OCAMLC dev/vm_printers.ml OCAMLC lib/system.ml OCAMLC lib/envars.ml OCAMLC lib/gmap.ml OCAMLC lib/fset.ml OCAMLC lib/fmap.ml OCAMLC lib/gmapl.ml OCAMLC lib/explore.ml OCAMLC lib/heap.ml OCAMLC lib/dnet.ml OCAMLC library/decls.ml OCAMLC library/heads.ml OCAMLC library/assumptions.ml OCAMLC pretyping/retyping.ml OCAMLC pretyping/cbv.ml OCAMLC pretyping/pretype_errors.ml OCAMLC pretyping/evarutil.ml OCAMLC pretyping/term_dnet.ml OCAMLC pretyping/recordops.ml OCAMLC pretyping/evarconv.ml OCAMLC pretyping/arguments_renaming.ml OCAMLC pretyping/typing.ml OCAMLC pretyping/matching.ml OCAMLC pretyping/tacred.ml OCAMLC pretyping/classops.ml OCAMLC pretyping/typeclasses_errors.ml OCAMLC pretyping/typeclasses.ml OCAMLC pretyping/indrec.ml OCAMLC pretyping/coercion.ml OCAMLC pretyping/unification.ml OCAMLC pretyping/cases.ml OCAMLC library/declaremods.ml OCAMLC interp/notation.ml OCAMLC interp/dumpglob.ml OCAMLC interp/reserve.ml OCAMLC library/impargs.ml OCAMLC interp/syntax_def.ml OCAMLC interp/smartlocate.ml OCAMLC parsing/ppconstr.ml OCAMLC scripts/coqc.ml OCAMLC lib/xml_lexer.ml OCAMLC lib/xml_parser.ml OCAMLC lib/tries.ml OCAMLC lib/unionfind.ml OCAMLC kernel/vm.ml OCAMLC kernel/csymtable.ml OCAMLC library/library.ml OCAMLC kernel/vconv.ml OCAMLC library/states.ml OCAMLC library/dischargedhypsmap.ml OCAMLC pretyping/vnorm.ml OCAMLC interp/coqlib.ml OCAMLC toplevel/discharge.ml OCAMLC library/declare.ml OCAMLC proofs/redexpr.ml OCAMLC tactics/dn.ml OCAMLC tactics/termdn.ml OCAMLC tactics/btermdn.ml OCAMLC toplevel/ind_tables.ml OCAMLC toplevel/libtypes.ml OCAMLC toplevel/mltop.ml OCAMLC toplevel/usage.ml OCAMLC toplevel/coqinit.ml OCAMLC toplevel/coqtop.ml OCAMLC checker/validate.ml OCAMLC checker/check_stat.mli OCAMLOPT checker/validate.ml OCAMLC plugins/micromega/sos_lib.ml OCAMLC plugins/micromega/sos.mli OCAMLC ide/minilib.ml OCAMLC ide/utils/okey.mli OCAMLC ide/utils/config_file.mli OCAMLC ide/utils/configwin_keys.ml OCAMLC ide/utils/configwin_messages.ml OCAMLC ide/utils/configwin.mli OCAMLC ide/utils/editable_cells.ml OCAMLC ide/tags.mli OCAMLC ide/typed_notebook.ml OCAMLC ide/config_lexer.ml OCAMLC ide/utf8_convert.ml OCAMLC ide/preferences.mli OCAMLC ide/ideutils.mli OCAMLC ide/ideproof.ml OCAMLC ide/coq_lex.ml OCAMLC ide/gtk_parsing.ml OCAMLC ide/undo.mli OCAMLC ide/coq.mli OCAMLC ide/coq_commands.ml OCAMLC ide/command_windows.mli OCAMLC ide/coqide.mli OCAMLOPT ide/utils/okey.ml OCAMLOPT ide/utils/config_file.ml OCAMLOPT ide/utils/configwin_keys.ml OCAMLOPT ide/utils/editable_cells.ml OCAMLOPT ide/tags.ml OCAMLOPT ide/utf8_convert.ml OCAMLOPT ide/coq_lex.ml OCAMLOPT ide/gtk_parsing.ml OCAMLOPT ide/coq_commands.ml CAMLP4O ide/coqide_main.ml4 cd bin && ln -sf coqide.opt coqide OCAMLOPT lib/pp.ml OCAMLOPT lib/compat.ml OCAMLOPT scripts/tolink.ml OCAMLC scripts/coqmktop.ml OCAMLOPT lib/xml_lexer.ml OCAMLC lib/xml_utils.mli OCAMLOPT lib/gmap.ml OCAMLOPT lib/fset.ml OCAMLOPT lib/fmap.ml OCAMLOPT lib/explore.ml OCAMLOPT lib/heap.ml OCAMLOPT lib/dnet.ml OCAMLOPT lib/unionfind.ml OCAMLC pretyping/pretyping.mli OCAMLC interp/implicit_quantifiers.mli OCAMLC interp/constrintern.mli OCAMLC proofs/proof_type.mli OCAMLC proofs/proofview.mli OCAMLC tactics/nbtermdn.mli OCAMLC tactics/eqschemes.mli OCAMLC tactics/elimschemes.mli OCAMLC tactics/contradiction.mli OCAMLC tactics/leminv.mli OCAMLC tactics/tactic_option.mli OCAMLC toplevel/metasyntax.mli OCAMLC toplevel/auto_ind_decl.mli OCAMLC toplevel/classes.mli OCAMLC toplevel/ide_intf.mli OCAMLC tactics/extratactics.mli cd kernel/byterun/ && \ "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o OCAMLC -a -o plugins/syntax/nat_syntax_plugin.cma OCAMLC plugins/extraction/table.mli OCAMLC plugins/extraction/modutil.mli OCAMLC plugins/extraction/extraction.mli OCAMLC plugins/extraction/ocaml.mli OCAMLC plugins/extraction/haskell.mli OCAMLC plugins/extraction/scheme.mli OCAMLC plugins/extraction/extract_env.mli OCAMLC plugins/decl_mode/ppdecl_proof.mli OCAMLC plugins/funind/glob_termops.ml OCAMLC plugins/subtac/subtac_obligations.mli OCAMLC plugins/xml/unshare.ml OCAMLC plugins/xml/xml.ml OCAMLC plugins/xml/doubleTypeInference.mli OCAMLC plugins/xml/proof2aproof.ml OCAMLC -a -o plugins/syntax/z_syntax_plugin.cma OCAMLC -a -o plugins/syntax/ascii_syntax_plugin.cma OCAMLC -a -o plugins/syntax/string_syntax_plugin.cma OCAMLC -a -o plugins/syntax/r_syntax_plugin.cma OCAMLC -a -o plugins/syntax/numbers_syntax_plugin.cma OCAMLC plugins/micromega/mutils.ml OCAMLC plugins/micromega/micromega.ml OCAMLC plugins/rtauto/proof_search.ml OCAMLC plugins/nsatz/utile.ml OCAMLC plugins/nsatz/polynom.ml OCAMLC plugins/nsatz/ideal.ml OCAMLOPT ide/minilib.ml OCAMLC ide/project_file.ml OCAMLOPT tools/gallina_lexer.ml OCAMLC tools/gallina.ml OCAMLOPT tools/coq_tex.ml OCAMLOPT tools/coqwc.ml OCAMLOPT tools/coqdoc/cdglobals.ml OCAMLC tools/coqdoc/tokens.mli OCAMLC tools/coqdoc/output.mli OCAMLC tools/coqdoc/cpretty.mli OCAMLC pretyping/pretyping.ml OCAMLC interp/implicit_quantifiers.ml OCAMLC interp/constrintern.ml OCAMLC interp/modintern.ml OCAMLC interp/constrextern.ml OCAMLC proofs/proof_type.ml OCAMLC proofs/goal.ml OCAMLC lib/xml_utils.ml OCAMLC -a -o kernel/kernel.cma OCAMLC -a -o library/library.cma OCAMLC -a -o pretyping/pretyping.cma OCAMLC -a -o interp/interp.cma OCAMLC tactics/nbtermdn.ml OCAMLC tactics/eqschemes.ml OCAMLC tactics/elimschemes.ml OCAMLC toplevel/ide_intf.ml OCAMLC checker/term.mli OCAMLOPT plugins/micromega/sos_lib.ml OCAMLC plugins/micromega/csdpcert.ml OCAMLC tools/fake_ide.ml OCAMLC ide/utils/okey.ml OCAMLC ide/utils/config_file.ml OCAMLC ide/utils/configwin_types.ml OCAMLC ide/tags.ml OCAMLC ide/preferences.ml OCAMLC ide/ideutils.ml OCAMLC ide/undo.ml OCAMLC ide/coq.ml OCAMLC ide/command_windows.ml OCAMLC ide/coqide_ui.ml OCAMLOPT ide/utils/configwin_types.ml OCAMLOPT ide/utils/configwin_messages.ml OCAMLOPT ide/typed_notebook.ml OCAMLOPT ide/config_lexer.ml OCAMLOPT ide/ideproof.ml OCAMLOPT ide/coqide_ui.ml OCAMLOPT lib/util.ml OCAMLOPT lib/xml_parser.ml OCAMLOPT lib/tries.ml OCAMLC proofs/logic.mli OCAMLC proofs/proof.mli OCAMLC proofs/tactic_debug.mli OCAMLC proofs/clenvtac.mli OCAMLC parsing/printer.mli OCAMLC parsing/pptactic.mli OCAMLC parsing/tactic_printer.mli OCAMLOPT tactics/dn.ml OCAMLC toplevel/himsg.mli OCAMLC parsing/ppvernac.mli OCAMLOPT toplevel/ide_intf.ml OCAMLC plugins/extraction/table.ml OCAMLC plugins/extraction/mlutil.mli OCAMLC plugins/decl_mode/ppdecl_proof.ml OCAMLC plugins/subtac/subtac_errors.ml OCAMLC plugins/subtac/subtac_pretyping.mli OCAMLC plugins/subtac/subtac_command.mli OCAMLC plugins/subtac/subtac_classes.mli OCAMLC plugins/xml/doubleTypeInference.ml OCAMLC plugins/xml/cic2acic.ml OCAMLC plugins/xml/xmlcommand.mli OCAMLC plugins/micromega/polynomial.ml OCAMLOPT plugins/micromega/mutils.ml OCAMLOPT plugins/nsatz/polynom.ml OCAMLOPT ide/project_file.ml OCAMLC tools/coq_makefile.ml OCAMLOPT tools/gallina.ml OCAMLBEST -o bin/coq-tex OCAMLBEST -o bin/coqwc OCAMLOPT tools/coqdoc/alpha.ml OCAMLC tools/coqdoc/main.ml OCAMLC proofs/logic.ml OCAMLC proofs/proof.ml OCAMLC parsing/pptactic.ml OCAMLC parsing/tactic_printer.ml OCAMLC toplevel/himsg.ml OCAMLC -a -o lib/lib.cma OCAMLC parsing/printmod.ml OCAMLC parsing/prettyp.ml OCAMLC toplevel/class.ml OCAMLC toplevel/search.ml OCAMLC toplevel/autoinstance.ml OCAMLC checker/term.ml OCAMLC checker/declarations.mli OCAMLOPT plugins/micromega/sos.ml OCAMLC ide/utils/configwin_ihm.ml OCAMLC ide/coqide.ml OCAMLOPT ide/utils/configwin_ihm.ml OCAMLOPT lib/errors.ml OCAMLOPT lib/system.ml OCAMLOPT lib/xml_utils.ml OCAMLOPT lib/dyn.ml OCAMLOPT lib/gmapl.ml OCAMLOPT lib/rtree.ml OCAMLOPT lib/store.ml OCAMLOPT kernel/names.ml OCAMLOPT kernel/esubst.ml OCAMLOPT kernel/conv_oracle.ml OCAMLOPT library/nameops.ml OCAMLOPT library/summary.ml OCAMLOPT parsing/lexer.ml OCAMLOPT interp/ppextend.ml OCAMLC proofs/refiner.mli OCAMLOPT parsing/extend.ml OCAMLC proofs/proof_global.mli OCAMLC proofs/tacmach.mli OCAMLC parsing/g_vernac.ml OCAMLC tactics/refine.mli OCAMLC plugins/extraction/mlutil.ml OCAMLC plugins/extraction/modutil.ml OCAMLC plugins/extraction/extraction.ml OCAMLC plugins/extraction/common.mli OCAMLC plugins/decl_mode/decl_mode.mli OCAMLC plugins/cc/ccalgo.mli OCAMLC plugins/firstorder/formula.mli OCAMLC plugins/funind/functional_principles_proofs.mli OCAMLC plugins/funind/functional_principles_types.mli OCAMLC plugins/funind/indfun.mli OCAMLC plugins/subtac/subtac_utils.mli OCAMLC plugins/xml/acic2Xml.ml OCAMLC plugins/xml/xmlentries.ml OCAMLC plugins/xml/dumptree.ml OCAMLOPT plugins/omega/omega.ml OCAMLC plugins/romega/const_omega.mli OCAMLC plugins/micromega/mfourier.ml OCAMLOPT plugins/micromega/polynomial.ml OCAMLC plugins/rtauto/refl_tauto.mli OCAMLOPT plugins/nsatz/ideal.ml OCAMLOPT tools/coq_makefile.ml OCAMLBEST -o bin/gallina OCAMLOPT tools/coqdoc/index.ml OCAMLC proofs/refiner.ml OCAMLC proofs/clenv.ml OCAMLC proofs/proof_global.ml OCAMLC proofs/tactic_debug.ml OCAMLC toplevel/cerrors.ml OCAMLC proofs/tacmach.ml OCAMLC proofs/clenvtac.ml OCAMLC checker/declarations.ml OCAMLC checker/environ.mli OCAMLOPT plugins/micromega/csdpcert.ml OCAMLOPT tools/fake_ide.ml OCAMLC ide/utils/configwin.ml OCAMLOPT ide/utils/configwin.ml OCAMLOPT lib/envars.ml OCAMLOPT kernel/univ.ml OCAMLC proofs/evar_refiner.mli OCAMLC proofs/pfedit.mli OCAMLC tactics/tacticals.mli OCAMLC tactics/hipattern.mli OCAMLC tactics/tactics.mli OCAMLC tactics/hiddentac.mli OCAMLC tactics/elim.mli OCAMLC tactics/auto.mli OCAMLC tactics/equality.mli OCAMLC tactics/inv.mli OCAMLC tactics/tacinterp.mli OCAMLC toplevel/lemmas.mli OCAMLC toplevel/command.mli OCAMLOPT toplevel/usage.ml OCAMLC parsing/g_proofs.ml OCAMLC tactics/extraargs.mli OCAMLC tactics/eauto.mli OCAMLC tactics/tauto.ml OCAMLC tactics/eqdecide.ml OCAMLC plugins/extraction/common.ml OCAMLC plugins/extraction/ocaml.ml OCAMLC plugins/extraction/haskell.ml OCAMLC plugins/extraction/scheme.ml OCAMLC plugins/extraction/extract_env.ml OCAMLC plugins/extraction/g_extraction.ml OCAMLC plugins/decl_mode/decl_mode.ml OCAMLC plugins/decl_mode/decl_interp.mli OCAMLC plugins/decl_mode/decl_proof_instr.mli OCAMLC plugins/cc/ccalgo.ml OCAMLC plugins/cc/ccproof.mli OCAMLC plugins/firstorder/formula.ml OCAMLC plugins/firstorder/unify.ml OCAMLC plugins/firstorder/sequent.mli OCAMLC plugins/funind/indfun_common.ml OCAMLC plugins/funind/recdef.ml OCAMLC plugins/funind/glob_term_to_relation.ml OCAMLC plugins/funind/functional_principles_types.ml OCAMLC plugins/funind/invfun.ml OCAMLC plugins/funind/merge.ml OCAMLC plugins/subtac/subtac_utils.ml OCAMLC plugins/subtac/eterm.mli OCAMLC plugins/subtac/subtac_obligations.ml OCAMLC plugins/subtac/subtac_cases.ml OCAMLC plugins/subtac/subtac_pretyping_F.ml OCAMLC plugins/subtac/subtac_command.ml OCAMLC plugins/subtac/subtac_classes.ml OCAMLC plugins/subtac/subtac.ml OCAMLC plugins/subtac/g_subtac.ml OCAMLC plugins/xml/xmlcommand.ml OCAMLC plugins/xml/proofTree2Xml.ml OCAMLC plugins/xml/cic2Xml.ml OCAMLC plugins/quote/quote.ml OCAMLC plugins/omega/coq_omega.ml OCAMLC plugins/romega/const_omega.ml OCAMLC plugins/romega/refl_omega.ml OCAMLC plugins/ring/ring.ml OCAMLC plugins/micromega/certificate.ml OCAMLOPT plugins/micromega/mfourier.ml OCAMLC plugins/rtauto/refl_tauto.ml OCAMLC plugins/rtauto/g_rtauto.ml OCAMLC plugins/nsatz/nsatz.ml OCAMLOPT tools/coqdep.ml OCAMLBEST -o bin/coq_makefile OCAMLOPT tools/coqdoc/tokens.ml OCAMLC dev/top_printers.ml OCAMLC proofs/evar_refiner.ml OCAMLC proofs/proofview.ml OCAMLC proofs/pfedit.ml OCAMLC parsing/printer.ml OCAMLC toplevel/vernacinterp.ml OCAMLOPT scripts/coqc.ml OCAMLC -a -o proofs/proofs.cma OCAMLC -a -o parsing/parsing.cma OCAMLC tactics/tacticals.ml OCAMLC tactics/hipattern.ml OCAMLC tactics/tactics.ml OCAMLC tactics/hiddentac.ml OCAMLC tactics/elim.ml OCAMLC tactics/auto.ml OCAMLC tactics/equality.ml OCAMLC tactics/contradiction.ml OCAMLC tactics/inv.ml OCAMLC tactics/leminv.ml OCAMLC tactics/tacinterp.ml OCAMLC tactics/tactic_option.ml OCAMLC toplevel/metasyntax.ml OCAMLC toplevel/auto_ind_decl.ml OCAMLC toplevel/lemmas.ml OCAMLC toplevel/indschemes.ml OCAMLC toplevel/command.ml OCAMLC toplevel/classes.ml OCAMLC toplevel/record.ml OCAMLC parsing/ppvernac.ml OCAMLC toplevel/backtrack.ml OCAMLC toplevel/whelp.ml OCAMLC toplevel/vernac.ml OCAMLC toplevel/ide_slave.ml OCAMLC toplevel/toplevel.ml OCAMLC -a -o parsing/highparsing.cma OCAMLC tactics/refine.ml OCAMLC tactics/extraargs.ml OCAMLC tactics/eauto.ml OCAMLC checker/environ.ml OCAMLC checker/closure.mli OCAMLC checker/reduction.mli OCAMLC checker/type_errors.mli OCAMLC checker/modops.mli OCAMLC checker/inductive.mli OCAMLC checker/typeops.mli OCAMLC checker/subtyping.mli OCAMLC checker/mod_checking.mli OCAMLC checker/safe_typing.mli OCAMLOPT checker/term.ml OCAMLBEST -o plugins/micromega/csdpcert OCAMLBEST -o bin/fake_ide OCAMLC -a -o ide/ide.cma OCAMLOPT ide/preferences.ml OCAMLOPT scripts/coqmktop.ml OCAMLOPT -a -o lib/lib.cmxa OCAMLOPT kernel/term.ml OCAMLC tactics/evar_tactics.mli OCAMLC tactics/autorewrite.mli OCAMLC tactics/class_tactics.ml OCAMLC -a -o plugins/extraction/extraction_plugin.cma OCAMLC plugins/decl_mode/decl_interp.ml OCAMLC plugins/decl_mode/decl_proof_instr.ml OCAMLC plugins/decl_mode/g_decl_mode.ml OCAMLC plugins/cc/ccproof.ml OCAMLC plugins/cc/cctac.mli OCAMLC plugins/firstorder/sequent.ml OCAMLC plugins/firstorder/rules.mli OCAMLC plugins/firstorder/ground.mli OCAMLC plugins/funind/functional_principles_proofs.ml OCAMLC plugins/funind/indfun.ml OCAMLC plugins/funind/g_indfun.ml OCAMLC plugins/subtac/eterm.ml OCAMLC plugins/subtac/subtac_coercion.ml OCAMLC plugins/subtac/subtac_pretyping.ml OCAMLC -a -o plugins/xml/xml_plugin.cma OCAMLOPT plugins/xml/acic.ml OCAMLC plugins/quote/g_quote.ml OCAMLC plugins/omega/g_omega.ml OCAMLC plugins/romega/g_romega.ml OCAMLC plugins/ring/g_ring.ml OCAMLC plugins/field/field.ml OCAMLC plugins/fourier/fourierR.ml OCAMLC plugins/micromega/coq_micromega.ml OCAMLC -a -o plugins/rtauto/rtauto_plugin.cma OCAMLC -a -o plugins/nsatz/nsatz_plugin.cma OCAMLBEST -o bin/coqdep Testing dev/printers.cma OCAMLOPT tools/coqdoc/output.ml OCAMLC -a dev/printers.cma OCAMLC tactics/evar_tactics.ml OCAMLC tactics/autorewrite.ml OCAMLC toplevel/vernacentries.ml OCAMLC tactics/extratactics.ml OCAMLC checker/closure.ml OCAMLC checker/reduction.ml OCAMLC checker/type_errors.ml OCAMLC checker/modops.ml OCAMLC checker/inductive.ml OCAMLC checker/typeops.ml OCAMLC checker/indtypes.mli OCAMLC checker/subtyping.ml OCAMLC checker/mod_checking.ml OCAMLC checker/safe_typing.ml OCAMLC checker/check.ml OCAMLC checker/check_stat.ml OCAMLOPT checker/declarations.ml OCAMLOPT ide/ideutils.ml OCAMLOPT -o bin/coqmktop.opt OCAMLOPT kernel/mod_subst.ml strip bin/coqmktop.opt OCAMLOPT kernel/sign.ml OCAMLOPT kernel/cbytecodes.ml OCAMLOPT kernel/entries.ml OCAMLOPT kernel/vm.ml OCAMLOPT library/libnames.ml OCAMLC tactics/rewrite.ml OCAMLC -a -o plugins/decl_mode/decl_mode_plugin.cma OCAMLC plugins/cc/cctac.ml OCAMLC plugins/cc/g_congruence.ml OCAMLC plugins/firstorder/rules.ml OCAMLC plugins/firstorder/instances.mli OCAMLC plugins/firstorder/g_ground.ml OCAMLC -a -o plugins/funind/recdef_plugin.cma OCAMLC -a -o plugins/subtac/subtac_plugin.cma OCAMLC -a -o plugins/quote/quote_plugin.cma OCAMLC plugins/setoid_ring/newring.ml OCAMLC -a -o plugins/omega/omega_plugin.cma OCAMLC -a -o plugins/romega/romega_plugin.cma OCAMLC -a -o plugins/ring/ring_plugin.cma OCAMLC -a -o plugins/field/field_plugin.cma OCAMLC plugins/fourier/g_fourier.ml OCAMLC plugins/micromega/g_micromega.ml OCAMLOPT tools/coqdoc/cpretty.ml cd bin && ln -sf coqmktop.opt coqmktop OCAMLC -a -o tactics/tactics.cma OCAMLC -a -o toplevel/toplevel.cma OCAMLC -a -o tactics/hightactics.cma OCAMLC checker/indtypes.ml OCAMLC checker/checker.ml OCAMLOPT checker/environ.ml OCAMLOPT ide/undo.ml OCAMLOPT ide/coq.ml OCAMLOPT kernel/cemitcodes.ml OCAMLOPT kernel/retroknowledge.ml OCAMLOPT library/libobject.ml OCAMLOPT library/decl_kinds.ml OCAMLC -a -o plugins/cc/cc_plugin.cma OCAMLC plugins/firstorder/instances.ml OCAMLC plugins/firstorder/ground.ml OCAMLC -a -o plugins/setoid_ring/newring_plugin.cma OCAMLC -a -o plugins/fourier/fourier_plugin.cma OCAMLC -a -o plugins/micromega/micromega_plugin.cma OCAMLOPT tools/coqdoc/main.ml COQMKTOP -o bin/coqtop.byte File "lib/lib.cma(Errors)", line 1: Warning 31: files lib/lib.cma(Errors) and /usr/pkg/lib/ocaml/compiler-libs/ocamlbytecomp.cma(Errors) both define a module named Errors File "pretyping/pretyping.cma(Matching)", line 1: Warning 31: files pretyping/pretyping.cma(Matching) and /usr/pkg/lib/ocaml/compiler-libs/ocamlcommon.cma(Matching) both define a module named Matching File "interp/interp.cma(Lexer)", line 1: Warning 31: files interp/interp.cma(Lexer) and /usr/pkg/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer) both define a module named Lexer OCAMLC -a -o checker/check.cma OCAMLOPT checker/closure.ml OCAMLOPT checker/type_errors.ml OCAMLOPT checker/modops.ml OCAMLC -o bin/coqide.byte OCAMLOPT ide/command_windows.ml OCAMLOPT kernel/declarations.ml OCAMLC -a -o plugins/firstorder/ground_plugin.cma OCAMLBEST -o bin/coqdoc OCAMLC -o bin/coqchk.byte OCAMLOPT checker/reduction.ml OCAMLOPT ide/coqide.ml OCAMLOPT kernel/pre_env.ml OCAMLOPT library/nametab.ml OCAMLOPT checker/inductive.ml OCAMLOPT kernel/cbytegen.ml OCAMLOPT checker/typeops.ml OCAMLOPT kernel/environ.ml OCAMLOPT checker/indtypes.ml OCAMLOPT checker/subtyping.ml OCAMLOPT kernel/closure.ml OCAMLOPT kernel/modops.ml OCAMLOPT kernel/csymtable.ml OCAMLOPT checker/mod_checking.ml OCAMLOPT kernel/reduction.ml OCAMLOPT checker/safe_typing.ml OCAMLOPT -a -o ide/ide.cmxa OCAMLOPT checker/check.ml OCAMLOPT checker/check_stat.ml OCAMLOPT kernel/type_errors.ml OCAMLOPT kernel/vconv.ml OCAMLOPT checker/checker.ml OCAMLOPT kernel/inductive.ml OCAMLOPT -a -o checker/check.cmxa OCAMLOPT -o bin/coqchk.opt OCAMLOPT kernel/typeops.ml strip bin/coqchk.opt cd bin && ln -sf coqchk.opt coqchk OCAMLOPT kernel/indtypes.ml OCAMLOPT kernel/cooking.ml OCAMLOPT kernel/subtyping.ml OCAMLOPT library/lib.ml OCAMLOPT pretyping/vnorm.ml OCAMLOPT kernel/term_typing.ml OCAMLOPT library/dischargedhypsmap.ml OCAMLOPT library/goptions.ml OCAMLOPT kernel/mod_typing.ml OCAMLOPT plugins/rtauto/proof_search.ml OCAMLOPT kernel/safe_typing.ml OCAMLOPT -a -o kernel/kernel.cmxa OCAMLOPT library/global.ml OCAMLOPT library/decls.ml OCAMLOPT library/declaremods.ml OCAMLOPT library/assumptions.ml OCAMLOPT pretyping/termops.ml OCAMLOPT library/library.ml OCAMLOPT library/heads.ml OCAMLOPT pretyping/evd.ml OCAMLOPT pretyping/namegen.ml OCAMLOPT toplevel/discharge.ml OCAMLOPT library/states.ml OCAMLOPT pretyping/reductionops.ml OCAMLOPT pretyping/glob_term.ml OCAMLOPT -a -o library/library.cmxa OCAMLOPT pretyping/inductiveops.ml OCAMLOPT pretyping/cbv.ml OCAMLOPT pretyping/retyping.ml OCAMLOPT pretyping/pretype_errors.ml OCAMLOPT pretyping/arguments_renaming.ml OCAMLOPT pretyping/pattern.ml OCAMLOPT pretyping/detyping.ml OCAMLOPT pretyping/indrec.ml OCAMLOPT tactics/termdn.ml OCAMLOPT pretyping/evarutil.ml OCAMLOPT pretyping/matching.ml OCAMLOPT interp/topconstr.ml OCAMLOPT tactics/btermdn.ml OCAMLOPT pretyping/term_dnet.ml OCAMLOPT tactics/nbtermdn.ml OCAMLOPT pretyping/typeclasses_errors.ml OCAMLOPT interp/reserve.ml OCAMLOPT library/impargs.ml OCAMLOPT pretyping/recordops.ml OCAMLOPT pretyping/evarconv.ml OCAMLOPT pretyping/typing.ml OCAMLOPT pretyping/tacred.ml OCAMLOPT pretyping/typeclasses.ml OCAMLOPT pretyping/classops.ml OCAMLOPT proofs/redexpr.ml OCAMLOPT pretyping/coercion.ml OCAMLOPT interp/notation.ml OCAMLOPT interp/dumpglob.ml OCAMLOPT interp/implicit_quantifiers.ml OCAMLOPT pretyping/unification.ml OCAMLOPT pretyping/cases.ml OCAMLOPT interp/genarg.ml OCAMLOPT interp/syntax_def.ml OCAMLOPT library/declare.ml OCAMLOPT proofs/tacexpr.ml OCAMLOPT parsing/extrawit.ml OCAMLOPT toplevel/ind_tables.ml OCAMLOPT toplevel/libtypes.ml OCAMLOPT pretyping/pretyping.ml OCAMLOPT interp/smartlocate.ml OCAMLOPT toplevel/vernacexpr.ml OCAMLOPT parsing/pcoq.ml OCAMLOPT tactics/elimschemes.ml OCAMLOPT -a -o pretyping/pretyping.cmxa OCAMLOPT interp/constrintern.ml OCAMLOPT interp/coqlib.ml OCAMLOPT parsing/egrammar.ml OCAMLOPT parsing/g_xml.ml OCAMLOPT tactics/eqschemes.ml OCAMLOPT parsing/g_constr.ml OCAMLOPT parsing/g_prim.ml OCAMLOPT parsing/g_tactic.ml OCAMLOPT parsing/g_ltac.ml OCAMLOPT plugins/syntax/nat_syntax.ml OCAMLOPT plugins/syntax/z_syntax.ml OCAMLOPT plugins/syntax/ascii_syntax.ml OCAMLOPT plugins/syntax/r_syntax.ml OCAMLOPT plugins/syntax/numbers_syntax.ml OCAMLOPT interp/modintern.ml OCAMLOPT interp/constrextern.ml OCAMLOPT proofs/goal.ml OCAMLOPT plugins/syntax/string_syntax.ml OCAMLOPT proofs/proof_type.ml OCAMLOPT proofs/logic.ml OCAMLOPT plugins/xml/proof2aproof.ml OCAMLOPT -a -o interp/interp.cmxa OCAMLOPT parsing/ppconstr.ml OCAMLOPT proofs/refiner.ml OCAMLOPT proofs/evar_refiner.ml OCAMLOPT proofs/tacmach.ml OCAMLOPT proofs/tactic_debug.ml OCAMLOPT proofs/clenv.ml OCAMLOPT proofs/proofview.ml OCAMLOPT plugins/cc/ccalgo.ml OCAMLOPT plugins/romega/const_omega.ml OCAMLOPT proofs/proof.ml OCAMLOPT proofs/clenvtac.ml OCAMLOPT plugins/cc/ccproof.ml OCAMLOPT plugins/micromega/certificate.ml OCAMLOPT proofs/proof_global.ml OCAMLOPT tactics/tacticals.ml OCAMLOPT proofs/pfedit.ml OCAMLOPT tactics/hipattern.ml OCAMLOPT toplevel/backtrack.ml OCAMLOPT plugins/decl_mode/decl_mode.ml OCAMLOPT -a -o proofs/proofs.cmxa OCAMLOPT parsing/printer.ml OCAMLOPT plugins/firstorder/formula.ml OCAMLOPT plugins/firstorder/unify.ml OCAMLOPT parsing/pptactic.ml OCAMLOPT parsing/printmod.ml OCAMLOPT tactics/tactics.ml OCAMLOPT toplevel/class.ml OCAMLOPT toplevel/search.ml OCAMLOPT toplevel/autoinstance.ml OCAMLOPT plugins/extraction/table.ml OCAMLOPT plugins/decl_mode/ppdecl_proof.ml OCAMLOPT plugins/funind/indfun_common.ml OCAMLOPT plugins/subtac/subtac_errors.ml OCAMLOPT plugins/xml/doubleTypeInference.ml OCAMLOPT plugins/quote/quote.ml OCAMLOPT plugins/romega/refl_omega.ml OCAMLOPT plugins/micromega/coq_micromega.ml OCAMLOPT parsing/tactic_printer.ml OCAMLOPT parsing/prettyp.ml OCAMLOPT tactics/hiddentac.ml OCAMLOPT tactics/contradiction.ml OCAMLOPT toplevel/himsg.ml OCAMLOPT toplevel/lemmas.ml OCAMLOPT tactics/refine.ml OCAMLOPT plugins/extraction/mlutil.ml OCAMLOPT plugins/funind/glob_termops.ml OCAMLOPT plugins/subtac/subtac_utils.ml OCAMLOPT plugins/xml/cic2acic.ml OCAMLOPT -a -o parsing/parsing.cmxa OCAMLOPT tactics/elim.ml OCAMLOPT tactics/auto.ml OCAMLOPT toplevel/cerrors.ml OCAMLOPT plugins/extraction/modutil.ml OCAMLOPT plugins/extraction/extraction.ml OCAMLOPT plugins/extraction/common.ml OCAMLOPT plugins/firstorder/sequent.ml OCAMLOPT plugins/subtac/subtac_cases.ml OCAMLOPT plugins/xml/acic2Xml.ml OCAMLOPT tactics/equality.ml OCAMLOPT plugins/extraction/ocaml.ml OCAMLOPT plugins/extraction/haskell.ml OCAMLOPT plugins/extraction/scheme.ml OCAMLOPT plugins/firstorder/rules.ml OCAMLOPT plugins/xml/proofTree2Xml.ml OCAMLOPT plugins/omega/coq_omega.ml OCAMLOPT tactics/inv.ml OCAMLOPT toplevel/auto_ind_decl.ml OCAMLOPT plugins/firstorder/instances.ml OCAMLOPT tactics/leminv.ml OCAMLOPT toplevel/indschemes.ml OCAMLOPT tactics/tacinterp.ml OCAMLOPT tactics/evar_tactics.ml OCAMLOPT toplevel/vernacinterp.ml OCAMLOPT tactics/tactic_option.ml OCAMLOPT toplevel/metasyntax.ml OCAMLOPT parsing/ppvernac.ml OCAMLOPT toplevel/mltop.optml OCAMLOPT tactics/extraargs.ml OCAMLOPT tactics/tauto.ml OCAMLOPT plugins/syntax/nat_syntax_plugin_mod.ml OCAMLOPT plugins/extraction/extraction_plugin_mod.ml OCAMLOPT plugins/decl_mode/decl_interp.ml OCAMLOPT plugins/decl_mode/decl_mode_plugin_mod.ml OCAMLOPT plugins/cc/cctac.ml OCAMLOPT plugins/cc/cc_plugin_mod.ml OCAMLOPT plugins/firstorder/ground.ml OCAMLOPT plugins/firstorder/ground_plugin_mod.ml OCAMLOPT plugins/funind/invfun.ml OCAMLOPT plugins/funind/recdef_plugin_mod.ml OCAMLOPT plugins/subtac/eterm.ml OCAMLOPT plugins/subtac/subtac_plugin_mod.ml OCAMLOPT plugins/xml/cic2Xml.ml OCAMLOPT plugins/xml/dumptree.ml OCAMLOPT plugins/xml/xml_plugin_mod.ml OCAMLOPT plugins/syntax/z_syntax_plugin_mod.ml OCAMLOPT plugins/quote/g_quote.ml OCAMLOPT plugins/quote/quote_plugin_mod.ml OCAMLOPT plugins/setoid_ring/newring_plugin_mod.ml OCAMLOPT plugins/omega/g_omega.ml OCAMLOPT plugins/omega/omega_plugin_mod.ml OCAMLOPT plugins/romega/g_romega.ml OCAMLOPT plugins/romega/romega_plugin_mod.ml OCAMLOPT plugins/syntax/ascii_syntax_plugin_mod.ml OCAMLOPT plugins/syntax/string_syntax_plugin_mod.ml OCAMLOPT plugins/syntax/r_syntax_plugin_mod.ml OCAMLOPT plugins/ring/ring.ml OCAMLOPT plugins/ring/ring_plugin_mod.ml OCAMLOPT plugins/field/field_plugin_mod.ml OCAMLOPT plugins/fourier/fourier_plugin_mod.ml OCAMLOPT plugins/syntax/numbers_syntax_plugin_mod.ml OCAMLOPT plugins/micromega/micromega_plugin_mod.ml OCAMLOPT plugins/rtauto/refl_tauto.ml OCAMLOPT plugins/rtauto/rtauto_plugin_mod.ml OCAMLOPT plugins/nsatz/nsatz.ml OCAMLOPT plugins/nsatz/nsatz_plugin_mod.ml OCAMLOPT tactics/autorewrite.ml OCAMLOPT toplevel/command.ml OCAMLOPT tactics/extratactics.ml OCAMLOPT tactics/eauto.ml OCAMLOPT -a -o plugins/syntax/nat_syntax_plugin.cmxa OCAMLOPT plugins/decl_mode/decl_proof_instr.ml OCAMLOPT plugins/cc/g_congruence.ml OCAMLOPT plugins/funind/glob_term_to_relation.ml OCAMLOPT plugins/funind/merge.ml OCAMLOPT plugins/subtac/subtac_coercion.ml OCAMLOPT plugins/subtac/subtac_obligations.ml OCAMLOPT -a -o plugins/syntax/z_syntax_plugin.cmxa OCAMLOPT -a -o plugins/quote/quote_plugin.cmxa OCAMLOPT -a -o plugins/omega/omega_plugin.cmxa OCAMLOPT -a -o plugins/romega/romega_plugin.cmxa OCAMLOPT -a -o plugins/syntax/ascii_syntax_plugin.cmxa OCAMLOPT -a -o plugins/syntax/string_syntax_plugin.cmxa OCAMLOPT -a -o plugins/syntax/r_syntax_plugin.cmxa OCAMLOPT plugins/ring/g_ring.ml OCAMLOPT plugins/field/field.ml OCAMLOPT plugins/fourier/fourierR.ml OCAMLOPT -a -o plugins/syntax/numbers_syntax_plugin.cmxa OCAMLOPT plugins/micromega/g_micromega.ml OCAMLOPT plugins/rtauto/g_rtauto.ml OCAMLOPT -a -o plugins/nsatz/nsatz_plugin.cmxa OCAMLOPT -a -o tactics/tactics.cmxa OCAMLOPT toplevel/classes.ml OCAMLOPT toplevel/whelp.ml OCAMLOPT tactics/eqdecide.ml OCAMLOPT -shared -o plugins/syntax/nat_syntax_plugin.cmxs OCAMLOPT -a -o plugins/cc/cc_plugin.cmxa OCAMLOPT plugins/firstorder/g_ground.ml OCAMLOPT plugins/subtac/subtac_pretyping_F.ml OCAMLOPT -shared -o plugins/syntax/z_syntax_plugin.cmxs OCAMLOPT -shared -o plugins/quote/quote_plugin.cmxs OCAMLOPT -shared -o plugins/omega/omega_plugin.cmxs OCAMLOPT -shared -o plugins/romega/romega_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/ascii_syntax_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/string_syntax_plugin.cmxs OCAMLOPT -shared -o plugins/syntax/r_syntax_plugin.cmxs OCAMLOPT -a -o plugins/ring/ring_plugin.cmxa OCAMLOPT -a -o plugins/field/field_plugin.cmxa OCAMLOPT plugins/fourier/g_fourier.ml OCAMLOPT -shared -o plugins/syntax/numbers_syntax_plugin.cmxs OCAMLOPT -a -o plugins/micromega/micromega_plugin.cmxa OCAMLOPT -a -o plugins/rtauto/rtauto_plugin.cmxa OCAMLOPT -shared -o plugins/nsatz/nsatz_plugin.cmxs OCAMLOPT toplevel/record.ml OCAMLOPT tactics/class_tactics.ml OCAMLOPT -shared -o plugins/cc/cc_plugin.cmxs OCAMLOPT -a -o plugins/firstorder/ground_plugin.cmxa OCAMLOPT plugins/subtac/subtac_pretyping.ml OCAMLOPT -shared -o plugins/ring/ring_plugin.cmxs OCAMLOPT -shared -o plugins/field/field_plugin.cmxs OCAMLOPT -a -o plugins/fourier/fourier_plugin.cmxa OCAMLOPT -shared -o plugins/micromega/micromega_plugin.cmxs OCAMLOPT -shared -o plugins/rtauto/rtauto_plugin.cmxs OCAMLOPT toplevel/vernacentries.ml OCAMLOPT tactics/rewrite.ml OCAMLOPT -shared -o plugins/firstorder/ground_plugin.cmxs OCAMLOPT plugins/funind/recdef.ml OCAMLOPT plugins/subtac/subtac_command.ml OCAMLOPT -shared -o plugins/fourier/fourier_plugin.cmxs OCAMLOPT toplevel/vernac.ml OCAMLOPT plugins/extraction/extract_env.ml OCAMLOPT plugins/funind/functional_principles_proofs.ml OCAMLOPT plugins/subtac/subtac_classes.ml OCAMLOPT plugins/xml/xmlcommand.ml OCAMLOPT plugins/setoid_ring/newring.ml OCAMLOPT toplevel/ide_slave.ml OCAMLOPT toplevel/toplevel.ml OCAMLOPT -a -o tactics/hightactics.cmxa OCAMLOPT plugins/extraction/g_extraction.ml OCAMLOPT plugins/funind/functional_principles_types.ml OCAMLOPT plugins/subtac/subtac.ml OCAMLOPT plugins/xml/xmlentries.ml OCAMLOPT -a -o plugins/setoid_ring/newring_plugin.cmxa OCAMLOPT toplevel/coqinit.ml OCAMLOPT -a -o plugins/extraction/extraction_plugin.cmxa OCAMLOPT plugins/funind/indfun.ml OCAMLOPT plugins/subtac/g_subtac.ml OCAMLOPT -a -o plugins/xml/xml_plugin.cmxa OCAMLOPT -shared -o plugins/setoid_ring/newring_plugin.cmxs OCAMLOPT toplevel/coqtop.ml OCAMLOPT parsing/g_vernac.ml OCAMLOPT -shared -o plugins/extraction/extraction_plugin.cmxs OCAMLOPT plugins/funind/g_indfun.ml OCAMLOPT -a -o plugins/subtac/subtac_plugin.cmxa OCAMLOPT -shared -o plugins/xml/xml_plugin.cmxs OCAMLOPT -a -o toplevel/toplevel.cmxa OCAMLOPT -a -o plugins/funind/recdef_plugin.cmxa OCAMLOPT -shared -o plugins/subtac/subtac_plugin.cmxs OCAMLOPT parsing/g_proofs.ml OCAMLOPT plugins/decl_mode/g_decl_mode.ml OCAMLOPT -shared -o plugins/funind/recdef_plugin.cmxs OCAMLOPT -a -o parsing/highparsing.cmxa COQMKTOP -o bin/coqtop.opt OCAMLOPT -a -o plugins/decl_mode/decl_mode_plugin.cmxa OCAMLOPT -shared -o plugins/decl_mode/decl_mode_plugin.cmxs strip bin/coqtop.opt COQC -nois theories/Init/Notations.v OCAMLOPT -o bin/coqc.opt cd bin && ln -sf coqtop.opt coqtop OCAMLOPT -o bin/coqide.opt strip bin/coqc.opt COQC -nois theories/Init/Logic.v Identifier 'IF' now a keyword Identifier 'exists2' now a keyword Identifier 'rew' now a keyword cd bin && ln -sf coqc.opt coqc COQC -nois theories/Init/Datatypes.v COQC -nois theories/Init/Logic_Type.v COQC -nois theories/Init/Peano.v COQC -nois theories/Init/Specif.v COQC -nois theories/Init/Wf.v COQC -nois theories/Init/Tactics.v COQC -nois theories/Init/Prelude.v BUILD states/initial.coq COQC theories/Logic/Berardi.v COQC theories/Arith/Le.v COQC theories/Logic/Decidable.v COQC theories/Program/Basics.v COQC theories/Program/Tactics.v COQC theories/Relations/Relation_Definitions.v COQC theories/Classes/Init.v strip bin/coqide.opt COQC theories/Logic/EqdepFacts.v COQC theories/Arith/EqNat.v COQC theories/Numbers/BinNums.v COQC theories/Bool/Bool.v COQC theories/Relations/Relation_Operators.v COQC theories/PArith/BinPosDef.v COQC theories/Bool/Sumbool.v COQC theories/Arith/Even.v COQC plugins/quote/Quote.v COQC theories/Logic/Hurkens.v COQC theories/Logic/RelationalChoice.v COQC theories/Logic/Eqdep.v COQC theories/Logic/FunctionalExtensionality.v COQC theories/Logic/ProofIrrelevanceFacts.v COQC theories/Logic/SetIsType.v COQC theories/Bool/BoolEq.v COQC theories/Bool/DecBool.v COQC theories/Bool/IfProp.v COQC plugins/omega/OmegaPlugin.v COQC theories/Sets/Relations_1.v COQC theories/Lists/Streams.v COQC theories/Sets/Ensembles.v COQC theories/Sets/Relations_1_facts.v COQC theories/Sets/Permut.v COQC theories/Sets/Relations_2.v COQC theories/Wellfounded/Disjoint_Union.v COQC theories/Wellfounded/Inclusion.v COQC theories/Wellfounded/Inverse_Image.v COQC theories/Wellfounded/Transitive_Closure.v COQC theories/Wellfounded/Well_Ordering.v COQC plugins/ring/LegacyRing_theory.v COQC theories/Unicode/Utf8_core.v Identifier 'λ' now a keyword COQC theories/Program/Utils.v COQC theories/Program/Combinators.v COQC plugins/micromega/CheckerMaker.v COQC plugins/setoid_ring/Algebra_syntax.v COQC plugins/extraction/ExtrOcamlBasic.v COQC theories/Arith/Lt.v COQC theories/Classes/RelationClasses.v COQC theories/Logic/Eqdep_dec.v COQC theories/Relations/Operators_Properties.v COQC theories/Logic/ClassicalFacts.v COQC theories/Logic/JMeq.v COQC theories/Logic/ProofIrrelevance.v COQC theories/Lists/StreamMemo.v COQC theories/Sets/Constructive_sets.v COQC theories/Sets/Partial_Order.v COQC theories/Sets/Relations_2_facts.v COQC theories/Sets/Relations_3.v COQC theories/Sets/Uniset.v COQC theories/Wellfounded/Lexicographic_Product.v COQC theories/Wellfounded/Union.v COQC plugins/ring/Ring_normalize.v COQC theories/Unicode/Utf8.v COQC theories/Program/Wf.v COQC theories/Program/Equality.v COQC theories/Arith/Plus.v COQC theories/Classes/Morphisms.v COQC theories/Arith/Minus.v COQC theories/Arith/Between.v COQC theories/Arith/Peano_dec.v COQC theories/Relations/Relations.v COQC theories/Logic/Classical_Prop.v COQC theories/Sets/Cpo.v COQC theories/Sets/Finite_sets.v COQC theories/Sets/Relations_3_facts.v COQC theories/Classes/RelationPairs.v COQC plugins/ring/Ring_abstract.v COQC theories/Program/Subset.v COQC theories/Arith/Gt.v COQC theories/Classes/Morphisms_Prop.v COQC theories/Classes/Equivalence.v COQC theories/Arith/Mult.v COQC theories/Logic/Classical_Pred_Type.v COQC theories/Sets/Powerset.v COQC plugins/ring/LegacyRing.v COQC theories/Arith/Compare_dec.v COQC theories/Classes/SetoidTactics.v COQC theories/Arith/Factorial.v COQC theories/Logic/Classical.v COQC theories/Logic/Classical_Pred_Set.v COQC theories/Logic/Classical_Type.v COQC theories/Arith/Bool_nat.v COQC theories/Sets/Powerset_facts.v COQC theories/Arith/Wf_nat.v COQC theories/Setoids/Setoid.v COQC theories/Arith/Arith_base.v COQC theories/Structures/Equalities.v COQC theories/Numbers/NumPrelude.v COQC theories/Arith/Div2.v COQC theories/Lists/List.v COQC theories/Logic/ClassicalUniqueChoice.v COQC theories/Arith/Euclid.v COQC theories/Vectors/Fin.v COQC theories/Sets/Classical_sets.v COQC theories/Sets/Multiset.v COQC plugins/funind/Recdef.v COQC plugins/ring/Setoid_ring_theory.v COQC theories/Structures/Orders.v COQC theories/Vectors/VectorDef.v COQC theories/Lists/ListSet.v COQC theories/Sorting/Sorted.v COQC theories/Sets/Powerset_Classical_facts.v COQC theories/Wellfounded/Lexicographic_Exponentiation.v COQC plugins/field/LegacyField_Compl.v COQC theories/Sorting/Permutation.v COQC theories/Numbers/NaryFunctions.v COQC plugins/micromega/Refl.v COQC plugins/ring/Setoid_ring_normalize.v COQC theories/Structures/OrdersTac.v COQC theories/Vectors/VectorSpec.v COQC theories/Lists/SetoidList.v COQC theories/Sets/Finite_sets_facts.v COQC theories/Wellfounded/Wellfounded.v COQC plugins/field/LegacyField_Theory.v COQC theories/Sorting/Mergesort.v COQC plugins/micromega/Tauto.v COQC plugins/ring/Setoid_ring.v COQC theories/Structures/OrdersFacts.v COQC theories/Vectors/Vector.v COQC theories/Lists/SetoidPermutation.v COQC theories/Sets/Image.v COQC theories/Structures/DecidableType.v COQC theories/Structures/OrderedType.v COQC theories/MSets/MSetInterface.v COQC theories/Structures/OrdersLists.v COQC theories/Structures/EqualitiesFacts.v COQC plugins/field/LegacyField_Tactic.v COQC theories/Sorting/Sorting.v COQC theories/Structures/GenericMinMax.v COQC theories/Bool/Bvector.v COQC theories/Sets/Infinite_sets.v COQC theories/FSets/FMapInterface.v COQC theories/Structures/OrderedTypeAlt.v COQC theories/FSets/FSetInterface.v COQC theories/Structures/OrdersAlt.v COQC theories/MSets/MSetList.v COQC theories/MSets/MSetWeakList.v COQC plugins/field/LegacyField.v COQC theories/Program/Syntax.v COQC theories/PArith/BinPos.v COQC theories/Numbers/NatInt/NZAxioms.v COQC theories/Sets/Integers.v COQC theories/FSets/FMapList.v COQC theories/FSets/FMapWeakList.v COQC theories/FSets/FSetBridge.v COQC theories/MSets/MSetPositive.v COQC theories/Program/Program.v COQC plugins/rtauto/Bintree.v COQC theories/Numbers/NatInt/NZBase.v COQC theories/NArith/BinNatDef.v COQC theories/PArith/Pnat.v Identifier 'mod' now a keyword COQC plugins/setoid_ring/BinList.v COQC theories/Lists/ListTactics.v COQC theories/PArith/POrderedType.v COQC theories/Classes/EquivDec.v COQC theories/Classes/Morphisms_Relations.v COQC theories/Classes/SetoidClass.v COQC plugins/rtauto/Rtauto.v COQC theories/Numbers/NatInt/NZAdd.v COQC theories/Numbers/NatInt/NZOrder.v COQC theories/PArith/PArith.v COQC theories/Numbers/NatInt/NZMul.v COQC theories/Numbers/NatInt/NZAddOrder.v COQC theories/Numbers/NatInt/NZMulOrder.v COQC theories/Numbers/NatInt/NZDomain.v COQC theories/Numbers/NatInt/NZParity.v COQC theories/Numbers/NatInt/NZPow.v COQC theories/Numbers/NatInt/NZSqrt.v COQC theories/Numbers/NatInt/NZDiv.v Identifier 'mod' now a keyword COQC theories/Numbers/NatInt/NZGcd.v COQC theories/Numbers/NatInt/NZProperties.v COQC theories/Numbers/NatInt/NZLog.v COQC theories/Numbers/NatInt/NZBits.v COQC theories/Numbers/Natural/Abstract/NAxioms.v COQC theories/Numbers/Integer/Abstract/ZAxioms.v COQC theories/Numbers/Natural/Abstract/NBase.v Identifier 'rem' now a keyword COQC theories/Numbers/Integer/Abstract/ZBase.v COQC theories/Numbers/Natural/Abstract/NAdd.v COQC theories/Numbers/Natural/Abstract/NIso.v COQC theories/Numbers/Natural/Abstract/NOrder.v COQC theories/Numbers/Integer/Abstract/ZAdd.v COQC theories/Numbers/Integer/Abstract/ZMul.v COQC theories/Numbers/Natural/Abstract/NAddOrder.v COQC theories/Numbers/Integer/Abstract/ZLt.v COQC theories/Numbers/Natural/Abstract/NMulOrder.v COQC theories/Numbers/Integer/Abstract/ZAddOrder.v COQC theories/Numbers/Natural/Abstract/NSub.v COQC theories/Numbers/Integer/Abstract/ZMulOrder.v COQC theories/Numbers/Natural/Abstract/NMaxMin.v COQC theories/Numbers/Natural/Abstract/NParity.v COQC theories/Numbers/Natural/Abstract/NSqrt.v COQC theories/Numbers/Natural/Abstract/NDiv.v COQC theories/Numbers/Natural/Abstract/NGcd.v COQC theories/Numbers/Integer/Abstract/ZMaxMin.v COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v COQC theories/Numbers/Integer/Abstract/ZParity.v COQC theories/Numbers/Natural/Abstract/NStrongRec.v COQC theories/Numbers/Natural/Abstract/NPow.v COQC theories/Numbers/Natural/Abstract/NLcm.v COQC theories/Numbers/Integer/Abstract/ZPow.v COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v COQC theories/Numbers/Integer/Abstract/ZDivFloor.v COQC theories/Numbers/Integer/Abstract/ZGcd.v COQC theories/Numbers/Integer/Abstract/ZBits.v COQC theories/Numbers/Integer/Abstract/ZDivEucl.v COQC theories/Numbers/Natural/Abstract/NDefOps.v COQC theories/Numbers/Natural/Abstract/NLog.v COQC theories/Numbers/Integer/Abstract/ZLcm.v COQC theories/Numbers/Natural/Abstract/NBits.v COQC theories/Numbers/Integer/Abstract/ZProperties.v COQC theories/Numbers/Natural/Abstract/NProperties.v COQC theories/NArith/BinNat.v COQC theories/Numbers/Natural/Peano/NPeano.v Identifier 'mod' now a keyword COQC theories/Arith/Min.v Identifier 'mod' now a keyword COQC theories/Arith/Max.v COQC plugins/setoid_ring/Ring_theory.v COQC theories/ZArith/BinIntDef.v COQC theories/Arith/Compare.v COQC theories/NArith/Ndiv_def.v COQC theories/NArith/Nsqrt_def.v COQC theories/NArith/Ngcd_def.v COQC theories/MSets/MSetGenTree.v COQC theories/Numbers/Natural/Binary/NBinary.v COQC plugins/setoid_ring/Ring_equiv.v COQC theories/NArith/Nnat.v COQC theories/ZArith/BinInt.v COQC theories/NArith/Ndigits.v COQC theories/Strings/Ascii.v COQC theories/MSets/MSetRBT.v COQC theories/Numbers/Natural/SpecViaZ/NSig.v COQC theories/Numbers/Integer/SpecViaZ/ZSig.v COQC theories/Numbers/Integer/Binary/ZBinary.v COQC plugins/micromega/Env.v COQC plugins/setoid_ring/Ring_polynom.v COQC theories/ZArith/Zcompare.v COQC theories/ZArith/Zeven.v COQC theories/ZArith/Znat.v COQC theories/ZArith/Zpow_def.v COQC plugins/omega/OmegaLemmas.v COQC theories/ZArith/Zpow_alt.v COQC theories/ZArith/ZOdiv_def.v COQC theories/ZArith/Zeuclid.v COQC plugins/micromega/EnvRing.v COQC theories/ZArith/Zorder.v COQC theories/ZArith/Zminmax.v COQC theories/ZArith/Zmin.v COQC theories/ZArith/Zmax.v COQC theories/ZArith/ZArith_dec.v COQC theories/ZArith/auxiliary.v COQC theories/ZArith/Zbool.v COQC theories/ZArith/Zmisc.v COQC theories/ZArith/Zabs.v COQC theories/ZArith/Wf_Z.v COQC theories/ZArith/Zhints.v COQC theories/ZArith/ZArith_base.v COQC plugins/setoid_ring/InitialRing.v COQC plugins/romega/ReflOmegaCore.v COQC theories/Reals/Rdefinitions.v COQC plugins/setoid_ring/Ncring.v COQC plugins/setoid_ring/Ring_tac.v COQC theories/Reals/Raxioms.v COQC theories/Reals/Rpow_def.v COQC plugins/setoid_ring/Ncring_polynom.v COQC plugins/setoid_ring/Ring_base.v COQC theories/Reals/LegacyRfield.v COQC plugins/setoid_ring/Ring.v COQC plugins/setoid_ring/ArithRing.v COQC plugins/setoid_ring/NArithRing.v COQC plugins/setoid_ring/ZArithRing.v COQC plugins/setoid_ring/Field_theory.v COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v COQC plugins/micromega/OrderedRing.v COQC theories/Arith/Arith.v COQC theories/NArith/NArith.v COQC theories/NArith/Ndec.v COQC theories/NArith/Ndist.v COQC plugins/omega/PreOmega.v COQC theories/Strings/String.v COQC plugins/setoid_ring/Field_tac.v COQC theories/Classes/SetoidDec.v COQC plugins/micromega/RingMicromega.v COQC plugins/ring/LegacyArithRing.v COQC plugins/ring/LegacyNArithRing.v COQC plugins/ring/LegacyZArithRing.v COQC plugins/extraction/ExtrOcamlNatInt.v COQC plugins/extraction/ExtrOcamlNatBigInt.v COQC plugins/extraction/ExtrOcamlString.v COQC theories/Logic/ChoiceFacts.v COQC theories/Logic/ConstructiveEpsilon.v COQC theories/Bool/Zerob.v COQC plugins/omega/Omega.v COQC plugins/romega/ROmega.v COQC plugins/setoid_ring/Field.v COQC theories/Sorting/PermutSetoid.v COQC plugins/setoid_ring/Ncring_initial.v COQC theories/Logic/ClassicalChoice.v COQC theories/Logic/Description.v COQC theories/Logic/ClassicalEpsilon.v COQC theories/Logic/Diaconescu.v COQC theories/Logic/Epsilon.v COQC theories/Logic/IndefiniteDescription.v COQC theories/ZArith/Zcomplements.v COQC theories/ZArith/Zsqrt_compat.v COQC theories/ZArith/Zwf.v COQC plugins/setoid_ring/RealField.v COQC theories/Sorting/Heap.v COQC theories/Sorting/PermutEq.v COQC theories/Logic/ClassicalDescription.v COQC theories/ZArith/Zpower.v COQC theories/ZArith/Zdiv.v COQC theories/ZArith/Zlogarithm.v COQC theories/Reals/RIneq.v COQC theories/ZArith/ZArith.v COQC theories/ZArith/Znumtheory.v COQC theories/ZArith/Zquot.v COQC theories/Structures/OrderedTypeEx.v COQC theories/Structures/OrdersEx.v COQC theories/Reals/DiscrR.v COQC theories/QArith/QArith_base.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v COQC theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v COQC theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v COQC plugins/micromega/ZCoeff.v COQC plugins/micromega/VarMap.v COQC plugins/setoid_ring/Ncring_tac.v COQC plugins/extraction/ExtrOcamlIntConv.v COQC plugins/extraction/ExtrOcamlBigIntConv.v COQC plugins/extraction/ExtrOcamlZInt.v COQC plugins/extraction/ExtrOcamlZBigInt.v COQC theories/ZArith/Int.v COQC theories/ZArith/Zdigits.v COQC theories/ZArith/Zgcd_alt.v COQC theories/ZArith/ZOdiv.v COQC theories/ZArith/Zpow_facts.v COQC theories/FSets/FMapAVL.v COQC theories/Structures/DecidableTypeEx.v COQC theories/FSets/FMapPositive.v COQC theories/FSets/FSetFacts.v COQC theories/MSets/MSetFacts.v COQC theories/MSets/MSetAVL.v COQC theories/FSets/FSetPositive.v COQC theories/FSets/FSetDecide.v COQC theories/MSets/MSetDecide.v COQC theories/Reals/Rbase.v COQC theories/QArith/Qfield.v COQC theories/QArith/Qreduction.v COQC theories/QArith/Qreals.v COQC theories/QArith/QOrderedType.v COQC theories/Numbers/BigNumPrelude.v COQC theories/Numbers/Cyclic/Int31/Int31.v COQC plugins/setoid_ring/Cring.v COQC theories/FSets/FMapFacts.v COQC theories/FSets/FMapFullAVL.v COQC theories/FSets/FSetCompat.v COQC theories/FSets/FSetProperties.v COQC theories/FSets/FSetList.v COQC theories/FSets/FSetWeakList.v COQC theories/FSets/FSetToFiniteSet.v COQC theories/MSets/MSetProperties.v COQC theories/Reals/R_Ifp.v COQC plugins/fourier/Fourier_util.v COQC theories/Reals/SplitRmult.v COQC theories/Reals/ROrderedType.v COQC theories/QArith/Qring.v COQC theories/QArith/Qpower.v COQC theories/QArith/Qminmax.v COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v COQC theories/Numbers/Integer/BigZ/ZMake.v COQC plugins/setoid_ring/Integral_domain.v COQC theories/FSets/FMaps.v COQC theories/FSets/FSetAVL.v COQC theories/FSets/FSetEqProperties.v COQC theories/MSets/MSetEqProperties.v COQC theories/MSets/MSetToFiniteSet.v COQC plugins/fourier/Fourier.v COQC theories/QArith/QArith.v COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v COQC theories/Numbers/Cyclic/Int31/Cyclic31.v COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v COQC theories/Numbers/Rational/SpecViaQ/QSig.v COQC plugins/micromega/ZMicromega.v COQC plugins/micromega/QMicromega.v COQC plugins/micromega/RMicromega.v COQC plugins/setoid_ring/Rings_Z.v COQC plugins/setoid_ring/Rings_Q.v COQC theories/FSets/FSets.v COQC theories/MSets/MSets.v COQC theories/Reals/Rbasic_fun.v COQC theories/QArith/Qabs.v COQC theories/QArith/Qcanon.v COQC theories/QArith/Qround.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v COQC theories/Numbers/Cyclic/Int31/Ring31.v COQC theories/Numbers/Rational/BigQ/QMake.v COQC plugins/micromega/Psatz.v COQC theories/Reals/R_sqr.v COQC theories/Reals/SplitAbsolu.v COQC theories/Reals/ArithProp.v COQC theories/Reals/Rminmax.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v COQC theories/Reals/Rfunctions.v COQC theories/Numbers/Natural/BigN/Nbasic.v COQC theories/Reals/Rseries.v COQC theories/Reals/Rlimit.v COQC theories/Reals/RList.v COQC theories/Numbers/Natural/BigN/NMake_gen.v COQC theories/Reals/SeqProp.v COQC theories/Reals/Rderiv.v COQC theories/Reals/Rcomplete.v COQC theories/Reals/Ranalysis1.v Identifier 'o' now a keyword COQC theories/Reals/PartSum.v COQC theories/Reals/Ranalysis2.v COQC theories/Reals/Rtopology.v COQC theories/Reals/Alembert.v COQC theories/Reals/AltSeries.v COQC theories/Reals/Binomial.v COQC theories/Reals/Cauchy_prod.v COQC theories/Reals/Rsigma.v COQC theories/Reals/Rprod.v COQC theories/Reals/Ranalysis3.v COQC theories/Reals/MVT.v COQC theories/Reals/SeqSeries.v COQC theories/Reals/Rtrigo_fun.v COQC theories/Reals/Rsqrt_def.v COQC theories/Reals/PSeries_reg.v COQC theories/Reals/R_sqrt.v COQC theories/Reals/Rtrigo_def.v COQC theories/Reals/Sqrt_reg.v COQC theories/Reals/Cos_rel.v COQC theories/Reals/Rtrigo_alt.v COQC theories/Numbers/Natural/BigN/NMake.v COQC theories/Reals/Cos_plus.v COQC theories/Reals/Rtrigo1.v COQC theories/Reals/Exp_prop.v COQC theories/Reals/Rtrigo_reg.v COQC theories/Reals/Rtrigo_calc.v COQC theories/Reals/Rgeom.v COQC theories/Reals/Ranalysis4.v COQC theories/Numbers/Natural/BigN/BigN.v COQC theories/Reals/Rpower.v COQC theories/Numbers/Integer/BigZ/BigZ.v COQC theories/Reals/Ranalysis_reg.v COQC theories/Reals/RiemannInt_SF.v COQC theories/Numbers/Rational/BigQ/BigQ.v COQC theories/Reals/RiemannInt.v COQC theories/Reals/Ranalysis5.v COQC theories/Reals/Rlogic.v COQC theories/Reals/Ratan.v COQC theories/Reals/Machin.v COQC theories/Reals/Rtrigo.v COQC theories/Reals/Ranalysis.v COQC theories/Reals/NewtonInt.v COQC theories/Reals/Integration.v COQC theories/Reals/Reals.v COQC plugins/setoid_ring/Rings_R.v COQC plugins/nsatz/Nsatz.v gmake[1]: Leaving directory `/scratch/lang/coq/work/coq-8.4pl1' => Unwrapping files-to-be-installed.