=> Bootstrap dependency digest>=20010302: found digest-20111104 => Bootstrap dependency fetch-[0-9]*: found fetch-1.7 ===> Building for coq-8.3pl1nb16 ***************************************************** ***************************************************** ****************** 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 CCDEP kernel/byterun/coq_values.c 455 states, 31494 transitions, table size 128706 bytes CCDEP kernel/byterun/coq_memory.c 457 states, 31161 transitions, table size 127386 bytes 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/conv_oracle.mli OCAMLDEP kernel/retroknowledge.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/modops.mli OCAMLDEP kernel/esubst.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 dev/ocamlweb-doc/lex.ml OCAMLDEP plugins/dp/dp_zenon.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 File "parsing/g_ltac.ml4", line 31, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 parsing/g_tactic.ml4 File "parsing/q_constr.ml4", line 30, characters 2-8: Parse error: Deprecated syntax, the grammar module is expected OCAMLDEP4 parsing/g_prim.ml4 File "parsing/g_prim.ml4", line 36, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/g_constr.ml4", line 126, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 parsing/vernacextend.ml4 OCAMLDEP4 parsing/tacextend.ml4 File "parsing/vernacextend.ml4", line 57, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) OCAMLDEP4 parsing/argextend.ml4 File "parsing/g_tactic.ml4", line 219, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 parsing/pcoq.ml4 File "parsing/tacextend.ml4", line 168, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) OCAMLDEP4 parsing/q_util.ml4 File "parsing/q_util.ml4", line 31, characters 38-55: While expanding quotation "patt" in a position of "expr": Parse error: EOI expected after [quotation of pattern] (in [quotation of pattern]) OCAMLDEP4 lib/pp.ml4 File "parsing/pcoq.ml4", line 186, characters 2-9: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 lib/compat.ml4 File "parsing/argextend.ml4", line 153, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) 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 plugins/field/field.ml parsing/q_coqast.ml toplevel/whelp.ml plugins/firstorder/g_ground.ml lib/compat.ml tactics/eauto.ml parsing/g_decl_mode.ml plugins/extraction/g_extraction.ml tactics/rewrite.ml plugins/romega/g_romega.ml plugins/xml/xmlentries.ml tactics/hipattern.ml plugins/fourier/g_fourier.ml parsing/lexer.ml parsing/g_vernac.ml plugins/funind/g_indfun.ml toplevel/mltop.ml plugins/dp/g_dp.ml plugins/xml/xml.ml plugins/xml/acic2Xml.ml plugins/ring/g_ring.ml plugins/quote/g_quote.ml plugins/rtauto/g_rtauto.ml lib/pp.ml plugins/omega/g_omega.ml plugins/xml/dumptree.ml tactics/extraargs.ml tactics/extratactics.ml plugins/xml/proofTree2Xml.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 tools/coq_makefile.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' 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 OCAMLDEP4 parsing/q_constr.ml4 OCAMLDEP4 parsing/g_constr.ml4 OCAMLDEP4 parsing/g_ltac.ml4 OCAMLDEP4 parsing/g_tactic.ml4 OCAMLDEP4 parsing/g_prim.ml4 File "parsing/g_ltac.ml4", line 31, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 parsing/vernacextend.ml4 File "parsing/g_prim.ml4", line 36, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/q_constr.ml4", line 30, characters 2-8: Parse error: Deprecated syntax, the grammar module is expected OCAMLDEP4 parsing/tacextend.ml4 OCAMLDEP4 parsing/argextend.ml4 File "parsing/g_constr.ml4", line 126, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead OCAMLDEP4 parsing/pcoq.ml4 File "parsing/vernacextend.ml4", line 57, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) OCAMLDEP4 parsing/q_util.ml4 File "parsing/g_tactic.ml4", line 219, characters 0-7: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead File "parsing/q_util.ml4", line 31, characters 38-55: While expanding quotation "patt" in a position of "expr": Parse error: EOI expected after [quotation of pattern] (in [quotation of pattern]) File "parsing/tacextend.ml4", line 168, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) File "parsing/argextend.ml4", line 153, characters 4-11: While expanding quotation "str_item" in a position of "expr": Parse error: EOI expected after [quotation of structure item] (in [quotation of structure item]) File "parsing/pcoq.ml4", line 186, characters 2-9: Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead make[1]: *** No rule to make target `parsing/q_constr.ml4.ml.d', needed by `parsing/q_constr.cmo'. Stop. make[1]: *** Waiting for unfinished jobs.... OCAMLC -o bin/coqdep_boot rm lib/refutpat.ml tactics/class_tactics.ml parsing/g_vernac.ml plugins/micromega/g_micromega.ml tools/coq_tex.ml plugins/field/field.ml parsing/g_decl_mode.ml plugins/quote/g_quote.ml tools/coq_makefile.ml toplevel/whelp.ml lib/compat.ml plugins/xml/dumptree.ml parsing/g_xml.ml plugins/extraction/g_extraction.ml tactics/hipattern.ml tactics/tauto.ml plugins/fourier/g_fourier.ml plugins/dp/g_dp.ml plugins/cc/g_congruence.ml plugins/romega/g_romega.ml plugins/xml/xml.ml plugins/xml/xmlentries.ml plugins/firstorder/g_ground.ml plugins/funind/g_indfun.ml plugins/rtauto/g_rtauto.ml lib/pp.ml tactics/eauto.ml plugins/xml/proofTree2Xml.ml plugins/ring/g_ring.ml tactics/extratactics.ml plugins/setoid_ring/newring.ml tactics/extraargs.ml parsing/lexer.ml parsing/q_coqast.ml toplevel/mltop.ml parsing/g_proofs.ml plugins/nsatz/nsatz.ml plugins/subtac/g_subtac.ml plugins/xml/acic2Xml.ml tactics/eqdecide.ml plugins/omega/g_omega.ml tactics/rewrite.ml make[1]: Leaving directory `/tmp/pkgsrc/lang/coq/work/coq-8.3pl1' make: *** [stage1] Error 2 *** Error code 2 Stop. bmake: stopped in /usr/pkgsrc/lang/coq *** Error code 1 Stop. bmake: stopped in /usr/pkgsrc/lang/coq