=> Bootstrap dependency digest>=20010302: found digest-20111104
=> Bootstrap dependency fetch-[0-9]*: found fetch-1.7
===> Building for coq-8.3pl1nb11
*****************************************************
*****************************************************
****************** Entering stage1 ******************
*****************************************************
*****************************************************
/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage1 "stage1"
make[1]: Entering directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
               -e '/^}/q' kernel/byterun/coq_instruct.h > \
                          kernel/byterun/coq_jumptbl.h \
  || ( RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV} )
OCAMLLEX  ide/utf8_convert.mll
OCAMLLEX  ide/coq_lex.mll
OCAMLLEX  ide/highlight.mll
OCAMLLEX  ide/config_lexer.mll
OCAMLLEX  tools/gallina_lexer.mll
13 states, 332 transitions, table size 1406 bytes
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX  tools/coqdep_lexer.mll
OCAMLLEX  tools/coqdoc/cpretty.mll
190 states, 498 transitions, table size 3132 bytes
OCAMLLEX  tools/coqwc.mll
200 states, 5470 transitions, table size 23080 bytes
2243 additional bytes used for bindings
230 states, 833 transitions, table size 4712 bytes
OCAMLLEX  plugins/dp/dp_zenon.mll
OCAMLLEX  dev/ocamlweb-doc/lex.mll
85 states, 637 transitions, table size 3058 bytes
1881 additional bytes used for bindings
OCAMLYACC ide/config_parser.mly
OCAMLYACC dev/ocamlweb-doc/syntax.mly
3 shift/reduce conflicts.
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} )
"ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > theories/Numbers/Natural/BigN/NMake_gen.v
99 states, 6415 transitions, table size 26254 bytes
TOUCH     parsing/g_ltac.ml
TOUCH     parsing/g_xml.ml
TOUCH     parsing/vernacextend.ml
TOUCH     parsing/g_prim.ml
TOUCH     parsing/g_constr.ml
TOUCH     parsing/g_decl_mode.ml
TOUCH     parsing/g_vernac.ml
TOUCH     parsing/argextend.ml
TOUCH     parsing/g_tactic.ml
TOUCH     parsing/lexer.ml
TOUCH     parsing/tacextend.ml
TOUCH     parsing/q_coqast.ml
TOUCH     parsing/q_constr.ml
TOUCH     parsing/pcoq.ml
TOUCH     parsing/g_proofs.ml
TOUCH     parsing/q_util.ml
TOUCH     toplevel/whelp.ml
TOUCH     toplevel/mltop.ml
TOUCH     tools/coq_tex.ml
TOUCH     tools/coq_makefile.ml
TOUCH     lib/compat.ml
TOUCH     lib/pp.ml
TOUCH     lib/refutpat.ml
TOUCH     plugins/rtauto/g_rtauto.ml
TOUCH     plugins/nsatz/nsatz.ml
TOUCH     plugins/field/field.ml
TOUCH     plugins/setoid_ring/newring.ml
TOUCH     plugins/extraction/g_extraction.ml
TOUCH     plugins/dp/g_dp.ml
TOUCH     plugins/quote/g_quote.ml
TOUCH     plugins/firstorder/g_ground.ml
TOUCH     plugins/subtac/g_subtac.ml
TOUCH     plugins/romega/g_romega.ml
TOUCH     plugins/ring/g_ring.ml
TOUCH     plugins/cc/g_congruence.ml
TOUCH     plugins/fourier/g_fourier.ml
TOUCH     plugins/xml/proofTree2Xml.ml
TOUCH     plugins/xml/dumptree.ml
TOUCH     plugins/xml/xmlentries.ml
TOUCH     plugins/xml/xml.ml
TOUCH     plugins/xml/acic2Xml.ml
TOUCH     plugins/micromega/g_micromega.ml
TOUCH     plugins/omega/g_omega.ml
TOUCH     plugins/funind/g_indfun.ml
TOUCH     tactics/hipattern.ml
TOUCH     tactics/rewrite.ml
TOUCH     tactics/class_tactics.ml
TOUCH     tactics/eauto.ml
TOUCH     tactics/tauto.ml
TOUCH     tactics/eqdecide.ml
TOUCH     tactics/extratactics.ml
TOUCH     tactics/extraargs.ml
CAMLP4DEPS parsing/q_constr.ml4
CAMLP4DEPS parsing/q_coqast.ml4
CAMLP4DEPS parsing/lexer.ml4
CAMLP4DEPS parsing/g_constr.ml4
CAMLP4DEPS parsing/g_ltac.ml4
CAMLP4DEPS parsing/g_tactic.ml4
CAMLP4DEPS parsing/g_prim.ml4
CAMLP4DEPS parsing/vernacextend.ml4
CAMLP4DEPS parsing/tacextend.ml4
CAMLP4DEPS parsing/argextend.ml4
CAMLP4DEPS parsing/pcoq.ml4
CAMLP4DEPS parsing/q_util.ml4
CAMLP4DEPS lib/pp.ml4
CAMLP4DEPS lib/compat.ml4
OCAMLDEP  checker/check_stat.mli
OCAMLDEP  checker/term.mli
OCAMLDEP  checker/closure.mli
OCAMLDEP  checker/subtyping.mli
OCAMLDEP  checker/type_errors.mli
OCAMLDEP  checker/declarations.mli
OCAMLDEP  checker/typeops.mli
OCAMLDEP  checker/modops.mli
OCAMLDEP  checker/reduction.mli
OCAMLDEP  checker/inductive.mli
OCAMLDEP  checker/environ.mli
OCAMLDEP  checker/safe_typing.mli
OCAMLDEP  checker/indtypes.mli
OCAMLDEP  checker/checker.ml
OCAMLDEP  checker/inductive.ml
OCAMLDEP  checker/typeops.ml
OCAMLDEP  checker/environ.ml
OCAMLDEP  checker/main.ml
OCAMLDEP  checker/validate.ml
OCAMLDEP  checker/reduction.ml
OCAMLDEP  checker/mod_checking.ml
OCAMLDEP  checker/subtyping.ml
OCAMLDEP  checker/modops.ml
OCAMLDEP  checker/indtypes.ml
OCAMLDEP  checker/check_stat.ml
OCAMLDEP  checker/check.ml
OCAMLDEP  checker/closure.ml
OCAMLDEP  checker/safe_typing.ml
OCAMLDEP  checker/type_errors.ml
OCAMLDEP  checker/declarations.ml
OCAMLDEP  checker/term.ml
CAMLP4DEPS tactics/extraargs.ml4
CAMLP4DEPS tactics/extratactics.ml4
CAMLP4DEPS tactics/eqdecide.ml4
CAMLP4DEPS tactics/tauto.ml4
CAMLP4DEPS tactics/eauto.ml4
CAMLP4DEPS tactics/class_tactics.ml4
CAMLP4DEPS tactics/rewrite.ml4
CAMLP4DEPS tactics/hipattern.ml4
CAMLP4DEPS plugins/funind/g_indfun.ml4
CAMLP4DEPS plugins/omega/g_omega.ml4
CAMLP4DEPS plugins/micromega/g_micromega.ml4
CAMLP4DEPS plugins/xml/acic2Xml.ml4
CAMLP4DEPS plugins/xml/xml.ml4
CAMLP4DEPS plugins/xml/xmlentries.ml4
CAMLP4DEPS plugins/xml/dumptree.ml4
CAMLP4DEPS plugins/xml/proofTree2Xml.ml4
CAMLP4DEPS plugins/fourier/g_fourier.ml4
CAMLP4DEPS plugins/cc/g_congruence.ml4
CAMLP4DEPS plugins/ring/g_ring.ml4
CAMLP4DEPS plugins/romega/g_romega.ml4
CAMLP4DEPS plugins/subtac/g_subtac.ml4
CAMLP4DEPS plugins/firstorder/g_ground.ml4
CAMLP4DEPS plugins/quote/g_quote.ml4
CAMLP4DEPS plugins/dp/g_dp.ml4
CAMLP4DEPS plugins/extraction/g_extraction.ml4
CAMLP4DEPS plugins/setoid_ring/newring.ml4
CAMLP4DEPS plugins/field/field.ml4
CAMLP4DEPS plugins/nsatz/nsatz.ml4
CAMLP4DEPS plugins/rtauto/g_rtauto.ml4
CAMLP4DEPS lib/refutpat.ml4
CAMLP4DEPS tools/coq_makefile.ml4
CAMLP4DEPS tools/coq_tex.ml4
CAMLP4DEPS toplevel/mltop.ml4
CAMLP4DEPS toplevel/whelp.ml4
CAMLP4DEPS parsing/g_proofs.ml4
CAMLP4DEPS parsing/g_vernac.ml4
CAMLP4DEPS parsing/g_decl_mode.ml4
CAMLP4DEPS parsing/g_xml.ml4
CCDEP     kernel/byterun/coq_fix_code.c
CCDEP     kernel/byterun/coq_interp.c
2130 states, 6466 transitions, table size 38644 bytes
457 states, 31161 transitions, table size 127386 bytes
455 states, 31494 transitions, table size 128706 bytes
CCDEP     kernel/byterun/coq_values.c
CCDEP     kernel/byterun/coq_memory.c
OCAMLDEP  kernel/csymtable.mli
OCAMLDEP  kernel/mod_subst.mli
OCAMLDEP  kernel/term.mli
OCAMLDEP  kernel/closure.mli
OCAMLDEP  kernel/subtyping.mli
OCAMLDEP  kernel/type_errors.mli
OCAMLDEP  kernel/cbytegen.mli
OCAMLDEP  kernel/cooking.mli
OCAMLDEP  kernel/declarations.mli
OCAMLDEP  kernel/vm.mli
OCAMLDEP  kernel/names.mli
OCAMLDEP  kernel/cbytecodes.mli
OCAMLDEP  kernel/retroknowledge.mli
OCAMLDEP  kernel/conv_oracle.mli
OCAMLDEP  kernel/mod_typing.mli
OCAMLDEP  kernel/entries.mli
OCAMLDEP  kernel/pre_env.mli
OCAMLDEP  kernel/typeops.mli
OCAMLDEP  kernel/univ.mli
OCAMLDEP  kernel/esubst.mli
OCAMLDEP  kernel/modops.mli
OCAMLDEP  kernel/reduction.mli
OCAMLDEP  kernel/inductive.mli
OCAMLDEP  kernel/environ.mli
OCAMLDEP  kernel/term_typing.mli
OCAMLDEP  kernel/safe_typing.mli
OCAMLDEP  kernel/cemitcodes.mli
OCAMLDEP  kernel/vconv.mli
OCAMLDEP  kernel/sign.mli
OCAMLDEP  kernel/indtypes.mli
OCAMLDEP  parsing/printmod.mli
OCAMLDEP  parsing/egrammar.mli
OCAMLDEP  parsing/pcoq.mli
OCAMLDEP  parsing/extend.mli
OCAMLDEP  parsing/q_util.mli
OCAMLDEP  parsing/prettyp.mli
OCAMLDEP  parsing/lexer.mli
OCAMLDEP  parsing/printer.mli
OCAMLDEP  parsing/extrawit.mli
OCAMLDEP  parsing/ppdecl_proof.mli
OCAMLDEP  parsing/g_zsyntax.mli
OCAMLDEP  parsing/ppvernac.mli
OCAMLDEP  parsing/g_intsyntax.mli
OCAMLDEP  parsing/tactic_printer.mli
OCAMLDEP  parsing/ppconstr.mli
OCAMLDEP  parsing/g_natsyntax.mli
OCAMLDEP  parsing/pptactic.mli
OCAMLDEP  kernel/copcodes.ml
OCAMLDEP  scripts/tolink.ml
OCAMLDEP  dev/ocamlweb-doc/syntax.ml
OCAMLDEP  ide/config_parser.ml
OCAMLDEP  plugins/dp/dp_zenon.ml
OCAMLDEP  dev/ocamlweb-doc/lex.ml
OCAMLDEP  tools/coqwc.ml
OCAMLDEP  tools/coqdoc/cpretty.ml
OCAMLDEP  tools/coqdep_lexer.ml
OCAMLDEP  tools/gallina_lexer.ml
OCAMLDEP  ide/config_lexer.ml
OCAMLDEP  ide/highlight.ml
OCAMLDEP  ide/coq_lex.ml
OCAMLDEP  ide/utf8_convert.ml
OCAMLDEP  interp/genarg.ml
OCAMLDEP  interp/topconstr.ml
OCAMLDEP  interp/constrextern.ml
OCAMLDEP  interp/syntax_def.ml
OCAMLDEP  interp/ppextend.ml
OCAMLDEP  interp/modintern.ml
OCAMLDEP  interp/coqlib.ml
OCAMLDEP  interp/notation.ml
OCAMLDEP  interp/implicit_quantifiers.ml
OCAMLDEP  interp/smartlocate.ml
OCAMLDEP  interp/dumpglob.ml
OCAMLDEP  interp/reserve.ml
OCAMLDEP  interp/constrintern.ml
OCAMLDEP  tactics/tacticals.ml
OCAMLDEP  tactics/termdn.ml
OCAMLDEP  tactics/tacinterp.ml
OCAMLDEP  tactics/inv.ml
OCAMLDEP  tactics/tactic_option.ml
OCAMLDEP  tactics/contradiction.ml
OCAMLDEP  tactics/elim.ml
OCAMLDEP  tactics/decl_proof_instr.ml
OCAMLDEP  tactics/tactics.ml
OCAMLDEP  tactics/eqschemes.ml
OCAMLDEP  tactics/hiddentac.ml
OCAMLDEP  tactics/decl_interp.ml
OCAMLDEP  tactics/equality.ml
OCAMLDEP  tactics/refine.ml
OCAMLDEP  tactics/elimschemes.ml
OCAMLDEP  tactics/leminv.ml
OCAMLDEP  tactics/btermdn.ml
OCAMLDEP  tactics/autorewrite.ml
OCAMLDEP  tactics/evar_tactics.ml
OCAMLDEP  tactics/nbtermdn.ml
OCAMLDEP  tactics/dhyp.ml
OCAMLDEP  tactics/dn.ml
OCAMLDEP  tactics/auto.ml
OCAMLDEP  pretyping/retyping.ml
OCAMLDEP  pretyping/classops.ml
OCAMLDEP  pretyping/typeclasses_errors.ml
OCAMLDEP  pretyping/evd.ml
OCAMLDEP  pretyping/reductionops.ml
OCAMLDEP  pretyping/rawterm.ml
OCAMLDEP  pretyping/vnorm.ml
OCAMLDEP  pretyping/typing.ml
OCAMLDEP  pretyping/recordops.ml
OCAMLDEP  pretyping/cbv.ml
OCAMLDEP  pretyping/cases.ml
OCAMLDEP  pretyping/evarconv.ml
OCAMLDEP  pretyping/indrec.ml
OCAMLDEP  pretyping/detyping.ml
OCAMLDEP  pretyping/namegen.ml
OCAMLDEP  pretyping/inductiveops.ml
OCAMLDEP  pretyping/evarutil.ml
OCAMLDEP  pretyping/clenv.ml
OCAMLDEP  pretyping/term_dnet.ml
OCAMLDEP  pretyping/unification.ml
OCAMLDEP  pretyping/matching.ml
OCAMLDEP  pretyping/pretype_errors.ml
OCAMLDEP  pretyping/typeclasses.ml
OCAMLDEP  pretyping/pattern.ml
OCAMLDEP  pretyping/coercion.ml
OCAMLDEP  pretyping/tacred.ml
OCAMLDEP  pretyping/termops.ml
OCAMLDEP  pretyping/pretyping.ml
OCAMLDEP  theories/Numbers/Natural/BigN/NMake_gen.ml
OCAMLDEP  dev/ocamlweb-doc/parse.ml
OCAMLDEP  dev/ocamlweb-doc/ast.ml
OCAMLDEP  dev/db_printers.ml
OCAMLDEP  dev/vm_printers.ml
OCAMLDEP  dev/top_printers.ml
OCAMLDEP  library/nametab.ml
OCAMLDEP  library/lib.ml
OCAMLDEP  library/libnames.ml
OCAMLDEP  library/library.ml
OCAMLDEP  library/global.ml
OCAMLDEP  library/libobject.ml
OCAMLDEP  library/impargs.ml
OCAMLDEP  library/nameops.ml
OCAMLDEP  library/heads.ml
OCAMLDEP  library/declaremods.ml
OCAMLDEP  library/dischargedhypsmap.ml
OCAMLDEP  library/goptions.ml
OCAMLDEP  library/decl_kinds.ml
OCAMLDEP  library/summary.ml
OCAMLDEP  library/declare.ml
OCAMLDEP  library/decls.ml
OCAMLDEP  library/states.ml
OCAMLDEP  plugins/funind/invfun.ml
OCAMLDEP  plugins/funind/indfun_common.ml
OCAMLDEP  plugins/funind/functional_principles_proofs.ml
OCAMLDEP  plugins/funind/rawterm_to_relation.ml
OCAMLDEP  plugins/funind/recdef.ml
OCAMLDEP  plugins/funind/functional_principles_types.ml
OCAMLDEP  plugins/funind/indfun.ml
OCAMLDEP  plugins/funind/merge.ml
OCAMLDEP  plugins/funind/rawtermops.ml
OCAMLDEP  plugins/omega/coq_omega.ml
OCAMLDEP  plugins/omega/omega.ml
OCAMLDEP  plugins/micromega/mfourier.ml
OCAMLDEP  plugins/micromega/csdpcert.ml
OCAMLDEP  plugins/micromega/mutils.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/certificate.ml
OCAMLDEP  plugins/micromega/persistent_cache.ml
OCAMLDEP  plugins/micromega/sos.ml
OCAMLDEP  plugins/xml/unshare.ml
OCAMLDEP  plugins/xml/acic.ml
OCAMLDEP  plugins/xml/proof2aproof.ml
OCAMLDEP  plugins/xml/xmlcommand.ml
OCAMLDEP  plugins/xml/cic2acic.ml
OCAMLDEP  plugins/xml/doubleTypeInference.ml
OCAMLDEP  plugins/xml/cic2Xml.ml
OCAMLDEP  plugins/fourier/fourier.ml
OCAMLDEP  plugins/fourier/fourierR.ml
OCAMLDEP  plugins/cc/cctac.ml
OCAMLDEP  plugins/cc/ccalgo.ml
OCAMLDEP  plugins/cc/ccproof.ml
OCAMLDEP  plugins/ring/ring.ml
OCAMLDEP  plugins/syntax/z_syntax.ml
OCAMLDEP  plugins/syntax/numbers_syntax.ml
OCAMLDEP  plugins/syntax/string_syntax.ml
OCAMLDEP  plugins/syntax/nat_syntax.ml
OCAMLDEP  plugins/syntax/ascii_syntax.ml
OCAMLDEP  plugins/syntax/r_syntax.ml
OCAMLDEP  plugins/romega/refl_omega.ml
OCAMLDEP  plugins/romega/const_omega.ml
OCAMLDEP  plugins/subtac/subtac.ml
OCAMLDEP  plugins/subtac/subtac_classes.ml
OCAMLDEP  plugins/subtac/subtac_pretyping_F.ml
OCAMLDEP  plugins/subtac/subtac_cases.ml
OCAMLDEP  plugins/subtac/subtac_utils.ml
OCAMLDEP  plugins/subtac/eterm.ml
OCAMLDEP  plugins/subtac/subtac_obligations.ml
OCAMLDEP  plugins/subtac/subtac_errors.ml
OCAMLDEP  plugins/subtac/subtac_command.ml
OCAMLDEP  plugins/subtac/subtac_coercion.ml
OCAMLDEP  plugins/subtac/subtac_pretyping.ml
OCAMLDEP  plugins/firstorder/formula.ml
OCAMLDEP  plugins/firstorder/unify.ml
OCAMLDEP  plugins/firstorder/rules.ml
OCAMLDEP  plugins/firstorder/ground.ml
OCAMLDEP  plugins/firstorder/instances.ml
OCAMLDEP  plugins/firstorder/sequent.ml
OCAMLDEP  plugins/quote/quote.ml
OCAMLDEP  plugins/dp/dp.ml
OCAMLDEP  plugins/dp/dp_why.ml
OCAMLDEP  plugins/extraction/mlutil.ml
OCAMLDEP  plugins/extraction/modutil.ml
OCAMLDEP  plugins/extraction/extract_env.ml
OCAMLDEP  plugins/extraction/ocaml.ml
OCAMLDEP  plugins/extraction/scheme.ml
OCAMLDEP  plugins/extraction/big.ml
OCAMLDEP  plugins/extraction/haskell.ml
OCAMLDEP  plugins/extraction/common.ml
OCAMLDEP  plugins/extraction/table.ml
OCAMLDEP  plugins/extraction/extraction.ml
OCAMLDEP  plugins/nsatz/utile.ml
OCAMLDEP  plugins/nsatz/polynom.ml
OCAMLDEP  plugins/nsatz/ideal.ml
OCAMLDEP  plugins/rtauto/proof_search.ml
OCAMLDEP  plugins/rtauto/refl_tauto.ml
OCAMLDEP  lib/gmapl.ml
OCAMLDEP  lib/system.ml
OCAMLDEP  lib/flags.ml
OCAMLDEP  lib/dyn.ml
OCAMLDEP  lib/edit.ml
OCAMLDEP  lib/fmap.ml
OCAMLDEP  lib/heap.ml
OCAMLDEP  lib/profile.ml
OCAMLDEP  lib/gset.ml
OCAMLDEP  lib/unicodetable.ml
OCAMLDEP  lib/predicate.ml
OCAMLDEP  lib/rtree.ml
OCAMLDEP  lib/tries.ml
OCAMLDEP  lib/tlm.ml
OCAMLDEP  lib/fset.ml
OCAMLDEP  lib/dnet.ml
OCAMLDEP  lib/option.ml
OCAMLDEP  lib/gmap.ml
OCAMLDEP  lib/util.ml
OCAMLDEP  lib/explore.ml
OCAMLDEP  lib/pp_control.ml
OCAMLDEP  lib/envars.ml
OCAMLDEP  lib/hashcons.ml
OCAMLDEP  lib/bigint.ml
OCAMLDEP  lib/segmenttree.ml
OCAMLDEP  lib/bstack.ml
OCAMLDEP  config/coq_config.ml
OCAMLDEP  myocamlbuild.ml
OCAMLDEP  tools/coqdep.ml
OCAMLDEP  tools/coqdep_boot.ml
OCAMLDEP  tools/coqdoc/alpha.ml
OCAMLDEP  tools/coqdoc/index.ml
OCAMLDEP  tools/coqdoc/output.ml
OCAMLDEP  tools/coqdoc/main.ml
OCAMLDEP  tools/coqdoc/tokens.ml
OCAMLDEP  tools/coqdoc/cdglobals.ml
OCAMLDEP  tools/coqdep_common.ml
OCAMLDEP  tools/gallina.ml
OCAMLDEP  proofs/pfedit.ml
OCAMLDEP  proofs/refiner.ml
OCAMLDEP  proofs/redexpr.ml
OCAMLDEP  proofs/decl_mode.ml
OCAMLDEP  proofs/tacmach.ml
OCAMLDEP  proofs/proof_type.ml
OCAMLDEP  proofs/proof_trees.ml
OCAMLDEP  proofs/tactic_debug.ml
OCAMLDEP  proofs/tacexpr.ml
OCAMLDEP  proofs/evar_refiner.ml
OCAMLDEP  proofs/clenvtac.ml
OCAMLDEP  proofs/logic.ml
OCAMLDEP  ide/ideutils.ml
OCAMLDEP  ide/coq.ml
OCAMLDEP  ide/preferences.ml
OCAMLDEP  ide/utils/configwin_types.ml
OCAMLDEP  ide/utils/config_file.ml
OCAMLDEP  ide/utils/configwin.ml
OCAMLDEP  ide/utils/editable_cells.ml
OCAMLDEP  ide/utils/configwin_ihm.ml
OCAMLDEP  ide/utils/configwin_keys.ml
OCAMLDEP  ide/utils/okey.ml
OCAMLDEP  ide/utils/configwin_messages.ml
OCAMLDEP  ide/gtk_parsing.ml
OCAMLDEP  ide/command_windows.ml
OCAMLDEP  ide/tags.ml
OCAMLDEP  ide/coq_commands.ml
OCAMLDEP  ide/coq_tactics.ml
OCAMLDEP  ide/coqide.ml
OCAMLDEP  ide/undo.ml
OCAMLDEP  ide/typed_notebook.ml
OCAMLDEP  toplevel/auto_ind_decl.ml
OCAMLDEP  toplevel/coqtop.ml
OCAMLDEP  toplevel/usage.ml
OCAMLDEP  toplevel/vernacexpr.ml
OCAMLDEP  toplevel/coqinit.ml
OCAMLDEP  toplevel/search.ml
OCAMLDEP  toplevel/ind_tables.ml
OCAMLDEP  toplevel/metasyntax.ml
OCAMLDEP  toplevel/lemmas.ml
OCAMLDEP  toplevel/vernac.ml
OCAMLDEP  toplevel/toplevel.ml
OCAMLDEP  toplevel/himsg.ml
OCAMLDEP  toplevel/class.ml
OCAMLDEP  toplevel/indschemes.ml
OCAMLDEP  toplevel/discharge.ml
OCAMLDEP  toplevel/libtypes.ml
OCAMLDEP  toplevel/vernacinterp.ml
OCAMLDEP  toplevel/record.ml
OCAMLDEP  toplevel/command.ml
OCAMLDEP  toplevel/vernacentries.ml
OCAMLDEP  toplevel/classes.ml
OCAMLDEP  toplevel/autoinstance.ml
OCAMLDEP  toplevel/cerrors.ml
OCAMLDEP  kernel/entries.ml
OCAMLDEP  kernel/names.ml
OCAMLDEP  kernel/sign.ml
OCAMLDEP  kernel/inductive.ml
OCAMLDEP  kernel/cemitcodes.ml
OCAMLDEP  kernel/vm.ml
OCAMLDEP  kernel/typeops.ml
OCAMLDEP  kernel/term_typing.ml
OCAMLDEP  kernel/environ.ml
OCAMLDEP  kernel/reduction.ml
OCAMLDEP  kernel/mod_typing.ml
OCAMLDEP  kernel/subtyping.ml
OCAMLDEP  kernel/modops.ml
OCAMLDEP  kernel/indtypes.ml
OCAMLDEP  kernel/esubst.ml
OCAMLDEP  kernel/conv_oracle.ml
OCAMLDEP  kernel/closure.ml
OCAMLDEP  kernel/safe_typing.ml
OCAMLDEP  kernel/type_errors.ml
OCAMLDEP  kernel/retroknowledge.ml
OCAMLDEP  kernel/mod_subst.ml
OCAMLDEP  kernel/cooking.ml
OCAMLDEP  kernel/declarations.ml
OCAMLDEP  kernel/univ.ml
OCAMLDEP  kernel/cbytecodes.ml
OCAMLDEP  kernel/term.ml
OCAMLDEP  kernel/pre_env.ml
OCAMLDEP  kernel/csymtable.ml
OCAMLDEP  kernel/vconv.ml
OCAMLDEP  kernel/cbytegen.ml
OCAMLDEP  parsing/prettyp.ml
OCAMLDEP  parsing/ppconstr.ml
OCAMLDEP  parsing/pptactic.ml
OCAMLDEP  parsing/extrawit.ml
OCAMLDEP  parsing/ppvernac.ml
OCAMLDEP  parsing/ppdecl_proof.ml
OCAMLDEP  parsing/tactic_printer.ml
OCAMLDEP  parsing/egrammar.ml
OCAMLDEP  parsing/printer.ml
OCAMLDEP  parsing/extend.ml
OCAMLDEP  parsing/printmod.ml
OCAMLDEP  scripts/coqc.ml
OCAMLDEP  scripts/coqmktop.ml
OCAMLDEP4 parsing/q_constr.ml4
OCAMLDEP4 parsing/q_coqast.ml4
OCAMLDEP4 parsing/lexer.ml4
OCAMLDEP4 parsing/g_constr.ml4
OCAMLDEP4 parsing/g_ltac.ml4
OCAMLDEP4 parsing/g_tactic.ml4
OCAMLDEP4 parsing/g_prim.ml4
OCAMLDEP4 parsing/vernacextend.ml4
OCAMLDEP4 parsing/tacextend.ml4
OCAMLDEP4 parsing/argextend.ml4
OCAMLDEP4 parsing/pcoq.ml4
OCAMLDEP4 parsing/q_util.ml4
OCAMLDEP4 lib/pp.ml4
OCAMLDEP4 lib/compat.ml4
OCAMLDEP  dev/ocamlweb-doc/syntax.mli
OCAMLDEP  ide/config_parser.mli
OCAMLDEP  interp/dumpglob.mli
OCAMLDEP  interp/constrintern.mli
OCAMLDEP  interp/implicit_quantifiers.mli
OCAMLDEP  interp/ppextend.mli
OCAMLDEP  interp/notation.mli
OCAMLDEP  interp/genarg.mli
OCAMLDEP  interp/coqlib.mli
OCAMLDEP  interp/modintern.mli
OCAMLDEP  interp/smartlocate.mli
OCAMLDEP  interp/constrextern.mli
OCAMLDEP  interp/syntax_def.mli
OCAMLDEP  interp/topconstr.mli
OCAMLDEP  interp/reserve.mli
OCAMLDEP  tactics/hipattern.mli
OCAMLDEP  tactics/dn.mli
OCAMLDEP  tactics/tacticals.mli
OCAMLDEP  tactics/auto.mli
OCAMLDEP  tactics/decl_interp.mli
OCAMLDEP  tactics/elim.mli
OCAMLDEP  tactics/dhyp.mli
OCAMLDEP  tactics/contradiction.mli
OCAMLDEP  tactics/termdn.mli
OCAMLDEP  tactics/tacinterp.mli
OCAMLDEP  tactics/evar_tactics.mli
OCAMLDEP  tactics/nbtermdn.mli
OCAMLDEP  tactics/eauto.mli
OCAMLDEP  tactics/autorewrite.mli
OCAMLDEP  tactics/equality.mli
OCAMLDEP  tactics/inv.mli
OCAMLDEP  tactics/tactic_option.mli
OCAMLDEP  tactics/decl_proof_instr.mli
OCAMLDEP  tactics/eqschemes.mli
OCAMLDEP  tactics/extraargs.mli
OCAMLDEP  tactics/refine.mli
OCAMLDEP  tactics/tactics.mli
OCAMLDEP  tactics/btermdn.mli
OCAMLDEP  tactics/hiddentac.mli
OCAMLDEP  tactics/extratactics.mli
OCAMLDEP  tactics/elimschemes.mli
OCAMLDEP  tactics/leminv.mli
OCAMLDEP  pretyping/cases.mli
OCAMLDEP  pretyping/coercion.mli
OCAMLDEP  pretyping/cbv.mli
OCAMLDEP  pretyping/namegen.mli
OCAMLDEP  pretyping/retyping.mli
OCAMLDEP  pretyping/evd.mli
OCAMLDEP  pretyping/term_dnet.mli
OCAMLDEP  pretyping/pattern.mli
OCAMLDEP  pretyping/rawterm.mli
OCAMLDEP  pretyping/evarutil.mli
OCAMLDEP  pretyping/evarconv.mli
OCAMLDEP  pretyping/clenv.mli
OCAMLDEP  pretyping/typeclasses_errors.mli
OCAMLDEP  pretyping/vnorm.mli
OCAMLDEP  pretyping/classops.mli
OCAMLDEP  pretyping/reductionops.mli
OCAMLDEP  pretyping/recordops.mli
OCAMLDEP  pretyping/unification.mli
OCAMLDEP  pretyping/inductiveops.mli
OCAMLDEP  pretyping/tacred.mli
OCAMLDEP  pretyping/typing.mli
OCAMLDEP  pretyping/typeclasses.mli
OCAMLDEP  pretyping/pretyping.mli
OCAMLDEP  pretyping/pretype_errors.mli
OCAMLDEP  pretyping/detyping.mli
OCAMLDEP  pretyping/indrec.mli
OCAMLDEP  pretyping/matching.mli
OCAMLDEP  pretyping/termops.mli
OCAMLDEP  library/impargs.mli
OCAMLDEP  library/dischargedhypsmap.mli
OCAMLDEP  library/libobject.mli
OCAMLDEP  library/states.mli
OCAMLDEP  library/declare.mli
OCAMLDEP  library/nameops.mli
OCAMLDEP  library/library.mli
OCAMLDEP  library/declaremods.mli
OCAMLDEP  library/decl_kinds.mli
OCAMLDEP  library/decls.mli
OCAMLDEP  library/nametab.mli
OCAMLDEP  library/goptions.mli
OCAMLDEP  library/heads.mli
OCAMLDEP  library/summary.mli
OCAMLDEP  library/libnames.mli
OCAMLDEP  library/global.mli
OCAMLDEP  library/lib.mli
OCAMLDEP  plugins/funind/indfun_common.mli
OCAMLDEP  plugins/funind/functional_principles_types.mli
OCAMLDEP  plugins/funind/functional_principles_proofs.mli
OCAMLDEP  plugins/funind/rawtermops.mli
OCAMLDEP  plugins/funind/rawterm_to_relation.mli
OCAMLDEP  plugins/micromega/micromega.mli
OCAMLDEP  plugins/micromega/sos.mli
OCAMLDEP  plugins/xml/unshare.mli
OCAMLDEP  plugins/xml/xml.mli
OCAMLDEP  plugins/xml/doubleTypeInference.mli
OCAMLDEP  plugins/xml/xmlcommand.mli
OCAMLDEP  plugins/cc/cctac.mli
OCAMLDEP  plugins/cc/ccalgo.mli
OCAMLDEP  plugins/cc/ccproof.mli
OCAMLDEP  plugins/romega/const_omega.mli
OCAMLDEP  plugins/subtac/subtac_obligations.mli
OCAMLDEP  plugins/subtac/eterm.mli
OCAMLDEP  plugins/subtac/subtac.mli
OCAMLDEP  plugins/subtac/subtac_classes.mli
OCAMLDEP  plugins/subtac/subtac_coercion.mli
OCAMLDEP  plugins/subtac/subtac_cases.mli
OCAMLDEP  plugins/subtac/subtac_command.mli
OCAMLDEP  plugins/subtac/subtac_pretyping.mli
OCAMLDEP  plugins/subtac/subtac_errors.mli
OCAMLDEP  plugins/subtac/subtac_utils.mli
OCAMLDEP  plugins/firstorder/rules.mli
OCAMLDEP  plugins/firstorder/sequent.mli
OCAMLDEP  plugins/firstorder/instances.mli
OCAMLDEP  plugins/firstorder/ground.mli
OCAMLDEP  plugins/firstorder/formula.mli
OCAMLDEP  plugins/firstorder/unify.mli
OCAMLDEP  plugins/dp/fol.mli
OCAMLDEP  plugins/dp/dp_zenon.mli
OCAMLDEP  plugins/dp/dp_why.mli
OCAMLDEP  plugins/dp/dp.mli
OCAMLDEP  plugins/extraction/scheme.mli
OCAMLDEP  plugins/extraction/table.mli
OCAMLDEP  plugins/extraction/extract_env.mli
OCAMLDEP  plugins/extraction/miniml.mli
OCAMLDEP  plugins/extraction/extraction.mli
OCAMLDEP  plugins/extraction/haskell.mli
OCAMLDEP  plugins/extraction/ocaml.mli
OCAMLDEP  plugins/extraction/common.mli
OCAMLDEP  plugins/extraction/mlutil.mli
OCAMLDEP  plugins/extraction/modutil.mli
OCAMLDEP  plugins/nsatz/utile.mli
OCAMLDEP  plugins/nsatz/polynom.mli
OCAMLDEP  plugins/rtauto/proof_search.mli
OCAMLDEP  plugins/rtauto/refl_tauto.mli
OCAMLDEP  lib/dnet.mli
OCAMLDEP  lib/flags.mli
OCAMLDEP  lib/fmap.mli
OCAMLDEP  lib/fset.mli
OCAMLDEP  lib/tries.mli
OCAMLDEP  lib/envars.mli
OCAMLDEP  lib/dyn.mli
OCAMLDEP  lib/gmapl.mli
OCAMLDEP  lib/pp_control.mli
OCAMLDEP  lib/heap.mli
OCAMLDEP  lib/option.mli
OCAMLDEP  lib/rtree.mli
OCAMLDEP  lib/pp.mli
OCAMLDEP  lib/tlm.mli
OCAMLDEP  lib/explore.mli
OCAMLDEP  lib/gmap.mli
OCAMLDEP  lib/profile.mli
OCAMLDEP  lib/bstack.mli
OCAMLDEP  lib/util.mli
OCAMLDEP  lib/edit.mli
OCAMLDEP  lib/gset.mli
OCAMLDEP  lib/system.mli
OCAMLDEP  lib/predicate.mli
OCAMLDEP  lib/hashcons.mli
OCAMLDEP  lib/segmenttree.mli
OCAMLDEP  lib/bigint.mli
OCAMLDEP  config/coq_config.mli
OCAMLDEP  tools/coqdoc/cpretty.mli
OCAMLDEP  tools/coqdoc/output.mli
OCAMLDEP  tools/coqdoc/alpha.mli
OCAMLDEP  tools/coqdoc/tokens.mli
OCAMLDEP  tools/coqdoc/index.mli
OCAMLDEP  proofs/logic.mli
OCAMLDEP  proofs/decl_mode.mli
OCAMLDEP  proofs/proof_type.mli
OCAMLDEP  proofs/tacmach.mli
OCAMLDEP  proofs/refiner.mli
OCAMLDEP  proofs/proof_trees.mli
OCAMLDEP  proofs/redexpr.mli
OCAMLDEP  proofs/evar_refiner.mli
OCAMLDEP  proofs/pfedit.mli
OCAMLDEP  proofs/decl_expr.mli
OCAMLDEP  proofs/tactic_debug.mli
OCAMLDEP  proofs/clenvtac.mli
OCAMLDEP  ide/undo_lablgtk_ge212.mli
OCAMLDEP  ide/command_windows.mli
OCAMLDEP  ide/utils/config_file.mli
OCAMLDEP  ide/utils/configwin.mli
OCAMLDEP  ide/utils/okey.mli
OCAMLDEP  ide/preferences.mli
OCAMLDEP  ide/coqide.mli
OCAMLDEP  ide/coq.mli
OCAMLDEP  ide/undo_lablgtk_ge26.mli
OCAMLDEP  ide/coq_tactics.mli
OCAMLDEP  ide/undo_lablgtk_lt26.mli
OCAMLDEP  ide/ideutils.mli
OCAMLDEP  toplevel/usage.mli
OCAMLDEP  toplevel/indschemes.mli
OCAMLDEP  toplevel/coqtop.mli
OCAMLDEP  toplevel/search.mli
OCAMLDEP  toplevel/mltop.mli
OCAMLDEP  toplevel/vernacinterp.mli
OCAMLDEP  toplevel/himsg.mli
OCAMLDEP  toplevel/ind_tables.mli
OCAMLDEP  toplevel/classes.mli
OCAMLDEP  toplevel/toplevel.mli
OCAMLDEP  toplevel/auto_ind_decl.mli
OCAMLDEP  toplevel/vernacentries.mli
OCAMLDEP  toplevel/command.mli
OCAMLDEP  toplevel/metasyntax.mli
OCAMLDEP  toplevel/coqinit.mli
OCAMLDEP  toplevel/libtypes.mli
OCAMLDEP  toplevel/class.mli
OCAMLDEP  toplevel/lemmas.mli
OCAMLDEP  toplevel/discharge.mli
OCAMLDEP  toplevel/whelp.mli
OCAMLDEP  toplevel/vernac.mli
OCAMLDEP  toplevel/cerrors.mli
OCAMLDEP  toplevel/record.mli
OCAMLDEP  toplevel/autoinstance.mli
rm tactics/tauto.ml tactics/class_tactics.ml plugins/micromega/g_micromega.ml parsing/g_prim.ml plugins/field/field.ml parsing/q_coqast.ml parsing/vernacextend.ml tools/coq_makefile.ml toplevel/whelp.ml plugins/firstorder/g_ground.ml lib/compat.ml tactics/eauto.ml parsing/q_constr.ml parsing/g_decl_mode.ml plugins/extraction/g_extraction.ml tactics/rewrite.ml plugins/romega/g_romega.ml parsing/g_ltac.ml plugins/xml/xmlentries.ml tactics/hipattern.ml parsing/g_tactic.ml plugins/fourier/g_fourier.ml parsing/lexer.ml parsing/g_vernac.ml plugins/funind/g_indfun.ml toplevel/mltop.ml plugins/dp/g_dp.ml plugins/xml/xml.ml parsing/tacextend.ml plugins/xml/acic2Xml.ml plugins/ring/g_ring.ml plugins/quote/g_quote.ml parsing/g_constr.ml plugins/rtauto/g_rtauto.ml lib/pp.ml plugins/omega/g_omega.ml plugins/xml/dumptree.ml tactics/extraargs.ml tactics/extratactics.ml plugins/xml/proofTree2Xml.ml parsing/argextend.ml parsing/pcoq.ml lib/refutpat.ml parsing/g_proofs.ml plugins/setoid_ring/newring.ml plugins/cc/g_congruence.ml parsing/g_xml.ml plugins/nsatz/nsatz.ml plugins/subtac/g_subtac.ml parsing/q_util.ml tactics/eqdecide.ml tools/coq_tex.ml
make[1]: Leaving directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
make[1]: Entering directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
OCAMLOPT -o bin/coqdep_boot
OCAMLC    lib/pp_control.mli
OCAMLC4   lib/compat.ml4
OCAMLC    lib/predicate.mli
OCAMLC    library/summary.mli
OCAMLC    lib/dyn.mli
OCAMLC    lib/option.mli
OCAMLC    lib/flags.mli
OCAMLC    lib/pp.mli
OCAMLC    lib/util.mli
OCAMLC    kernel/names.mli
OCAMLC    lib/rtree.mli
OCAMLC    lib/bigint.mli
OCAMLC    kernel/univ.mli
OCAMLC    interp/ppextend.mli
OCAMLC    kernel/conv_oracle.mli
OCAMLC    kernel/esubst.mli
OCAMLC    parsing/extend.mli
OCAMLC    kernel/term.mli
OCAMLC    kernel/sign.mli
OCAMLC    kernel/mod_subst.mli
OCAMLC    kernel/cbytecodes.mli
OCAMLC    library/libnames.mli
OCAMLC    kernel/retroknowledge.mli
OCAMLC    kernel/cemitcodes.mli
OCAMLC    kernel/declarations.mli
OCAMLC    library/nametab.mli
OCAMLC    library/libobject.mli
OCAMLC    library/decl_kinds.mli
OCAMLC    kernel/pre_env.mli
OCAMLC    library/lib.mli
OCAMLC    library/goptions.mli
OCAMLC    kernel/environ.mli
OCAMLC    kernel/closure.mli
OCAMLC    kernel/reduction.mli
OCAMLC    pretyping/termops.mli
OCAMLC    pretyping/evd.mli
OCAMLC    pretyping/rawterm.mli
OCAMLC    pretyping/classops.mli
OCAMLC    interp/topconstr.mli
OCAMLC    pretyping/pattern.mli
OCAMLC    interp/notation.mli
OCAMLC    interp/genarg.mli
OCAMLC    proofs/tacexpr.ml
OCAMLC    proofs/decl_expr.mli
OCAMLC    toplevel/vernacexpr.ml
OCAMLC    parsing/pcoq.mli
OCAMLC    parsing/q_util.mli
OCAMLC4   parsing/q_constr.ml4
strip bin/coqdep_boot
COQDEP  parsing/grammar.mllib
Testing parsing/grammar.cma
OCAMLC -a parsing/grammar.cma
make[1]: Leaving directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
*****************************************************
*****************************************************
****************** Entering stage2 ******************
*****************************************************
*****************************************************
/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage2 "world"
make[1]: Entering directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
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/dp/Dp.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/Psatz.v
COQDEP    plugins/micromega/QMicromega.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/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/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/NZDiv.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/ZDivEucl.v
COQDEP    theories/Numbers/Integer/Abstract/ZDivTrunc.v
COQDEP    theories/Numbers/Integer/Abstract/ZDivFloor.v
COQDEP    theories/Numbers/Integer/Abstract/ZProperties.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/ZAxioms.v
COQDEP    theories/Numbers/Integer/Abstract/ZAdd.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/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/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/Ranalysis.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/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/MSetList.v
COQDEP    theories/MSets/MSetInterface.v
COQDEP    theories/MSets/MSetFacts.v
COQDEP    theories/MSets/MSetEqProperties.v
COQDEP    theories/MSets/MSetDecide.v
COQDEP    theories/MSets/MSetAVL.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/TheoryList.v
COQDEP    theories/Lists/Streams.v
COQDEP    theories/Lists/StreamMemo.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/ZOrderedType.v
COQDEP    theories/ZArith/Zwf.v
COQDEP    theories/ZArith/Zsqrt.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/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/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/Zdigits.v
COQDEP    theories/ZArith/Zbool.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/auxiliary.v
COQDEP    theories/NArith/Nminmax.v
COQDEP    theories/NArith/NOrderedType.v
COQDEP    theories/NArith/Pminmax.v
COQDEP    theories/NArith/POrderedType.v
COQDEP    theories/NArith/Pnat.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/BinPos.v
COQDEP    theories/NArith/BinNat.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/MinMax.v
COQDEP    theories/Arith/NatOrderedType.v
COQDEP    theories/Arith/Wf_nat.v
COQDEP    theories/Arith/Peano_dec.v
COQDEP    theories/Arith/Plus.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
OCAMLC    config/coq_config.mli
OCAMLC    lib/profile.mli
OCAMLC    lib/pp_control.ml
OCAMLC4   lib/pp.ml4
OCAMLC    lib/segmenttree.mli
OCAMLC    lib/unicodetable.ml
OCAMLC    lib/bigint.ml
OCAMLC    lib/dyn.ml
OCAMLC    lib/hashcons.mli
OCAMLC    lib/predicate.ml
OCAMLC    lib/rtree.ml
OCAMLC    lib/option.ml
OCAMLC    kernel/names.ml
OCAMLC    kernel/univ.ml
OCAMLC    kernel/esubst.ml
OCAMLC    kernel/term.ml
OCAMLC    kernel/mod_subst.ml
OCAMLC    kernel/sign.ml
OCAMLC    kernel/cbytecodes.ml
OCAMLC    kernel/copcodes.ml
OCAMLC    kernel/declarations.ml
OCAMLC    kernel/retroknowledge.ml
OCAMLC    kernel/pre_env.ml
OCAMLC    kernel/cbytegen.mli
OCAMLC    kernel/conv_oracle.ml
OCAMLC    kernel/closure.ml
OCAMLC    kernel/reduction.ml
OCAMLC    kernel/type_errors.mli
OCAMLC    kernel/entries.mli
OCAMLC    kernel/inductive.mli
OCAMLC    kernel/subtyping.mli
OCAMLC    kernel/cooking.mli
OCAMLC    kernel/mod_typing.mli
OCAMLC    library/nameops.mli
OCAMLC    library/summary.ml
OCAMLC    library/libobject.ml
OCAMLC    library/lib.ml
OCAMLC    library/goptions.ml
OCAMLC    library/decl_kinds.ml
OCAMLC    pretyping/namegen.mli
OCAMLC    pretyping/reductionops.mli
OCAMLC    pretyping/inductiveops.mli
OCAMLC    pretyping/rawterm.ml
OCAMLC    pretyping/detyping.mli
OCAMLC    interp/genarg.ml
OCAMLC    interp/ppextend.ml
OCAMLC    parsing/lexer.mli
OCAMLC    parsing/extend.ml
OCAMLC    parsing/extrawit.mli
OCAMLC4   parsing/q_coqast.ml4
OCAMLC    parsing/egrammar.mli
OCAMLC4   parsing/g_prim.ml4
OCAMLC4   parsing/g_tactic.ml4
OCAMLC4   parsing/g_ltac.ml4
OCAMLC4   parsing/g_constr.ml4
TOUCH     parsing/g_ltac.ml
TOUCH     parsing/g_xml.ml
TOUCH     parsing/vernacextend.ml
TOUCH     parsing/g_prim.ml
TOUCH     parsing/g_constr.ml
TOUCH     parsing/g_decl_mode.ml
TOUCH     parsing/g_vernac.ml
TOUCH     parsing/argextend.ml
TOUCH     parsing/g_tactic.ml
TOUCH     parsing/lexer.ml
TOUCH     parsing/tacextend.ml
TOUCH     parsing/q_coqast.ml
TOUCH     parsing/q_constr.ml
TOUCH     parsing/pcoq.ml
TOUCH     parsing/g_proofs.ml
TOUCH     parsing/q_util.ml
TOUCH     toplevel/whelp.ml
TOUCH     toplevel/mltop.ml
TOUCH     tools/coq_tex.ml
TOUCH     tools/coq_makefile.ml
TOUCH     lib/compat.ml
TOUCH     lib/pp.ml
TOUCH     lib/refutpat.ml
TOUCH     plugins/rtauto/g_rtauto.ml
TOUCH     plugins/nsatz/nsatz.ml
TOUCH     plugins/field/field.ml
TOUCH     plugins/setoid_ring/newring.ml
TOUCH     plugins/extraction/g_extraction.ml
TOUCH     plugins/dp/g_dp.ml
TOUCH     plugins/quote/g_quote.ml
TOUCH     plugins/firstorder/g_ground.ml
TOUCH     plugins/subtac/g_subtac.ml
TOUCH     plugins/romega/g_romega.ml
TOUCH     plugins/ring/g_ring.ml
TOUCH     plugins/cc/g_congruence.ml
TOUCH     plugins/fourier/g_fourier.ml
TOUCH     plugins/xml/proofTree2Xml.ml
TOUCH     plugins/xml/dumptree.ml
TOUCH     plugins/xml/xmlentries.ml
TOUCH     plugins/xml/xml.ml
TOUCH     plugins/xml/acic2Xml.ml
TOUCH     plugins/micromega/g_micromega.ml
TOUCH     plugins/omega/g_omega.ml
TOUCH     plugins/funind/g_indfun.ml
TOUCH     tactics/hipattern.ml
TOUCH     tactics/rewrite.ml
TOUCH     tactics/class_tactics.ml
TOUCH     tactics/eauto.ml
TOUCH     tactics/tauto.ml
TOUCH     tactics/eqdecide.ml
TOUCH     tactics/extratactics.ml
TOUCH     tactics/extraargs.ml
ECHO... > plugins/funind/recdef_plugin_mod.ml
ECHO... > plugins/omega/omega_plugin_mod.ml
ECHO... > plugins/micromega/micromega_plugin_mod.ml
ECHO... > plugins/xml/xml_plugin_mod.ml
ECHO... > plugins/fourier/fourier_plugin_mod.ml
ECHO... > plugins/cc/cc_plugin_mod.ml
ECHO... > plugins/ring/ring_plugin_mod.ml
ECHO... > plugins/syntax/r_syntax_plugin_mod.ml
ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml
ECHO... > plugins/syntax/z_syntax_plugin_mod.ml
ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml
ECHO... > plugins/syntax/string_syntax_plugin_mod.ml
ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml
ECHO... > plugins/romega/romega_plugin_mod.ml
ECHO... > plugins/subtac/subtac_plugin_mod.ml
ECHO... > plugins/firstorder/ground_plugin_mod.ml
ECHO... > plugins/quote/quote_plugin_mod.ml
ECHO... > plugins/dp/dp_plugin_mod.ml
ECHO... > plugins/setoid_ring/newring_plugin_mod.ml
ECHO... > plugins/extraction/extraction_plugin_mod.ml
ECHO... > plugins/field/field_plugin_mod.ml
ECHO... > plugins/nsatz/nsatz_plugin_mod.ml
ECHO... > plugins/rtauto/rtauto_plugin_mod.ml
COQDEP  interp/interp.mllib
COQDEP  tactics/hightactics.mllib
COQDEP  tactics/tactics.mllib
COQDEP  pretyping/pretyping.mllib
COQDEP  dev/printers.mllib
COQDEP  library/library.mllib
COQDEP  plugins/funind/recdef_plugin.mllib
COQDEP  plugins/omega/omega_plugin.mllib
COQDEP  plugins/micromega/micromega_plugin.mllib
COQDEP  plugins/xml/xml_plugin.mllib
COQDEP  plugins/fourier/fourier_plugin.mllib
COQDEP  plugins/cc/cc_plugin.mllib
COQDEP  plugins/ring/ring_plugin.mllib
COQDEP  plugins/syntax/r_syntax_plugin.mllib
COQDEP  plugins/syntax/ascii_syntax_plugin.mllib
COQDEP  plugins/syntax/z_syntax_plugin.mllib
COQDEP  plugins/syntax/nat_syntax_plugin.mllib
COQDEP  plugins/syntax/string_syntax_plugin.mllib
COQDEP  plugins/syntax/numbers_syntax_plugin.mllib
COQDEP  plugins/romega/romega_plugin.mllib
COQDEP  plugins/subtac/subtac_plugin.mllib
COQDEP  plugins/firstorder/ground_plugin.mllib
COQDEP  plugins/quote/quote_plugin.mllib
COQDEP  plugins/dp/dp_plugin.mllib
COQDEP  plugins/extraction/extraction_plugin.mllib
COQDEP  plugins/setoid_ring/newring_plugin.mllib
COQDEP  plugins/field/field_plugin.mllib
COQDEP  plugins/nsatz/nsatz_plugin.mllib
COQDEP  plugins/rtauto/rtauto_plugin.mllib
COQDEP  lib/lib.mllib
COQDEP  proofs/proofs.mllib
COQDEP  ide/ide.mllib
COQDEP  toplevel/toplevel.mllib
COQDEP  checker/check.mllib
COQDEP  kernel/kernel.mllib
COQDEP  parsing/highparsing.mllib
COQDEP  parsing/parsing.mllib
OCAMLC    config/coq_config.ml
OCAMLC    lib/profile.ml
OCAMLC    lib/flags.ml
OCAMLC    lib/segmenttree.ml
OCAMLC    lib/util.ml
OCAMLC    lib/hashcons.ml
OCAMLC    kernel/cemitcodes.ml
OCAMLC    kernel/cbytegen.ml
OCAMLC    kernel/environ.ml
OCAMLC    kernel/type_errors.ml
OCAMLC    kernel/entries.ml
OCAMLC    kernel/modops.mli
OCAMLC    kernel/inductive.ml
OCAMLC    kernel/typeops.mli
OCAMLC    kernel/safe_typing.mli
OCAMLC    library/nameops.ml
OCAMLC    library/libnames.ml
OCAMLC    library/nametab.ml
OCAMLC    pretyping/namegen.ml
OCAMLC    pretyping/reductionops.ml
OCAMLC    pretyping/pattern.ml
OCAMLC4   parsing/lexer.ml4
OCAMLC    parsing/extrawit.ml
OCAMLC4   parsing/pcoq.ml4
OCAMLC4   parsing/q_util.ml4
OCAMLC    parsing/egrammar.ml
OCAMLC4   parsing/argextend.ml4
OCAMLDEP4 plugins/xml/acic2Xml.ml4
OCAMLDEP4 plugins/xml/xml.ml4
OCAMLDEP4 plugins/xml/proofTree2Xml.ml4
OCAMLDEP4 lib/refutpat.ml4
OCAMLDEP4 tools/coq_makefile.ml4
OCAMLDEP4 tools/coq_tex.ml4
OCAMLDEP4 toplevel/mltop.ml4
OCAMLDEP4 parsing/g_proofs.ml4
OCAMLDEP4 parsing/g_xml.ml4
OCAMLDEP  plugins/funind/recdef_plugin_mod.ml
OCAMLDEP  plugins/omega/omega_plugin_mod.ml
OCAMLDEP  plugins/micromega/micromega_plugin_mod.ml
OCAMLDEP  plugins/xml/xml_plugin_mod.ml
OCAMLDEP  plugins/fourier/fourier_plugin_mod.ml
OCAMLDEP  plugins/cc/cc_plugin_mod.ml
OCAMLDEP  plugins/ring/ring_plugin_mod.ml
OCAMLDEP  plugins/syntax/r_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/ascii_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/z_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/string_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/numbers_syntax_plugin_mod.ml
OCAMLDEP  plugins/romega/romega_plugin_mod.ml
OCAMLDEP  plugins/subtac/subtac_plugin_mod.ml
OCAMLDEP  plugins/firstorder/ground_plugin_mod.ml
OCAMLDEP  plugins/quote/quote_plugin_mod.ml
OCAMLDEP  plugins/dp/dp_plugin_mod.ml
OCAMLDEP  plugins/extraction/extraction_plugin_mod.ml
OCAMLDEP  plugins/setoid_ring/newring_plugin_mod.ml
OCAMLDEP  plugins/field/field_plugin_mod.ml
OCAMLDEP  plugins/nsatz/nsatz_plugin_mod.ml
OCAMLDEP  plugins/rtauto/rtauto_plugin_mod.ml
OCAMLC    kernel/modops.ml
OCAMLC    kernel/typeops.ml
OCAMLC    kernel/indtypes.mli
OCAMLC    kernel/cooking.ml
OCAMLC    kernel/term_typing.mli
OCAMLC    kernel/subtyping.ml
OCAMLC    library/global.mli
OCAMLC4   parsing/tacextend.ml4
OCAMLC    kernel/indtypes.ml
OCAMLC    kernel/term_typing.ml
OCAMLC    kernel/mod_typing.ml
OCAMLC    kernel/safe_typing.ml
OCAMLC    library/global.ml
OCAMLC    pretyping/termops.ml
OCAMLC    pretyping/evd.ml
OCAMLC    pretyping/inductiveops.ml
OCAMLC    pretyping/detyping.ml
OCAMLC    interp/topconstr.ml
OCAMLC4   parsing/vernacextend.ml4
Testing parsing/grammar.cma
OCAMLC -a parsing/grammar.cma
OCAMLDEP4 tactics/extraargs.ml4
OCAMLDEP4 tactics/extratactics.ml4
OCAMLDEP4 tactics/eqdecide.ml4
OCAMLDEP4 tactics/tauto.ml4
OCAMLDEP4 tactics/eauto.ml4
OCAMLDEP4 tactics/class_tactics.ml4
OCAMLDEP4 tactics/rewrite.ml4
OCAMLDEP4 tactics/hipattern.ml4
OCAMLDEP4 plugins/funind/g_indfun.ml4
OCAMLDEP4 plugins/omega/g_omega.ml4
OCAMLDEP4 plugins/micromega/g_micromega.ml4
OCAMLDEP4 plugins/xml/xmlentries.ml4
OCAMLDEP4 plugins/xml/dumptree.ml4
OCAMLDEP4 plugins/fourier/g_fourier.ml4
OCAMLDEP4 plugins/cc/g_congruence.ml4
OCAMLDEP4 plugins/ring/g_ring.ml4
OCAMLDEP4 plugins/romega/g_romega.ml4
OCAMLDEP4 plugins/subtac/g_subtac.ml4
OCAMLDEP4 plugins/firstorder/g_ground.ml4
OCAMLDEP4 plugins/quote/g_quote.ml4
OCAMLDEP4 plugins/dp/g_dp.ml4
OCAMLDEP4 plugins/extraction/g_extraction.ml4
OCAMLDEP4 plugins/setoid_ring/newring.ml4
OCAMLDEP4 plugins/field/field.ml4
OCAMLDEP4 plugins/nsatz/nsatz.ml4
OCAMLDEP4 plugins/rtauto/g_rtauto.ml4
OCAMLDEP4 toplevel/whelp.ml4
OCAMLDEP4 parsing/g_vernac.ml4
OCAMLDEP4 parsing/g_decl_mode.ml4
rm tactics/tauto.ml tactics/class_tactics.ml plugins/micromega/g_micromega.ml plugins/subtac/g_subtac.ml tools/coq_tex.ml plugins/field/field.ml parsing/vernacextend.ml toplevel/whelp.ml parsing/q_coqast.ml plugins/omega/g_omega.ml plugins/romega/g_romega.ml parsing/g_ltac.ml plugins/xml/xmlentries.ml parsing/g_tactic.ml parsing/lexer.ml tactics/hipattern.ml plugins/funind/g_indfun.ml parsing/tacextend.ml plugins/quote/g_quote.ml plugins/fourier/g_fourier.ml lib/pp.ml tactics/eauto.ml plugins/dp/g_dp.ml parsing/g_proofs.ml plugins/xml/proofTree2Xml.ml parsing/g_decl_mode.ml toplevel/mltop.ml lib/refutpat.ml parsing/q_constr.ml plugins/cc/g_congruence.ml parsing/g_prim.ml lib/compat.ml plugins/extraction/g_extraction.ml parsing/g_vernac.ml parsing/pcoq.ml plugins/xml/xml.ml plugins/firstorder/g_ground.ml plugins/ring/g_ring.ml parsing/g_xml.ml tactics/rewrite.ml parsing/g_constr.ml plugins/rtauto/g_rtauto.ml plugins/xml/acic2Xml.ml plugins/xml/dumptree.ml tactics/extraargs.ml tactics/extratactics.ml parsing/argextend.ml plugins/setoid_ring/newring.ml plugins/nsatz/nsatz.ml parsing/q_util.ml tools/coq_makefile.ml tactics/eqdecide.ml
make[1]: Leaving directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
make[1]: Entering directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
CHECK revision
OCAMLOPT  config/coq_config.ml
OCAMLOPT  lib/pp_control.ml
OCAMLOPT4 lib/compat.ml4
OCAMLOPT  lib/segmenttree.ml
OCAMLOPT  lib/unicodetable.ml
OCAMLC    lib/system.mli
OCAMLC    lib/envars.mli
OCAMLOPT  scripts/tolink.ml
OCAMLOPT  lib/hashcons.ml
OCAMLC    lib/bstack.mli
OCAMLC    lib/edit.mli
OCAMLC    lib/gset.mli
OCAMLC    lib/gmap.mli
OCAMLC    lib/fset.mli
OCAMLC    lib/fmap.mli
OCAMLC    lib/tlm.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
OCAMLOPT  kernel/copcodes.ml
OCAMLC    kernel/vm.mli
OCAMLC    kernel/csymtable.mli
OCAMLC    kernel/vconv.mli
OCAMLC    library/declaremods.mli
OCAMLC    library/library.mli
OCAMLC    library/states.mli
OCAMLC    library/dischargedhypsmap.mli
OCAMLC    library/decls.mli
OCAMLC    library/heads.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/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    interp/dumpglob.mli
OCAMLC    interp/syntax_def.mli
OCAMLC    interp/smartlocate.mli
OCAMLC    interp/reserve.mli
OCAMLC    library/impargs.mli
OCAMLC    interp/implicit_quantifiers.mli
OCAMLC    interp/modintern.mli
OCAMLC    interp/constrextern.mli
OCAMLC    interp/coqlib.mli
OCAMLC    toplevel/discharge.mli
OCAMLC    library/declare.mli
OCAMLC    proofs/proof_type.mli
OCAMLC    proofs/redexpr.mli
OCAMLC    parsing/ppconstr.mli
OCAMLC    parsing/ppdecl_proof.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    tactics/tactic_option.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/classes.mli
OCAMLC    toplevel/record.mli
CAMLP4O   toplevel/mltop.ml4
OCAMLC    toplevel/mltop.mli
OCAMLC    toplevel/vernacentries.mli
OCAMLC    toplevel/whelp.mli
OCAMLC    toplevel/vernac.mli
OCAMLC    toplevel/toplevel.mli
OCAMLC    toplevel/usage.mli
OCAMLC    toplevel/coqinit.mli
OCAMLC    toplevel/coqtop.mli
OCAMLC    tactics/extratactics.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/cc/cc_plugin_mod.ml
OCAMLC    plugins/firstorder/unify.mli
OCAMLC    plugins/firstorder/ground_plugin_mod.ml
OCAMLC    plugins/dp/fol.mli
OCAMLC    plugins/dp/dp.mli
OCAMLC    plugins/dp/dp_plugin_mod.ml
OCAMLC    plugins/funind/indfun_common.mli
OCAMLC    plugins/funind/rawtermops.mli
OCAMLC    plugins/funind/rawterm_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_obligations.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
OCAMLOPT4 plugins/xml/xml.ml4
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_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/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
OCAMLOPT4 tools/coq_makefile.ml4
OCAMLOPT  tools/gallina_lexer.ml
OCAMLOPT4 tools/coq_tex.ml4
OCAMLOPT  tools/coqwc.ml
OCAMLOPT  tools/coqdoc/cdglobals.ml
OCAMLC    tools/coqdoc/alpha.mli
OCAMLC    tools/coqdoc/cdglobals.ml
OCAMLC    dev/vm_printers.ml
OCAMLC    lib/system.ml
OCAMLC    lib/envars.ml
OCAMLC    lib/bstack.ml
OCAMLC    lib/edit.ml
OCAMLC    lib/gset.ml
OCAMLC    lib/gmap.ml
OCAMLC    lib/fset.ml
OCAMLC    lib/fmap.ml
OCAMLC    lib/tlm.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    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/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    interp/notation.ml
OCAMLC    interp/dumpglob.ml
OCAMLC    interp/reserve.ml
OCAMLC    library/impargs.ml
OCAMLC    interp/constrextern.ml
OCAMLC    interp/syntax_def.ml
OCAMLC    interp/implicit_quantifiers.ml
OCAMLC    interp/smartlocate.ml
OCAMLC    proofs/proof_type.ml
OCAMLC    parsing/ppconstr.ml
OCAMLC    lib/tries.ml
OCAMLC    kernel/vm.ml
OCAMLC    kernel/csymtable.ml
OCAMLC    kernel/vconv.ml
OCAMLC    library/declaremods.ml
OCAMLC    library/library.ml
OCAMLC    library/states.ml
OCAMLC    library/dischargedhypsmap.ml
OCAMLC    pretyping/vnorm.ml
OCAMLC    toplevel/discharge.ml
OCAMLC    library/declare.ml
OCAMLC    proofs/redexpr.ml
OCAMLC4   parsing/g_xml.ml4
OCAMLC    parsing/printmod.ml
OCAMLC    tactics/dn.ml
OCAMLC    tactics/termdn.ml
OCAMLC    tactics/btermdn.ml
OCAMLC    toplevel/ind_tables.ml
OCAMLC    toplevel/libtypes.ml
CAMLP4O   toplevel/mltop.ml4
OCAMLC    toplevel/usage.ml
OCAMLC    toplevel/coqinit.ml
OCAMLC    toplevel/coqtop.ml
OCAMLC4   parsing/g_decl_mode.ml4
OCAMLC    checker/validate.ml
OCAMLC    checker/term.mli
OCAMLC    checker/check_stat.mli
OCAMLOPT  checker/validate.ml
OCAMLC    plugins/micromega/sos.mli
OCAMLOPT4 lib/pp.ml4
OCAMLOPT  lib/flags.ml
OCAMLOPT  lib/gset.ml
OCAMLOPT  lib/gmap.ml
OCAMLOPT  lib/fset.ml
OCAMLOPT  lib/fmap.ml
OCAMLOPT  lib/explore.ml
OCAMLOPT  lib/heap.ml
OCAMLOPT  lib/dnet.ml
OCAMLC    pretyping/clenv.mli
OCAMLC    pretyping/cases.mli
OCAMLC    proofs/proof_trees.mli
OCAMLC    proofs/logic.mli
OCAMLC    proofs/tactic_debug.mli
OCAMLC    proofs/clenvtac.mli
OCAMLC    parsing/printer.mli
OCAMLC    parsing/tactic_printer.mli
OCAMLC    tactics/nbtermdn.mli
OCAMLC    tactics/eqschemes.mli
OCAMLC    tactics/elimschemes.mli
OCAMLC    tactics/contradiction.mli
OCAMLC    tactics/leminv.mli
OCAMLC    toplevel/himsg.mli
OCAMLC    toplevel/auto_ind_decl.mli
OCAMLOPT  toplevel/usage.ml
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/dp/dp_why.mli
OCAMLC    plugins/dp/dp_zenon.mli
OCAMLC    plugins/funind/rawtermops.ml
OCAMLC    plugins/subtac/subtac_errors.ml
OCAMLC    plugins/subtac/subtac_cases.mli
OCAMLC    plugins/subtac/subtac_classes.mli
"ranlib" kernel/byterun/libcoqrun.a
OCAMLC    plugins/xml/unshare.ml
OCAMLC4   plugins/xml/xml.ml4
OCAMLC    plugins/xml/doubleTypeInference.mli
OCAMLC -a -o plugins/syntax/z_syntax_plugin.cma
OCAMLC -a -o plugins/syntax/ascii_syntax_plugin.cma
OCAMLC    plugins/syntax/string_syntax.ml
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/micromega/sos_lib.ml
OCAMLOPT  plugins/micromega/micromega.ml
OCAMLOPT  plugins/micromega/sos_lib.ml
OCAMLC    plugins/rtauto/proof_search.ml
OCAMLC    plugins/nsatz/utile.ml
OCAMLC    plugins/nsatz/polynom.ml
OCAMLC    plugins/nsatz/ideal.ml
OCAMLOPT  plugins/nsatz/utile.ml
OCAMLOPT -o bin/coq_makefile
OCAMLOPT  tools/gallina.ml
OCAMLOPT -o bin/coq-tex
OCAMLOPT -o bin/coqwc
OCAMLOPT  tools/coqdoc/alpha.ml
OCAMLC    tools/coqdoc/index.mli
OCAMLC    pretyping/cases.ml
strip bin/coq_makefile
OCAMLC    pretyping/clenv.ml
strip bin/coqwc
OCAMLC    proofs/proof_trees.ml
strip bin/coq-tex
OCAMLC    proofs/logic.ml
OCAMLC -a -o lib/lib.cma
OCAMLC -a -o kernel/kernel.cma
OCAMLC -a -o library/library.cma
OCAMLC    interp/coqlib.ml
OCAMLC    parsing/prettyp.ml
OCAMLC    tactics/nbtermdn.ml
OCAMLC    tactics/eqschemes.ml
OCAMLC    tactics/elimschemes.ml
OCAMLC    toplevel/class.ml
OCAMLC    toplevel/search.ml
OCAMLC    toplevel/autoinstance.ml
OCAMLC    toplevel/mltop.byteml
OCAMLC    checker/term.ml
OCAMLC    checker/declarations.mli
OCAMLOPT  plugins/micromega/sos.ml
OCAMLOPT  lib/util.ml
OCAMLOPT  lib/bigint.ml
OCAMLOPT  lib/tlm.ml
OCAMLOPT  lib/tries.ml
OCAMLC    pretyping/pretyping.mli
OCAMLC    proofs/refiner.mli
OCAMLC    parsing/pptactic.mli
OCAMLOPT  tactics/dn.ml
OCAMLC    plugins/extraction/table.ml
OCAMLC    plugins/extraction/mlutil.mli
OCAMLC    plugins/dp/dp_why.ml
OCAMLC    plugins/subtac/subtac_pretyping.mli
OCAMLC    plugins/xml/doubleTypeInference.ml
OCAMLC    plugins/xml/cic2acic.ml
OCAMLC -a -o plugins/syntax/string_syntax_plugin.cma
OCAMLC    plugins/micromega/mfourier.ml
OCAMLOPT  plugins/micromega/mutils.ml
OCAMLOPT -o bin/gallina
OCAMLOPT  tools/coqdoc/index.ml
OCAMLC    tools/coqdoc/tokens.mli
OCAMLC    tools/coqdoc/output.mli
OCAMLC    tools/coqdoc/cpretty.mli
OCAMLC    pretyping/pretyping.ml
OCAMLC    proofs/refiner.ml
OCAMLC    proofs/tactic_debug.ml
OCAMLC    parsing/pptactic.ml
OCAMLC    parsing/ppdecl_proof.ml
OCAMLC    parsing/tactic_printer.ml
strip bin/gallina
OCAMLC    toplevel/himsg.ml
OCAMLC    toplevel/cerrors.ml
OCAMLC -a -o pretyping/pretyping.cma
OCAMLC    checker/declarations.ml
OCAMLC    checker/environ.mli
OCAMLOPT  plugins/micromega/csdpcert.ml
OCAMLOPT  lib/system.ml
OCAMLOPT  lib/dyn.ml
OCAMLOPT  lib/bstack.ml
OCAMLOPT  lib/gmapl.ml
OCAMLOPT  lib/rtree.ml
OCAMLOPT  kernel/names.ml
OCAMLOPT  kernel/esubst.ml
OCAMLOPT  library/summary.ml
OCAMLOPT4 parsing/lexer.ml4
OCAMLC    interp/constrintern.mli
OCAMLC    proofs/evar_refiner.mli
OCAMLC    proofs/tacmach.mli
OCAMLOPT  parsing/extend.ml
OCAMLC    parsing/ppvernac.mli
OCAMLC    plugins/extraction/mlutil.ml
OCAMLC    plugins/extraction/modutil.ml
OCAMLC    plugins/extraction/extraction.ml
OCAMLC    plugins/extraction/common.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/subtac/subtac_utils.mli
OCAMLC    plugins/subtac/subtac_command.mli
OCAMLC4   plugins/xml/acic2Xml.ml4
OCAMLC    plugins/xml/proof2aproof.ml
OCAMLOPT  plugins/omega/omega.ml
OCAMLC    plugins/romega/const_omega.mli
OCAMLC    plugins/micromega/certificate.ml
OCAMLOPT  plugins/micromega/mfourier.ml
OCAMLC    plugins/rtauto/refl_tauto.mli
OCAMLOPT  plugins/nsatz/polynom.ml
OCAMLOPT  tools/coqdoc/tokens.ml
OCAMLC    interp/constrintern.ml
OCAMLC    proofs/evar_refiner.ml
OCAMLC    interp/modintern.ml
OCAMLC    proofs/tacmach.ml
OCAMLC    proofs/clenvtac.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/safe_typing.mli
OCAMLOPT  lib/envars.ml
OCAMLOPT  lib/edit.ml
OCAMLOPT  kernel/univ.ml
OCAMLOPT  kernel/conv_oracle.ml
OCAMLOPT  library/nameops.ml
OCAMLOPT  interp/ppextend.ml
OCAMLC    proofs/pfedit.mli
OCAMLC    proofs/decl_mode.mli
OCAMLC    tactics/tacticals.mli
OCAMLC    tactics/hipattern.mli
OCAMLC    tactics/dhyp.mli
OCAMLC    tactics/auto.mli
OCAMLC    tactics/inv.mli
OCAMLC    tactics/tacinterp.mli
OCAMLC    tactics/decl_proof_instr.mli
OCAMLC    toplevel/metasyntax.mli
OCAMLC    toplevel/lemmas.mli
OCAMLC    toplevel/command.mli
OCAMLC    tactics/refine.mli
OCAMLC    tactics/extraargs.mli
OCAMLC    tactics/eauto.mli
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
OCAMLC4   plugins/extraction/g_extraction.ml4
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/rawterm_to_relation.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_classes.ml
OCAMLC    plugins/subtac/subtac.ml
OCAMLC4   plugins/subtac/g_subtac.ml4
OCAMLC    plugins/xml/xmlcommand.mli
OCAMLC4   plugins/xml/proofTree2Xml.ml4
OCAMLC    plugins/xml/cic2Xml.ml
OCAMLC4   plugins/xml/dumptree.ml4
OCAMLC    plugins/romega/const_omega.ml
OCAMLOPT  plugins/micromega/certificate.ml
OCAMLC4   plugins/rtauto/g_rtauto.ml4
OCAMLOPT  plugins/nsatz/ideal.ml
OCAMLOPT  tools/coqdep.ml
OCAMLOPT  tools/coqdoc/output.ml
OCAMLC    dev/top_printers.ml
OCAMLC    proofs/pfedit.ml
OCAMLC    proofs/decl_mode.ml
OCAMLC    parsing/printer.ml
OCAMLC    toplevel/vernacinterp.ml
OCAMLOPT  scripts/coqc.ml
OCAMLC -a -o interp/interp.cma
OCAMLC -a -o proofs/proofs.cma
OCAMLC    tactics/tacticals.ml
OCAMLC4   tactics/hipattern.ml4
OCAMLC    tactics/tactic_option.ml
OCAMLC    toplevel/metasyntax.ml
OCAMLC    toplevel/indschemes.ml
OCAMLC    toplevel/command.ml
OCAMLC    toplevel/record.ml
OCAMLC    parsing/ppvernac.ml
OCAMLC4   toplevel/whelp.ml4
OCAMLC    toplevel/vernac.ml
OCAMLC    toplevel/toplevel.ml
OCAMLC4   parsing/g_vernac.ml4
OCAMLC4   tactics/extraargs.ml4
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/check.ml
OCAMLC    checker/check_stat.ml
OCAMLOPT  checker/term.ml
OCAMLOPT -o plugins/micromega/csdpcert
OCAMLOPT  scripts/coqmktop.ml
OCAMLOPT -a -o lib/lib.cmxa
OCAMLOPT  kernel/term.ml
OCAMLC    tactics/tactics.mli
OCAMLC    tactics/hiddentac.mli
OCAMLC    tactics/elim.mli
OCAMLC    tactics/evar_tactics.mli
OCAMLC    tactics/decl_interp.mli
OCAMLC -a -o plugins/extraction/extraction_plugin.cma
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/dp/dp_zenon.ml
OCAMLC    plugins/dp/dp.ml
strip plugins/micromega/csdpcert
OCAMLC4   plugins/dp/g_dp.ml4
OCAMLC    plugins/funind/functional_principles_types.ml
OCAMLC4   tactics/tauto.ml4
OCAMLC    plugins/funind/merge.ml
OCAMLC    plugins/subtac/subtac_utils.ml
OCAMLC    plugins/subtac/eterm.ml
OCAMLC    plugins/subtac/subtac_coercion.ml
OCAMLC    plugins/subtac/subtac_pretyping.ml
OCAMLC    plugins/subtac/subtac_command.ml
OCAMLC    plugins/xml/xmlcommand.ml
OCAMLC4   plugins/xml/xmlentries.ml4
OCAMLOPT  plugins/xml/acic.ml
OCAMLC    plugins/quote/quote.ml
OCAMLC4   tactics/class_tactics.ml4
OCAMLC    plugins/romega/refl_omega.ml
OCAMLC    plugins/micromega/coq_micromega.ml
OCAMLC    plugins/rtauto/refl_tauto.ml
OCAMLC4   plugins/nsatz/nsatz.ml4
OCAMLOPT -o bin/coqdep
OCAMLOPT  tools/coqdoc/cpretty.ml
Testing dev/printers.cma
OCAMLC -a -o parsing/parsing.cma
OCAMLC    tactics/tactics.ml
OCAMLC    tactics/hiddentac.ml
OCAMLC -a dev/printers.cma
OCAMLC    tactics/elim.ml
OCAMLC    tactics/dhyp.ml
strip bin/coqdep
OCAMLC    tactics/auto.ml
OCAMLC    tactics/contradiction.ml
OCAMLC    tactics/leminv.ml
OCAMLC    tactics/evar_tactics.ml
OCAMLC    tactics/decl_interp.ml
OCAMLC    tactics/decl_proof_instr.ml
OCAMLC    toplevel/lemmas.ml
OCAMLC    toplevel/classes.ml
OCAMLC4   parsing/g_proofs.ml4
OCAMLC    tactics/refine.ml
OCAMLC4   tactics/eauto.ml4
OCAMLC    checker/indtypes.ml
OCAMLC    checker/mod_checking.ml
OCAMLC    checker/checker.ml
OCAMLOPT  checker/declarations.ml
OCAMLOPT -o bin/coqmktop.opt
OCAMLOPT  kernel/mod_subst.ml
OCAMLOPT  kernel/sign.ml
OCAMLOPT  kernel/cbytecodes.ml
OCAMLOPT  kernel/entries.ml
OCAMLOPT  kernel/vm.ml
OCAMLC    tactics/equality.mli
OCAMLC    plugins/cc/cctac.ml
OCAMLC4   plugins/cc/g_congruence.ml4
strip bin/coqmktop.opt
OCAMLC    plugins/firstorder/rules.ml
OCAMLC    plugins/firstorder/instances.mli
OCAMLC4   plugins/firstorder/g_ground.ml4
OCAMLC -a -o plugins/dp/dp_plugin.cma
OCAMLOPT  plugins/dp/dp_why.ml
OCAMLC    plugins/funind/recdef.ml
OCAMLC    plugins/funind/invfun.ml
OCAMLC -a -o plugins/subtac/subtac_plugin.cma
OCAMLC -a -o plugins/xml/xml_plugin.cma
OCAMLC4   plugins/quote/g_quote.ml4
OCAMLC    plugins/omega/coq_omega.ml
OCAMLC4   plugins/romega/g_romega.ml4
OCAMLC    plugins/ring/ring.ml
OCAMLC -a -o plugins/rtauto/rtauto_plugin.cma
OCAMLC -a -o plugins/nsatz/nsatz_plugin.cma
OCAMLOPT  tools/coqdoc/main.ml
OCAMLC    tactics/equality.ml
OCAMLC    tactics/inv.ml
OCAMLC    tactics/tacinterp.ml
OCAMLC    toplevel/auto_ind_decl.ml
OCAMLC -a -o parsing/highparsing.cma
OCAMLC4   tactics/eqdecide.ml4
OCAMLC    checker/safe_typing.ml
OCAMLOPT  checker/environ.ml
cd bin; ln -sf coqmktop.opt coqmktop
OCAMLOPT  kernel/cemitcodes.ml
OCAMLOPT  kernel/retroknowledge.ml
OCAMLOPT  library/libnames.ml
OCAMLC    tactics/autorewrite.mli
OCAMLC -a -o plugins/cc/cc_plugin.cma
OCAMLC    plugins/firstorder/instances.ml
OCAMLC    plugins/firstorder/ground.ml
OCAMLC    plugins/funind/functional_principles_proofs.ml
OCAMLC    plugins/funind/indfun.ml
OCAMLC -a -o plugins/quote/quote_plugin.cma
OCAMLC4   tactics/rewrite.ml4
OCAMLC4   plugins/omega/g_omega.ml4
OCAMLC -a -o plugins/romega/romega_plugin.cma
OCAMLC4   plugins/ring/g_ring.ml4
OCAMLC4   plugins/field/field.ml4
OCAMLC    plugins/fourier/fourierR.ml
OCAMLC4   plugins/micromega/g_micromega.ml4
OCAMLOPT -o bin/coqdoc
OCAMLC    tactics/autorewrite.ml
OCAMLC    toplevel/vernacentries.ml
OCAMLC4   tactics/extratactics.ml4
OCAMLC -a -o checker/check.cma
OCAMLOPT  checker/closure.ml
OCAMLOPT  checker/type_errors.ml
strip bin/coqdoc
OCAMLOPT  checker/modops.ml
OCAMLOPT  kernel/declarations.ml
OCAMLOPT  library/libobject.ml
OCAMLOPT  library/decl_kinds.ml
OCAMLC -a -o plugins/firstorder/ground_plugin.cma
OCAMLC4   plugins/funind/g_indfun.ml4
OCAMLC4   plugins/setoid_ring/newring.ml4
OCAMLC -a -o plugins/omega/omega_plugin.cma
OCAMLC -a -o plugins/ring/ring_plugin.cma
OCAMLC -a -o plugins/field/field_plugin.cma
OCAMLC4   plugins/fourier/g_fourier.ml4
OCAMLC -a -o plugins/micromega/micromega_plugin.cma
OCAMLC -a -o tactics/tactics.cma
OCAMLC -a -o toplevel/toplevel.cma
OCAMLC -o bin/coqchk.byte
OCAMLOPT  checker/reduction.ml
OCAMLOPT  kernel/pre_env.ml
OCAMLOPT  library/nametab.ml
OCAMLC -a -o plugins/fourier/fourier_plugin.cma
OCAMLC -a -o tactics/hightactics.cma
OCAMLOPT  kernel/cbytegen.ml
COQMKTOP -o bin/coqtop.byte
OCAMLC -a -o plugins/funind/recdef_plugin.cma
OCAMLOPT  checker/inductive.ml
OCAMLC -a -o plugins/setoid_ring/newring_plugin.cma
OCAMLOPT  kernel/environ.ml
OCAMLOPT  checker/typeops.ml
OCAMLOPT  kernel/closure.ml
OCAMLOPT  kernel/modops.ml
OCAMLOPT  kernel/csymtable.ml
OCAMLOPT  checker/indtypes.ml
OCAMLOPT  checker/subtyping.ml
OCAMLOPT  checker/mod_checking.ml
OCAMLOPT  kernel/reduction.ml
OCAMLOPT  checker/safe_typing.ml
OCAMLOPT  checker/check.ml
OCAMLOPT  checker/check_stat.ml
OCAMLOPT  checker/checker.ml
OCAMLOPT  kernel/type_errors.ml
OCAMLOPT  kernel/vconv.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  pretyping/vnorm.ml
OCAMLOPT  library/lib.ml
OCAMLOPT  kernel/term_typing.ml
OCAMLOPT  kernel/mod_typing.ml
OCAMLOPT  library/goptions.ml
OCAMLOPT  library/dischargedhypsmap.ml
OCAMLOPT  plugins/rtauto/proof_search.ml
OCAMLOPT  kernel/safe_typing.ml
OCAMLOPT -a -o kernel/kernel.cmxa
OCAMLOPT  library/global.ml
OCAMLOPT  pretyping/termops.ml
OCAMLOPT  library/decls.ml
OCAMLOPT  library/heads.ml
OCAMLOPT  pretyping/evd.ml
OCAMLOPT  pretyping/namegen.ml
OCAMLOPT  toplevel/discharge.ml
OCAMLOPT  parsing/printmod.ml
OCAMLOPT  pretyping/rawterm.ml
OCAMLOPT  pretyping/reductionops.ml
OCAMLOPT  interp/reserve.ml
OCAMLOPT  pretyping/inductiveops.ml
OCAMLOPT  pretyping/cbv.ml
OCAMLOPT  pretyping/detyping.ml
OCAMLOPT  pretyping/retyping.ml
OCAMLOPT  pretyping/pretype_errors.ml
OCAMLOPT  pretyping/pattern.ml
OCAMLOPT  pretyping/indrec.ml
OCAMLOPT  pretyping/evarutil.ml
OCAMLOPT  pretyping/matching.ml
OCAMLOPT  tactics/termdn.ml
OCAMLOPT  tactics/btermdn.ml
OCAMLOPT  interp/topconstr.ml
OCAMLOPT  pretyping/term_dnet.ml
OCAMLOPT  library/declaremods.ml
OCAMLOPT  pretyping/typeclasses_errors.ml
OCAMLOPT  library/impargs.ml
OCAMLOPT  pretyping/typeclasses.ml
OCAMLOPT  interp/dumpglob.ml
OCAMLOPT  interp/implicit_quantifiers.ml
OCAMLOPT  library/library.ml
OCAMLOPT  library/states.ml
OCAMLOPT  pretyping/recordops.ml
OCAMLOPT  tactics/nbtermdn.ml
OCAMLOPT -a -o library/library.cmxa
OCAMLOPT  pretyping/evarconv.ml
OCAMLOPT  pretyping/typing.ml
OCAMLOPT  pretyping/tacred.ml
OCAMLOPT  pretyping/classops.ml
OCAMLOPT  proofs/redexpr.ml
OCAMLOPT  pretyping/coercion.ml
OCAMLOPT  interp/notation.ml
OCAMLOPT  pretyping/unification.ml
OCAMLOPT  pretyping/cases.ml
OCAMLOPT  interp/genarg.ml
OCAMLOPT  interp/syntax_def.ml
OCAMLOPT  interp/constrextern.ml
OCAMLOPT  library/declare.ml
OCAMLOPT  interp/smartlocate.ml
OCAMLOPT  proofs/tacexpr.ml
OCAMLOPT  parsing/extrawit.ml
OCAMLOPT  toplevel/ind_tables.ml
OCAMLOPT  toplevel/libtypes.ml
OCAMLOPT  proofs/proof_type.ml
OCAMLOPT4 parsing/pcoq.ml4
OCAMLOPT  toplevel/vernacexpr.ml
OCAMLOPT  tactics/elimschemes.ml
OCAMLOPT  pretyping/clenv.ml
OCAMLOPT  proofs/proof_trees.ml
OCAMLOPT  pretyping/pretyping.ml
OCAMLOPT  interp/coqlib.ml
OCAMLOPT  parsing/ppconstr.ml
OCAMLOPT  proofs/logic.ml
OCAMLOPT  tactics/eqschemes.ml
OCAMLOPT  parsing/egrammar.ml
OCAMLOPT4 parsing/g_xml.ml4
OCAMLOPT4 parsing/g_constr.ml4
OCAMLOPT4 parsing/g_prim.ml4
OCAMLOPT4 parsing/g_tactic.ml4
OCAMLOPT4 parsing/g_ltac.ml4
OCAMLOPT4 parsing/g_decl_mode.ml4
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 -a -o pretyping/pretyping.cmxa
OCAMLOPT  interp/constrintern.ml
OCAMLOPT  proofs/refiner.ml
OCAMLOPT  plugins/syntax/string_syntax.ml
OCAMLOPT  proofs/tactic_debug.ml
OCAMLOPT  interp/modintern.ml
OCAMLOPT  proofs/evar_refiner.ml
OCAMLOPT  proofs/tacmach.ml
OCAMLOPT -a -o interp/interp.cmxa
OCAMLOPT  proofs/pfedit.ml
OCAMLOPT  proofs/clenvtac.ml
OCAMLOPT  plugins/cc/ccalgo.ml
OCAMLOPT  plugins/romega/const_omega.ml
OCAMLOPT  proofs/decl_mode.ml
OCAMLOPT  tactics/tacticals.ml
OCAMLOPT -a -o proofs/proofs.cmxa
OCAMLOPT  parsing/printer.ml
OCAMLOPT4 tactics/hipattern.ml4
OCAMLOPT  plugins/cc/ccproof.ml
OCAMLOPT  parsing/pptactic.ml
OCAMLOPT  parsing/prettyp.ml
OCAMLOPT  toplevel/class.ml
OCAMLOPT  toplevel/search.ml
OCAMLOPT  plugins/extraction/table.ml
OCAMLOPT  plugins/funind/indfun_common.ml
OCAMLOPT  plugins/subtac/subtac_errors.ml
OCAMLOPT  plugins/xml/doubleTypeInference.ml
OCAMLOPT  tactics/tactics.ml
OCAMLOPT  plugins/firstorder/formula.ml
OCAMLOPT  plugins/funind/rawtermops.ml
OCAMLOPT  plugins/extraction/mlutil.ml
OCAMLOPT  plugins/xml/cic2acic.ml
OCAMLOPT  parsing/ppdecl_proof.ml
OCAMLOPT  toplevel/himsg.ml
OCAMLOPT  plugins/firstorder/unify.ml
OCAMLOPT  parsing/tactic_printer.ml
OCAMLOPT  plugins/extraction/modutil.ml
OCAMLOPT  plugins/extraction/extraction.ml
OCAMLOPT  plugins/xml/proof2aproof.ml
OCAMLOPT -a -o parsing/parsing.cmxa
OCAMLOPT4 plugins/xml/acic2Xml.ml4
OCAMLOPT  plugins/extraction/common.ml
OCAMLOPT  plugins/extraction/ocaml.ml
OCAMLOPT  plugins/extraction/haskell.ml
OCAMLOPT  plugins/extraction/scheme.ml
OCAMLOPT4 plugins/xml/proofTree2Xml.ml4
OCAMLOPT  toplevel/cerrors.ml
OCAMLOPT  toplevel/autoinstance.ml
OCAMLOPT  tactics/hiddentac.ml
OCAMLOPT  tactics/dhyp.ml
OCAMLOPT  tactics/contradiction.ml
OCAMLOPT  plugins/dp/dp_zenon.ml
OCAMLOPT  plugins/quote/quote.ml
OCAMLOPT  plugins/romega/refl_omega.ml
OCAMLOPT  plugins/micromega/coq_micromega.ml
OCAMLOPT  tactics/elim.ml
OCAMLOPT  tactics/auto.ml
OCAMLOPT  toplevel/lemmas.ml
OCAMLOPT  plugins/extraction/extract_env.ml
OCAMLOPT  plugins/dp/dp.ml
OCAMLOPT  plugins/subtac/subtac_utils.ml
OCAMLOPT  tactics/equality.ml
OCAMLOPT  plugins/firstorder/sequent.ml
OCAMLOPT  plugins/subtac/subtac_cases.ml
OCAMLOPT  plugins/firstorder/rules.ml
OCAMLOPT  plugins/firstorder/instances.ml
OCAMLOPT  tactics/inv.ml
OCAMLOPT  toplevel/auto_ind_decl.ml
OCAMLOPT  plugins/omega/coq_omega.ml
OCAMLOPT  tactics/leminv.ml
OCAMLOPT  tactics/tacinterp.ml
OCAMLOPT  toplevel/indschemes.ml
OCAMLOPT  tactics/evar_tactics.ml
OCAMLOPT  toplevel/vernacinterp.ml
OCAMLOPT  tactics/decl_interp.ml
OCAMLOPT  tactics/tactic_option.ml
OCAMLOPT  toplevel/metasyntax.ml
OCAMLOPT  parsing/ppvernac.ml
OCAMLOPT  toplevel/mltop.optml
OCAMLOPT4 tactics/tauto.ml4
OCAMLOPT4 plugins/extraction/g_extraction.ml4
OCAMLOPT  plugins/extraction/extraction_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
OCAMLOPT4 plugins/dp/g_dp.ml4
OCAMLOPT  plugins/dp/dp_plugin_mod.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
OCAMLOPT4 plugins/xml/dumptree.ml4
OCAMLOPT  plugins/xml/xml_plugin_mod.ml
OCAMLOPT  plugins/syntax/z_syntax_plugin_mod.ml
OCAMLOPT4 plugins/quote/g_quote.ml4
OCAMLOPT  plugins/quote/quote_plugin_mod.ml
OCAMLOPT  plugins/setoid_ring/newring_plugin_mod.ml
OCAMLOPT4 plugins/omega/g_omega.ml4
OCAMLOPT  plugins/omega/omega_plugin_mod.ml
OCAMLOPT4 plugins/romega/g_romega.ml4
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
OCAMLOPT4 plugins/nsatz/nsatz.ml4
OCAMLOPT  plugins/nsatz/nsatz_plugin_mod.ml
OCAMLOPT  tactics/autorewrite.ml
OCAMLOPT  tactics/decl_proof_instr.ml
OCAMLOPT  toplevel/command.ml
OCAMLOPT4 parsing/g_vernac.ml4
OCAMLOPT4 tactics/extraargs.ml4
OCAMLOPT  plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLOPT -a -o plugins/extraction/extraction_plugin.cmxa
OCAMLOPT4 plugins/cc/g_congruence.ml4
OCAMLOPT -a -o plugins/dp/dp_plugin.cmxa
OCAMLOPT  plugins/funind/rawterm_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
OCAMLOPT4 plugins/ring/g_ring.ml4
OCAMLOPT4 plugins/field/field.ml4
OCAMLOPT  plugins/fourier/fourierR.ml
OCAMLOPT -a -o plugins/syntax/numbers_syntax_plugin.cmxa
OCAMLOPT4 plugins/micromega/g_micromega.ml4
OCAMLOPT4 plugins/rtauto/g_rtauto.ml4
OCAMLOPT -a -o plugins/nsatz/nsatz_plugin.cmxa
OCAMLOPT -a -o tactics/tactics.cmxa
OCAMLOPT  toplevel/classes.ml
OCAMLOPT4 toplevel/whelp.ml4
OCAMLOPT  tactics/refine.ml
OCAMLOPT4 tactics/eauto.ml4
OCAMLOPT -a -o plugins/syntax/nat_syntax_plugin.cmxa
OCAMLOPT -shared -o plugins/extraction/extraction_plugin.cmxs
OCAMLOPT -a -o plugins/cc/cc_plugin.cmxa
OCAMLOPT4 plugins/firstorder/g_ground.ml4
OCAMLOPT -shared -o plugins/dp/dp_plugin.cmxs
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
OCAMLOPT4 plugins/fourier/g_fourier.ml4
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
OCAMLOPT4 parsing/g_proofs.ml4
OCAMLOPT4 tactics/extratactics.ml4
OCAMLOPT4 tactics/class_tactics.ml4
OCAMLOPT -shared -o plugins/syntax/nat_syntax_plugin.cmxs
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 -a -o parsing/highparsing.cmxa
OCAMLOPT -shared -o plugins/firstorder/ground_plugin.cmxs
OCAMLOPT  plugins/subtac/subtac_command.ml
OCAMLOPT -shared -o plugins/fourier/fourier_plugin.cmxs
OCAMLOPT4 tactics/rewrite.ml4
OCAMLOPT  toplevel/vernac.ml
OCAMLOPT  plugins/funind/recdef.ml
OCAMLOPT  plugins/funind/invfun.ml
OCAMLOPT  toplevel/toplevel.ml
OCAMLOPT4 tactics/eqdecide.ml4
OCAMLOPT  plugins/subtac/subtac_classes.ml
OCAMLOPT  plugins/xml/xmlcommand.ml
OCAMLOPT  toplevel/coqinit.ml
OCAMLOPT  plugins/subtac/subtac.ml
OCAMLOPT  toplevel/coqtop.ml
OCAMLOPT4 plugins/xml/xmlentries.ml4
OCAMLOPT4 plugins/subtac/g_subtac.ml4
OCAMLOPT -a -o toplevel/toplevel.cmxa
OCAMLOPT  plugins/funind/functional_principles_proofs.ml
OCAMLOPT -a -o plugins/xml/xml_plugin.cmxa
OCAMLOPT -shared -o plugins/xml/xml_plugin.cmxs
OCAMLOPT -a -o plugins/subtac/subtac_plugin.cmxa
OCAMLOPT -shared -o plugins/subtac/subtac_plugin.cmxs
OCAMLOPT  plugins/funind/functional_principles_types.ml
OCAMLOPT -a -o tactics/hightactics.cmxa
OCAMLOPT4 plugins/setoid_ring/newring.ml4
COQMKTOP -o bin/coqtop.opt
OCAMLOPT  plugins/funind/indfun.ml
OCAMLOPT4 plugins/funind/g_indfun.ml4
OCAMLOPT -a -o plugins/setoid_ring/newring_plugin.cmxa
OCAMLOPT -shared -o plugins/setoid_ring/newring_plugin.cmxs
OCAMLOPT -a -o plugins/funind/recdef_plugin.cmxa
OCAMLOPT -shared -o plugins/funind/recdef_plugin.cmxs
strip bin/coqtop.opt
cd bin; ln -sf coqtop.opt coqtop
COQC -nois theories/Init/Notations.v
OCAMLOPT -o bin/coqc.opt
COQC -nois theories/Init/Logic.v
Defining 'IF' as keyword
Defining 'exists2' as keyword
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
strip bin/coqc.opt
cd bin; ln -sf coqc.opt coqc
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
COQC      theories/Arith/EqNat.v
COQC      theories/Logic/EqdepFacts.v
COQC      theories/Bool/Sumbool.v
COQC      theories/Arith/Even.v
COQC      theories/Relations/Relation_Operators.v
COQC      theories/Bool/Bool.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/DecBool.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/Permut.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.v
COQC      theories/Unicode/Utf8_core.v
COQC      theories/Program/Utils.v
COQC      theories/Program/Combinators.v
COQC      plugins/extraction/ExtrOcamlBasic.v
COQC      theories/Arith/Lt.v
COQC      theories/Classes/RelationClasses.v
COQC      theories/Arith/Peano_dec.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/Bool/BoolEq.v
COQC      theories/Bool/IfProp.v
COQC      theories/Lists/StreamMemo.v
COQC      theories/Sets/Constructive_sets.v
COQC      theories/Sets/Partial_Order.v
COQC      theories/Sets/Relations_1_facts.v
COQC      theories/Sets/Relations_2.v
COQC      theories/Sets/Uniset.v
COQC      theories/Wellfounded/Lexicographic_Product.v
COQC      theories/Wellfounded/Union.v
COQC      plugins/ring/Ring_normalize.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/NArith/BinPos.v
COQC      theories/Relations/Relations.v
COQC      theories/Structures/Equalities.v
COQC      theories/Logic/Classical_Prop.v
COQC      theories/Sets/Cpo.v
COQC      theories/Sets/Finite_sets.v
COQC      theories/Sets/Relations_2_facts.v
COQC      theories/Sets/Relations_3.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      theories/Sets/Relations_3_facts.v
COQC      theories/Classes/RelationPairs.v
COQC      plugins/ring/Ring_abstract.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/Sets/Powerset_facts.v
COQC      theories/Setoids/Setoid.v
COQC      theories/NArith/BinNat.v
COQC      theories/Arith/Div2.v
COQC      theories/NArith/Pnat.v
COQC      theories/Logic/ClassicalUniqueChoice.v
COQC      theories/Arith/Bool_nat.v
COQC      theories/Sets/Classical_sets.v
COQC      theories/Sets/Multiset.v
COQC      plugins/ring/LegacyRing.v
COQC      theories/Numbers/NumPrelude.v
COQC      plugins/ring/Setoid_ring_theory.v
COQC      theories/Arith/Wf_nat.v
COQC      theories/Structures/Orders.v
COQC      theories/ZArith/BinInt.v
COQC      plugins/setoid_ring/Ring_theory.v
COQC      theories/Sets/Powerset_Classical_facts.v
COQC      plugins/funind/Recdef.v
COQC      theories/Arith/Arith_base.v
COQC      theories/Structures/OrdersTac.v
COQC      theories/Arith/Euclid.v
COQC      theories/Sets/Finite_sets_facts.v
COQC      theories/ZArith/Zcompare.v
COQC      theories/ZArith/Zeven.v
COQC      plugins/ring/Setoid_ring_normalize.v
COQC      theories/Arith/NatOrderedType.v
COQC      theories/Structures/OrdersFacts.v
COQC      theories/NArith/POrderedType.v
COQC      theories/NArith/NOrderedType.v
COQC      theories/Sets/Image.v
COQC      theories/ZArith/Zorder.v
COQC      plugins/setoid_ring/Ring_equiv.v
COQC      theories/Structures/GenericMinMax.v
COQC      theories/Sets/Infinite_sets.v
COQC      theories/ZArith/ZArith_dec.v
COQC      theories/ZArith/auxiliary.v
COQC      theories/ZArith/Zmisc.v
COQC      theories/Sets/Integers.v
COQC      theories/ZArith/Zbool.v
COQC      theories/ZArith/ZOrderedType.v
COQC      theories/Arith/MinMax.v
COQC      theories/ZArith/Zminmax.v
COQC      theories/NArith/Pminmax.v
COQC      theories/Numbers/NatInt/NZAxioms.v
COQC      theories/Numbers/Integer/Abstract/ZAxioms.v
COQC      theories/Numbers/NatInt/NZBase.v
COQC      theories/Numbers/Natural/Abstract/NAxioms.v
COQC      theories/Arith/Min.v
COQC      theories/Arith/Max.v
COQC      theories/ZArith/Zmax.v
COQC      theories/ZArith/Zmin.v
COQC      theories/Numbers/NatInt/NZAdd.v
COQC      theories/Numbers/NatInt/NZOrder.v
COQC      theories/Lists/List.v
COQC      theories/Arith/Compare.v
COQC      theories/ZArith/Znat.v
COQC      theories/Numbers/NatInt/NZMul.v
COQC      plugins/ring/Setoid_ring.v
COQC      theories/NArith/Nnat.v
COQC      theories/ZArith/Zabs.v
COQC      theories/ZArith/Wf_Z.v
COQC      theories/Numbers/NatInt/NZAddOrder.v
COQC      theories/NArith/Nminmax.v
COQC      theories/Strings/Ascii.v
COQC      theories/ZArith/Zhints.v
COQC      theories/ZArith/ZArith_base.v
COQC      theories/Numbers/NatInt/NZMulOrder.v
COQC      theories/Numbers/NatInt/NZDomain.v
COQC      theories/Lists/ListTactics.v
COQC      theories/Lists/ListSet.v
COQC      theories/Sorting/Sorted.v
COQC      theories/Sorting/Permutation.v
COQC      theories/Lists/TheoryList.v
COQC      theories/Wellfounded/Lexicographic_Exponentiation.v
COQC      theories/Reals/Rdefinitions.v
COQC      plugins/field/LegacyField_Compl.v
COQC      theories/Numbers/NaryFunctions.v
COQC      plugins/micromega/Refl.v
COQC      plugins/rtauto/Bintree.v
COQC      plugins/setoid_ring/BinList.v
COQC      theories/ZArith/Zpow_def.v
COQC      theories/ZArith/ZOdiv_def.v
COQC      plugins/omega/OmegaLemmas.v
COQC      plugins/romega/ReflOmegaCore.v
COQC      theories/Sorting/Mergesort.v
COQC      theories/Wellfounded/Wellfounded.v
COQC      theories/Reals/Raxioms.v
COQC      theories/Reals/Rpow_def.v
COQC      plugins/field/LegacyField_Theory.v
COQC      theories/Numbers/NatInt/NZProperties.v
COQC      theories/Numbers/NatInt/NZDiv.v
COQC      plugins/micromega/CheckerMaker.v
Defining 'mod' as keyword
COQC      plugins/micromega/Tauto.v
COQC      plugins/rtauto/Rtauto.v
COQC      plugins/setoid_ring/Ring_polynom.v
COQC      theories/Sorting/Sorting.v
COQC      plugins/field/LegacyField_Tactic.v
COQC      theories/Numbers/Integer/Abstract/ZBase.v
COQC      theories/Numbers/Natural/Abstract/NBase.v
COQC      theories/Lists/SetoidList.v
COQC      plugins/field/LegacyField.v
COQC      theories/Numbers/Integer/Abstract/ZAdd.v
COQC      theories/Reals/LegacyRfield.v
COQC      theories/Numbers/Natural/Abstract/NAdd.v
COQC      theories/Numbers/Natural/Abstract/NIso.v
COQC      theories/Numbers/Integer/Abstract/ZMul.v
COQC      theories/Numbers/Natural/Abstract/NOrder.v
COQC      theories/Numbers/Integer/Abstract/ZLt.v
COQC      theories/Numbers/Integer/Abstract/ZAddOrder.v
COQC      theories/Numbers/Natural/Abstract/NAddOrder.v
COQC      theories/Structures/DecidableType.v
COQC      theories/Structures/OrderedType.v
COQC      theories/MSets/MSetInterface.v
COQC      theories/Structures/OrdersLists.v
COQC      theories/Structures/EqualitiesFacts.v
COQC      theories/Numbers/Integer/Abstract/ZMulOrder.v
COQC      theories/Numbers/Natural/Abstract/NMulOrder.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      theories/Structures/OrdersEx.v
COQC      theories/MSets/MSetPositive.v
COQC      theories/Numbers/Integer/Abstract/ZSgnAbs.v
COQC      theories/Numbers/Natural/Abstract/NSub.v
COQC      theories/FSets/FMapList.v
COQC      theories/FSets/FMapWeakList.v
COQC      theories/FSets/FSetBridge.v
COQC      theories/Numbers/Integer/Abstract/ZProperties.v
COQC      theories/Numbers/Natural/Abstract/NProperties.v
COQC      theories/Numbers/Natural/Abstract/NStrongRec.v
COQC      theories/Numbers/Natural/Binary/NBinary.v
COQC      theories/Numbers/Integer/Abstract/ZDivFloor.v
COQC      theories/Numbers/Integer/Abstract/ZDivTrunc.v
COQC      theories/Numbers/Integer/Abstract/ZDivEucl.v
COQC      theories/Numbers/Natural/Abstract/NDiv.v
COQC      theories/Numbers/Integer/Binary/ZBinary.v
COQC      theories/Numbers/Natural/Abstract/NDefOps.v
COQC      plugins/setoid_ring/InitialRing.v
COQC      plugins/setoid_ring/Ring_tac.v
COQC      plugins/setoid_ring/Ring_base.v
COQC      plugins/setoid_ring/Ring.v
COQC      plugins/setoid_ring/ArithRing.v
COQC      plugins/setoid_ring/NArithRing.v
COQC      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/Logic/ChoiceFacts.v
COQC      theories/Logic/ConstructiveEpsilon.v
COQC      theories/Bool/Bvector.v
COQC      theories/Bool/Zerob.v
COQC      theories/Strings/String.v
COQC      theories/Numbers/Natural/Peano/NPeano.v
COQC      theories/Program/Syntax.v
COQC      plugins/ring/LegacyArithRing.v
COQC      plugins/extraction/ExtrOcamlNatInt.v
COQC      plugins/extraction/ExtrOcamlNatBigInt.v
Defining 'mod' as keyword
COQC      theories/Logic/ClassicalChoice.v
COQC      theories/Logic/ClassicalDescription.v
COQC      theories/Logic/ClassicalEpsilon.v
COQC      theories/Logic/Description.v
COQC      theories/Logic/Diaconescu.v
COQC      theories/Logic/Epsilon.v
COQC      theories/Logic/IndefiniteDescription.v
COQC      theories/NArith/Ndigits.v
COQC      theories/Program/Program.v
COQC      plugins/ring/LegacyZArithRing.v
COQC      plugins/extraction/ExtrOcamlString.v
COQC      theories/Classes/EquivDec.v
COQC      theories/Classes/Morphisms_Relations.v
COQC      theories/Classes/SetoidClass.v
COQC      theories/NArith/NArith.v
COQC      theories/NArith/Ndec.v
COQC      theories/NArith/Ndist.v
COQC      plugins/omega/PreOmega.v
COQC      theories/Classes/SetoidDec.v
COQC      plugins/ring/LegacyNArithRing.v
COQC      plugins/omega/Omega.v
COQC      plugins/romega/ROmega.v
COQC      theories/ZArith/Zcomplements.v
COQC      theories/ZArith/Zwf.v
COQC      theories/ZArith/Zsqrt.v
COQC      theories/Sorting/PermutSetoid.v
COQC      theories/ZArith/Zpower.v
COQC      theories/ZArith/Zdiv.v
Defining 'mod' as keyword
COQC      theories/ZArith/Zlogarithm.v
COQC      theories/Sorting/Heap.v
COQC      theories/Sorting/PermutEq.v
COQC      theories/ZArith/ZArith.v
COQC      theories/ZArith/Znumtheory.v
COQC      theories/ZArith/ZOdiv.v
Defining 'mod' as keyword
COQC      theories/ZArith/Int.v
COQC      theories/ZArith/Zdigits.v
COQC      theories/Structures/OrderedTypeEx.v
COQC      theories/MSets/MSetAVL.v
COQC      theories/QArith/QArith_base.v
COQC      theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
COQC      plugins/micromega/Env.v
COQC      plugins/micromega/VarMap.v
COQC      plugins/dp/Dp.v
COQC      plugins/extraction/ExtrOcamlIntConv.v
COQC      plugins/extraction/ExtrOcamlBigIntConv.v
COQC      plugins/extraction/ExtrOcamlZInt.v
COQC      plugins/extraction/ExtrOcamlZBigInt.v
COQC      theories/ZArith/Zgcd_alt.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/FSetPositive.v
COQC      theories/QArith/Qreduction.v
COQC      theories/QArith/QOrderedType.v
COQC      theories/Numbers/BigNumPrelude.v
COQC      theories/Numbers/Cyclic/Int31/Int31.v
COQC      theories/Numbers/Natural/SpecViaZ/NSig.v
COQC      theories/Numbers/Integer/SpecViaZ/ZSig.v
COQC      plugins/micromega/EnvRing.v
COQC      theories/FSets/FMapFacts.v
COQC      theories/FSets/FSetFacts.v
COQC      theories/MSets/MSetFacts.v
COQC      plugins/setoid_ring/Field_tac.v
COQC      theories/QArith/Qminmax.v
COQC      theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
COQC      theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
COQC      theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
COQC      theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
COQC      theories/Numbers/Integer/BigZ/ZMake.v
COQC      theories/FSets/FSetCompat.v
COQC      theories/FSets/FSetDecide.v
COQC      theories/FSets/FSetList.v
COQC      theories/FSets/FSetWeakList.v
COQC      theories/MSets/MSetDecide.v
COQC      plugins/setoid_ring/Field.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      plugins/micromega/RingMicromega.v
COQC      theories/FSets/FMapFullAVL.v
COQC      theories/FSets/FMaps.v
COQC      theories/FSets/FSetAVL.v
COQC      theories/FSets/FSetProperties.v
COQC      theories/MSets/MSetProperties.v
COQC      plugins/setoid_ring/RealField.v
COQC      theories/QArith/Qfield.v
COQC      theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
COQC      plugins/micromega/ZCoeff.v
COQC      theories/FSets/FSetEqProperties.v
COQC      theories/FSets/FSetToFiniteSet.v
COQC      theories/MSets/MSetEqProperties.v
COQC      theories/MSets/MSetToFiniteSet.v
COQC      theories/Reals/RIneq.v
COQC      theories/QArith/Qring.v
COQC      theories/QArith/Qpower.v
COQC      theories/Numbers/Cyclic/Int31/Ring31.v
COQC      theories/FSets/FSets.v
COQC      theories/MSets/MSets.v
COQC      theories/Reals/DiscrR.v
COQC      theories/QArith/QArith.v
COQC      theories/Reals/Rbase.v
COQC      theories/QArith/Qabs.v
COQC      theories/QArith/Qcanon.v
COQC      theories/QArith/Qround.v
COQC      theories/Numbers/Rational/SpecViaQ/QSig.v
COQC      plugins/micromega/ZMicromega.v
COQC      plugins/micromega/QMicromega.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/Qreals.v
COQC      theories/Numbers/Rational/BigQ/QMake.v
COQC      plugins/fourier/Fourier.v
COQC      plugins/micromega/RMicromega.v
COQC      theories/Reals/Rbasic_fun.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/Reals/Rfunctions.v
COQC      theories/Reals/Rseries.v
COQC      theories/Reals/Rlimit.v
COQC      theories/Reals/RList.v
COQC      theories/Reals/SeqProp.v
COQC      theories/Reals/Rderiv.v
COQC      theories/Reals/Ranalysis1.v
COQC      theories/Reals/Rcomplete.v
Defining 'o' as 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/Ranalysis3.v
COQC      theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
COQC      theories/Reals/Rprod.v
COQC      theories/Reals/MVT.v
COQC      theories/Numbers/Natural/BigN/Nbasic.v
COQC      theories/Numbers/Natural/BigN/NMake_gen.v
COQC      theories/Reals/SeqSeries.v
COQC      theories/Reals/Rtrigo_fun.v
COQC      theories/Reals/PSeries_reg.v
COQC      theories/Reals/Rsqrt_def.v
COQC      theories/Reals/Rtrigo_def.v
COQC      theories/Reals/R_sqrt.v
COQC      theories/Reals/Cos_rel.v
COQC      theories/Reals/Rtrigo_alt.v
COQC      theories/Reals/Sqrt_reg.v
COQC      theories/Reals/Cos_plus.v
COQC      theories/Reals/Rtrigo.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/Reals/Rpower.v
COQC      theories/Reals/Ranalysis.v
COQC      theories/Reals/NewtonInt.v
COQC      theories/Reals/RiemannInt_SF.v
COQC      theories/Reals/RiemannInt.v
COQC      theories/Numbers/Natural/BigN/NMake.v
COQC      theories/Numbers/Natural/BigN/BigN.v
COQC      theories/Reals/Integration.v
COQC      theories/Reals/Rlogic.v
COQC      theories/Numbers/Integer/BigZ/BigZ.v
COQC      theories/Reals/Reals.v
COQC      plugins/nsatz/Nsatz.v
COQC      theories/Numbers/Rational/BigQ/BigQ.v
make[1]: Leaving directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1'
=> Unwrapping files-to-be-installed.