diff options
Diffstat (limited to '.depend')
| -rw-r--r-- | .depend | 351 |
1 files changed, 126 insertions, 225 deletions
@@ -122,7 +122,7 @@ lib/util.cmi: lib/pp.cmi lib/compat.cmo parsing/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \ interp/ppextend.cmi parsing/pcoq.cmi kernel/names.cmi \ - kernel/mod_subst.cmi interp/genarg.cmi parsing/extend.cmi + kernel/mod_subst.cmi interp/genarg.cmi parsing/extend.cmi lib/compat.cmo parsing/extend.cmi: lib/util.cmi parsing/g_minicoq.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi \ kernel/environ.cmi @@ -130,7 +130,7 @@ parsing/lexer.cmi: lib/util.cmi lib/pp.cmi parsing/pcoq.cmi: toplevel/vernacexpr.cmo lib/util.cmi interp/topconstr.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi kernel/names.cmi \ library/libnames.cmi interp/genarg.cmi parsing/extend.cmi \ - library/decl_kinds.cmo proofs/decl_expr.cmi lib/bigint.cmi + library/decl_kinds.cmo proofs/decl_expr.cmi lib/compat.cmo lib/bigint.cmi parsing/ppconstr.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi interp/ppextend.cmi lib/pp.cmi \ parsing/pcoq.cmi kernel/names.cmi library/libnames.cmi interp/genarg.cmi \ @@ -429,7 +429,8 @@ contrib/extraction/ocaml.cmi: lib/pp.cmi kernel/names.cmi \ contrib/extraction/scheme.cmi: lib/pp.cmi kernel/names.cmi \ contrib/extraction/miniml.cmi contrib/extraction/table.cmi: kernel/term.cmi kernel/names.cmi \ - contrib/extraction/miniml.cmi library/libnames.cmi kernel/environ.cmi + contrib/extraction/miniml.cmi library/libnames.cmi kernel/environ.cmi \ + kernel/declarations.cmi contrib/first-order/formula.cmi: kernel/term.cmi proofs/tacmach.cmi \ kernel/sign.cmi proofs/proof_type.cmi kernel/names.cmi \ library/libnames.cmi kernel/closure.cmi @@ -1025,10 +1026,10 @@ library/nameops.cmo: lib/util.cmi lib/pp.cmi kernel/names.cmi \ library/nameops.cmx: lib/util.cmx lib/pp.cmx kernel/names.cmx \ library/nameops.cmi library/nametab.cmo: lib/util.cmi library/summary.cmi lib/pp.cmi \ - kernel/names.cmi library/nameops.cmi library/libnames.cmi \ + lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \ kernel/declarations.cmi library/nametab.cmi library/nametab.cmx: lib/util.cmx library/summary.cmx lib/pp.cmx \ - kernel/names.cmx library/nameops.cmx library/libnames.cmx \ + lib/options.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \ kernel/declarations.cmx library/nametab.cmi library/states.cmo: lib/system.cmi library/summary.cmi library/library.cmi \ library/lib.cmi library/states.cmi @@ -1046,10 +1047,10 @@ lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \ - interp/genarg.cmi + interp/genarg.cmi lib/compat.cmo parsing/argextend.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ parsing/q_util.cmx parsing/q_coqast.cmx parsing/pcoq.cmx \ - interp/genarg.cmx + interp/genarg.cmx lib/compat.cmx parsing/egrammar.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi proofs/tacexpr.cmo library/summary.cmi lib/pp.cmi \ parsing/pcoq.cmi interp/notation.cmi kernel/names.cmi library/nameops.cmi \ @@ -1076,10 +1077,10 @@ parsing/g_constr.cmo: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ parsing/g_constr.cmx: lib/util.cmx interp/topconstr.cmx kernel/term.cmx \ pretyping/rawterm.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ library/libnames.cmx parsing/lexer.cmx lib/bigint.cmx -parsing/g_decl_mode.cmo: interp/topconstr.cmi kernel/term.cmi \ +parsing/g_decl_mode.cmo: parsing/grammar.cma interp/topconstr.cmi kernel/term.cmi \ parsing/pcoq.cmi kernel/names.cmi library/libnames.cmi interp/genarg.cmi \ proofs/decl_expr.cmi -parsing/g_decl_mode.cmx: interp/topconstr.cmx kernel/term.cmx \ +parsing/g_decl_mode.cmx: parsing/grammar.cma interp/topconstr.cmx kernel/term.cmx \ parsing/pcoq.cmx kernel/names.cmx library/libnames.cmx interp/genarg.cmx \ proofs/decl_expr.cmi parsing/g_ltac.cmo: toplevel/vernacexpr.cmo lib/util.cmi interp/topconstr.cmi \ @@ -1136,14 +1137,14 @@ parsing/g_tactic.cmo: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \ parsing/g_tactic.cmx: lib/util.cmx interp/topconstr.cmx proofs/tacexpr.cmx \ pretyping/rawterm.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ parsing/lexer.cmx interp/genarg.cmx -parsing/g_vernac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ +parsing/g_vernac.cmo: parsing/grammar.cma toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \ interp/ppextend.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \ kernel/names.cmi library/nameops.cmi parsing/lexer.cmi \ library/goptions.cmi interp/genarg.cmi parsing/g_constr.cmo \ parsing/extend.cmi proofs/decl_mode.cmi library/decl_kinds.cmo \ toplevel/class.cmi -parsing/g_vernac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ +parsing/g_vernac.cmx: parsing/grammar.cma toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \ interp/ppextend.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \ kernel/names.cmx library/nameops.cmx parsing/lexer.cmx \ @@ -1173,11 +1174,11 @@ parsing/lexer.cmx: lib/util.cmx lib/pp.cmx lib/options.cmx parsing/lexer.cmi parsing/pcoq.cmo: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi interp/ppextend.cmi lib/pp.cmi lib/options.cmi \ kernel/names.cmi library/libnames.cmi parsing/lexer.cmi interp/genarg.cmi \ - parsing/extend.cmi library/decl_kinds.cmo parsing/pcoq.cmi + parsing/extend.cmi library/decl_kinds.cmo lib/compat.cmo parsing/pcoq.cmi parsing/pcoq.cmx: lib/util.cmx interp/topconstr.cmx proofs/tacexpr.cmx \ pretyping/rawterm.cmx interp/ppextend.cmx lib/pp.cmx lib/options.cmx \ kernel/names.cmx library/libnames.cmx parsing/lexer.cmx interp/genarg.cmx \ - parsing/extend.cmx library/decl_kinds.cmx parsing/pcoq.cmi + parsing/extend.cmx library/decl_kinds.cmx lib/compat.cmx parsing/pcoq.cmi parsing/ppconstr.cmo: lib/util.cmi kernel/univ.cmi interp/topconstr.cmi \ pretyping/termops.cmi kernel/term.cmi pretyping/rawterm.cmi \ interp/ppextend.cmi lib/pp.cmi pretyping/pattern.cmi lib/options.cmi \ @@ -1870,7 +1871,7 @@ tactics/dhyp.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/dhyp.cmi tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi -tactics/eauto.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ +tactics/eauto.cmo: parsing/grammar.cma lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo kernel/sign.cmi \ proofs/refiner.cmi kernel/reduction.cmi pretyping/rawterm.cmi \ @@ -1881,7 +1882,7 @@ tactics/eauto.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ parsing/egrammar.cmi kernel/declarations.cmi proofs/clenvtac.cmi \ pretyping/clenv.cmi toplevel/cerrors.cmi tactics/auto.cmi \ tactics/eauto.cmi -tactics/eauto.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ +tactics/eauto.cmx: parsing/grammar.cma lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx kernel/sign.cmx \ proofs/refiner.cmx kernel/reduction.cmx pretyping/rawterm.cmx \ @@ -1906,7 +1907,7 @@ tactics/elim.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ library/libnames.cmx pretyping/inductiveops.cmx tactics/hipattern.cmx \ tactics/hiddentac.cmx interp/genarg.cmx kernel/environ.cmx \ pretyping/clenv.cmx tactics/elim.cmi -tactics/eqdecide.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ +tactics/eqdecide.cmo: parsing/grammar.cma lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo proofs/refiner.cmi pretyping/rawterm.cmi \ proofs/proof_type.cmi proofs/proof_trees.cmi parsing/pptactic.cmi \ @@ -1916,7 +1917,7 @@ tactics/eqdecide.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/extratactics.cmi tactics/equality.cmi parsing/egrammar.cmi \ kernel/declarations.cmi interp/coqlib.cmi toplevel/cerrors.cmi \ tactics/auto.cmi -tactics/eqdecide.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ +tactics/eqdecide.cmx: parsing/grammar.cma lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx proofs/refiner.cmx pretyping/rawterm.cmx \ proofs/proof_type.cmx proofs/proof_trees.cmx parsing/pptactic.cmx \ @@ -1960,19 +1961,19 @@ tactics/evar_tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ proofs/refiner.cmx proofs/proof_type.cmx pretyping/evd.cmx \ pretyping/evarutil.cmx proofs/evar_refiner.cmx kernel/environ.cmx \ tactics/evar_tactics.cmi -tactics/extraargs.cmo: lib/util.cmi tactics/tacticals.cmi \ +tactics/extraargs.cmo: parsing/grammar.cma lib/util.cmi tactics/tacticals.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo tactics/setoid_replace.cmi \ parsing/printer.cmi parsing/pptactic.cmi interp/ppextend.cmi \ parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi \ library/nameops.cmi toplevel/metasyntax.cmi parsing/lexer.cmi \ interp/genarg.cmi tactics/extraargs.cmi -tactics/extraargs.cmx: lib/util.cmx tactics/tacticals.cmx \ +tactics/extraargs.cmx: parsing/grammar.cma lib/util.cmx tactics/tacticals.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx tactics/setoid_replace.cmx \ parsing/printer.cmx parsing/pptactic.cmx interp/ppextend.cmx \ parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ library/nameops.cmx toplevel/metasyntax.cmx parsing/lexer.cmx \ interp/genarg.cmx tactics/extraargs.cmi -tactics/extratactics.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ +tactics/extratactics.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi lib/util.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \ tactics/setoid_replace.cmi proofs/refiner.cmi tactics/refine.cmi \ @@ -1983,7 +1984,7 @@ tactics/extratactics.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/evd.cmi tactics/evar_tactics.cmi tactics/equality.cmi \ parsing/egrammar.cmi tactics/contradiction.cmi interp/constrintern.cmi \ toplevel/cerrors.cmi tactics/autorewrite.cmi tactics/extratactics.cmi -tactics/extratactics.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ +tactics/extratactics.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx lib/util.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx library/summary.cmx \ tactics/setoid_replace.cmx proofs/refiner.cmx tactics/refine.cmx \ @@ -2002,7 +2003,7 @@ tactics/hiddentac.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ proofs/tacmach.cmx proofs/tacexpr.cmx proofs/refiner.cmx \ proofs/redexpr.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ interp/genarg.cmx tactics/evar_tactics.cmx tactics/hiddentac.cmi -tactics/hipattern.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ +tactics/hipattern.cmo: parsing/grammar.cma parsing/q_constr.cmo lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi pretyping/reductionops.cmi \ pretyping/rawterm.cmi proofs/proof_trees.cmi lib/pp.cmi \ pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \ @@ -2010,7 +2011,7 @@ tactics/hipattern.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ kernel/declarations.cmi interp/coqlib.cmi pretyping/clenv.cmi \ tactics/hipattern.cmi -tactics/hipattern.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ +tactics/hipattern.cmx: parsing/grammar.cma parsing/q_constr.cmo lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tacticals.cmx proofs/tacmach.cmx pretyping/reductionops.cmx \ pretyping/rawterm.cmx proofs/proof_trees.cmx lib/pp.cmx \ pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \ @@ -2196,13 +2197,13 @@ tactics/tactics.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \ library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \ interp/coqlib.cmx interp/constrintern.cmx proofs/clenvtac.cmx \ pretyping/clenv.cmx tactics/tactics.cmi -tactics/tauto.cmo: lib/util.cmi interp/topconstr.cmi tactics/tactics.cmi \ +tactics/tauto.cmo: parsing/grammar.cma lib/util.cmi interp/topconstr.cmi tactics/tactics.cmi \ tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ proofs/refiner.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi \ library/libnames.cmi tactics/hipattern.cmi interp/genarg.cmi \ parsing/egrammar.cmi toplevel/cerrors.cmi -tactics/tauto.cmx: lib/util.cmx interp/topconstr.cmx tactics/tactics.cmx \ +tactics/tauto.cmx: parsing/grammar.cma lib/util.cmx interp/topconstr.cmx tactics/tactics.cmx \ tactics/tacticals.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ proofs/refiner.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ @@ -2344,16 +2345,16 @@ toplevel/metasyntax.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ parsing/pcoq.cmi lib/options.cmi interp/notation.cmi kernel/names.cmi \ library/libobject.cmi library/libnames.cmi library/lib.cmi \ parsing/lexer.cmi library/global.cmi parsing/extend.cmi \ - parsing/egrammar.cmi interp/constrintern.cmi pretyping/classops.cmi \ - lib/bigint.cmi toplevel/metasyntax.cmi + parsing/egrammar.cmi interp/constrintern.cmi lib/compat.cmo \ + pretyping/classops.cmi lib/bigint.cmi toplevel/metasyntax.cmi toplevel/metasyntax.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx tactics/tacinterp.cmx library/summary.cmx \ pretyping/rawterm.cmx parsing/pptactic.cmx interp/ppextend.cmx lib/pp.cmx \ parsing/pcoq.cmx lib/options.cmx interp/notation.cmx kernel/names.cmx \ library/libobject.cmx library/libnames.cmx library/lib.cmx \ parsing/lexer.cmx library/global.cmx parsing/extend.cmx \ - parsing/egrammar.cmx interp/constrintern.cmx pretyping/classops.cmx \ - lib/bigint.cmx toplevel/metasyntax.cmi + parsing/egrammar.cmx interp/constrintern.cmx lib/compat.cmx \ + pretyping/classops.cmx lib/bigint.cmx toplevel/metasyntax.cmi toplevel/minicoq.cmo: lib/util.cmi kernel/type_errors.cmi kernel/term.cmi \ kernel/sign.cmi kernel/safe_typing.cmi lib/pp.cmi kernel/names.cmi \ kernel/inductive.cmi parsing/g_minicoq.cmi toplevel/fhimsg.cmi \ @@ -2482,7 +2483,7 @@ toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \ lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \ parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi -toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ +toplevel/whelp.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \ interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \ proofs/pfedit.cmi parsing/pcoq.cmi lib/options.cmi library/nametab.cmi \ @@ -2491,7 +2492,7 @@ toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ parsing/egrammar.cmi library/dischargedhypsmap.cmi pretyping/detyping.cmi \ interp/constrintern.cmi toplevel/command.cmi toplevel/cerrors.cmi \ toplevel/whelp.cmi -toplevel/whelp.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ +toplevel/whelp.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/termops.cmx kernel/term.cmx proofs/tacmach.cmx lib/system.cmx \ interp/syntax_def.cmx proofs/refiner.cmx pretyping/rawterm.cmx lib/pp.cmx \ proofs/pfedit.cmx parsing/pcoq.cmx lib/options.cmx library/nametab.cmx \ @@ -2524,11 +2525,11 @@ contrib/cc/cctac.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ kernel/environ.cmx kernel/declarations.cmx interp/coqlib.cmx \ kernel/closure.cmx contrib/cc/ccproof.cmx contrib/cc/ccalgo.cmx \ contrib/cc/cctac.cmi -contrib/cc/g_congruence.cmo: lib/util.cmi tactics/tactics.cmi \ +contrib/cc/g_congruence.cmo: parsing/grammar.cma lib/util.cmi tactics/tactics.cmi \ tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi interp/genarg.cmi \ parsing/egrammar.cmi toplevel/cerrors.cmi contrib/cc/cctac.cmi -contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \ +contrib/cc/g_congruence.cmx: parsing/grammar.cma lib/util.cmx tactics/tactics.cmx \ tactics/tacticals.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx interp/genarg.cmx \ parsing/egrammar.cmx toplevel/cerrors.cmx contrib/cc/cctac.cmx @@ -2700,12 +2701,12 @@ contrib/dp/dp_zenon.cmo: lib/util.cmi contrib/dp/fol.cmi \ contrib/dp/dp_zenon.cmi contrib/dp/dp_zenon.cmx: lib/util.cmx contrib/dp/fol.cmi \ contrib/dp/dp_zenon.cmi -contrib/dp/g_dp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ +contrib/dp/g_dp.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi lib/util.cmi \ tactics/tactics.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ proofs/refiner.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \ interp/genarg.cmi parsing/egrammar.cmi contrib/dp/dp.cmi \ toplevel/cerrors.cmi -contrib/dp/g_dp.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ +contrib/dp/g_dp.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx lib/util.cmx \ tactics/tactics.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \ interp/genarg.cmx parsing/egrammar.cmx contrib/dp/dp.cmx \ @@ -2762,13 +2763,13 @@ contrib/extraction/extraction.cmx: lib/util.cmx kernel/typeops.cmx \ pretyping/inductiveops.cmx kernel/inductive.cmx pretyping/evd.cmx \ kernel/environ.cmx kernel/declarations.cmx \ contrib/extraction/extraction.cmi -contrib/extraction/g_extraction.cmo: toplevel/vernacinterp.cmi \ +contrib/extraction/g_extraction.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo lib/util.cmi tactics/tacinterp.cmi \ contrib/extraction/table.cmi parsing/pptactic.cmi lib/pp.cmi \ parsing/pcoq.cmi parsing/lexer.cmi interp/genarg.cmi \ contrib/extraction/extract_env.cmi parsing/egrammar.cmi \ toplevel/cerrors.cmi -contrib/extraction/g_extraction.cmx: toplevel/vernacinterp.cmx \ +contrib/extraction/g_extraction.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx \ toplevel/vernacexpr.cmx lib/util.cmx tactics/tacinterp.cmx \ contrib/extraction/table.cmx parsing/pptactic.cmx lib/pp.cmx \ parsing/pcoq.cmx parsing/lexer.cmx interp/genarg.cmx \ @@ -2824,17 +2825,19 @@ contrib/extraction/scheme.cmx: lib/util.cmx contrib/extraction/table.cmx \ contrib/extraction/scheme.cmi contrib/extraction/table.cmo: lib/util.cmi kernel/typeops.cmi kernel/term.cmi \ library/summary.cmi kernel/reduction.cmi parsing/printer.cmi lib/pp.cmi \ - lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ - contrib/extraction/miniml.cmi library/libobject.cmi library/libnames.cmi \ - library/lib.cmi library/goptions.cmi library/global.cmi \ - kernel/environ.cmi kernel/declarations.cmi contrib/extraction/table.cmi + library/nametab.cmi kernel/names.cmi library/nameops.cmi \ + contrib/extraction/miniml.cmi library/library.cmi library/libobject.cmi \ + library/libnames.cmi library/lib.cmi library/goptions.cmi \ + library/global.cmi kernel/environ.cmi kernel/declarations.cmi \ + contrib/extraction/table.cmi contrib/extraction/table.cmx: lib/util.cmx kernel/typeops.cmx kernel/term.cmx \ library/summary.cmx kernel/reduction.cmx parsing/printer.cmx lib/pp.cmx \ - lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ - contrib/extraction/miniml.cmi library/libobject.cmx library/libnames.cmx \ - library/lib.cmx library/goptions.cmx library/global.cmx \ - kernel/environ.cmx kernel/declarations.cmx contrib/extraction/table.cmi -contrib/field/field.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ + library/nametab.cmx kernel/names.cmx library/nameops.cmx \ + contrib/extraction/miniml.cmi library/library.cmx library/libobject.cmx \ + library/libnames.cmx library/lib.cmx library/goptions.cmx \ + library/global.cmx kernel/environ.cmx kernel/declarations.cmx \ + contrib/extraction/table.cmi +contrib/field/field.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ lib/util.cmi pretyping/typing.cmi interp/topconstr.cmi kernel/term.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo library/summary.cmi contrib/ring/ring.cmo \ @@ -2846,7 +2849,7 @@ contrib/field/field.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ interp/genarg.cmi parsing/extend.cmi pretyping/evd.cmi \ parsing/egrammar.cmi interp/coqlib.cmi interp/constrintern.cmi \ toplevel/cerrors.cmi -contrib/field/field.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ +contrib/field/field.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ lib/util.cmx pretyping/typing.cmx interp/topconstr.cmx kernel/term.cmx \ tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx library/summary.cmx contrib/ring/ring.cmx \ @@ -2870,7 +2873,7 @@ contrib/first-order/formula.cmx: lib/util.cmx pretyping/termops.cmx \ pretyping/inductiveops.cmx tactics/hipattern.cmx library/global.cmx \ kernel/declarations.cmx kernel/closure.cmx \ contrib/first-order/formula.cmi -contrib/first-order/g_ground.cmo: lib/util.cmi kernel/term.cmi \ +contrib/first-order/g_ground.cmo: parsing/grammar.cma lib/util.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo contrib/first-order/sequent.cmi proofs/refiner.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi \ @@ -2878,7 +2881,7 @@ contrib/first-order/g_ground.cmo: lib/util.cmi kernel/term.cmi \ interp/genarg.cmi contrib/first-order/formula.cmi parsing/egrammar.cmi \ tactics/decl_proof_instr.cmi toplevel/cerrors.cmi contrib/cc/cctac.cmi \ tactics/auto.cmi -contrib/first-order/g_ground.cmx: lib/util.cmx kernel/term.cmx \ +contrib/first-order/g_ground.cmx: parsing/grammar.cma lib/util.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx contrib/first-order/sequent.cmx proofs/refiner.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ @@ -2960,11 +2963,11 @@ contrib/fourier/fourierR.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ library/libnames.cmx contrib/fourier/fourier.cmx pretyping/evarutil.cmx \ tactics/equality.cmx interp/coqlib.cmx tactics/contradiction.cmx \ pretyping/clenv.cmx -contrib/fourier/g_fourier.cmo: lib/util.cmi tactics/tacinterp.cmi \ +contrib/fourier/g_fourier.cmo: parsing/grammar.cma lib/util.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo proofs/refiner.cmi parsing/pptactic.cmi lib/pp.cmi \ parsing/pcoq.cmi contrib/fourier/fourierR.cmo parsing/egrammar.cmi \ toplevel/cerrors.cmi -contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \ +contrib/fourier/g_fourier.cmx: parsing/grammar.cma lib/util.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \ parsing/pcoq.cmx contrib/fourier/fourierR.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx @@ -2972,9 +2975,9 @@ contrib/funind/functional_principles_proofs.cmo: lib/util.cmi \ pretyping/typing.cmi kernel/typeops.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ pretyping/tacred.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ - kernel/sign.cmi pretyping/reductionops.cmi contrib/recdef/recdef.cmo \ - pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ - lib/pp.cmi proofs/pfedit.cmi lib/options.cmi library/nametab.cmi \ + proofs/tacexpr.cmo kernel/sign.cmi pretyping/reductionops.cmi \ + contrib/recdef/recdef.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \ + parsing/printer.cmi lib/pp.cmi proofs/pfedit.cmi library/nametab.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ contrib/funind/indfun_common.cmi tactics/hiddentac.cmi library/global.cmi \ interp/genarg.cmi pretyping/evd.cmi tactics/equality.cmi \ @@ -2986,9 +2989,9 @@ contrib/funind/functional_principles_proofs.cmx: lib/util.cmx \ pretyping/typing.cmx kernel/typeops.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ pretyping/tacred.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ - kernel/sign.cmx pretyping/reductionops.cmx contrib/recdef/recdef.cmx \ - pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ - lib/pp.cmx proofs/pfedit.cmx lib/options.cmx library/nametab.cmx \ + proofs/tacexpr.cmx kernel/sign.cmx pretyping/reductionops.cmx \ + contrib/recdef/recdef.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ + parsing/printer.cmx lib/pp.cmx proofs/pfedit.cmx library/nametab.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \ interp/genarg.cmx pretyping/evd.cmx tactics/equality.cmx \ @@ -3044,7 +3047,7 @@ contrib/funind/indfun_common.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/entries.cmx library/declare.cmx kernel/declarations.cmx \ library/decl_kinds.cmx interp/coqlib.cmx kernel/closure.cmx \ contrib/funind/indfun_common.cmi -contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ +contrib/funind/indfun_main.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi lib/util.cmi \ interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \ @@ -3057,7 +3060,7 @@ contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ contrib/funind/functional_principles_types.cmi pretyping/evd.cmi \ parsing/egrammar.cmi interp/coqlib.cmi interp/constrintern.cmi \ toplevel/cerrors.cmi -contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ +contrib/funind/indfun_main.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx lib/util.cmx \ interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \ @@ -3180,7 +3183,7 @@ contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ pretyping/detyping.cmx kernel/declarations.cmx interp/coqlib.cmx \ interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx \ contrib/funind/rawterm_to_relation.cmi -contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ +contrib/funind/tacinv.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \ proofs/tacmach.cmi contrib/funind/tacinvutils.cmi tactics/tacinterp.cmi \ @@ -3192,7 +3195,7 @@ contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ tactics/equality.cmi kernel/environ.cmi kernel/entries.cmi \ parsing/egrammar.cmi library/declare.cmi library/decl_kinds.cmo \ interp/coqlib.cmi interp/constrintern.cmi toplevel/cerrors.cmi -contrib/funind/tacinv.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ +contrib/funind/tacinv.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/typing.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx pretyping/tacred.cmx \ proofs/tacmach.cmx contrib/funind/tacinvutils.cmx tactics/tacinterp.cmx \ @@ -3246,7 +3249,7 @@ contrib/interface/blast.cmx: toplevel/vernacinterp.cmx \ tactics/eauto.cmx library/declare.cmx kernel/declarations.cmx \ toplevel/command.cmx pretyping/clenv.cmx tactics/auto.cmx \ contrib/interface/blast.cmi -contrib/interface/centaur.cmo: contrib/interface/xlate.cmi \ +contrib/interface/centaur.cmo: parsing/grammar.cma contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo toplevel/vernacentries.cmi toplevel/vernac.cmi \ lib/util.cmi kernel/typeops.cmi contrib/interface/translate.cmi \ @@ -3266,7 +3269,7 @@ contrib/interface/centaur.cmo: contrib/interface/xlate.cmi \ contrib/interface/debug_tac.cmi interp/constrintern.cmi \ toplevel/command.cmi pretyping/classops.cmi toplevel/cerrors.cmi \ contrib/interface/blast.cmi contrib/interface/ascent.cmi -contrib/interface/centaur.cmx: contrib/interface/xlate.cmx \ +contrib/interface/centaur.cmx: parsing/grammar.cma contrib/interface/xlate.cmx \ contrib/interface/vtp.cmx toplevel/vernacinterp.cmx \ toplevel/vernacexpr.cmx toplevel/vernacentries.cmx toplevel/vernac.cmx \ lib/util.cmx kernel/typeops.cmx contrib/interface/translate.cmx \ @@ -3306,12 +3309,12 @@ contrib/interface/dad.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ library/libnames.cmx library/global.cmx interp/genarg.cmx \ pretyping/evd.cmx kernel/environ.cmx interp/constrintern.cmx \ interp/constrextern.cmx contrib/interface/dad.cmi -contrib/interface/debug_tac.cmo: lib/util.cmi tactics/tacticals.cmi \ +contrib/interface/debug_tac.cmo: parsing/grammar.cma lib/util.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printer.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi library/global.cmi \ interp/genarg.cmi toplevel/cerrors.cmi contrib/interface/debug_tac.cmi -contrib/interface/debug_tac.cmx: lib/util.cmx tactics/tacticals.cmx \ +contrib/interface/debug_tac.cmx: parsing/grammar.cma lib/util.cmx tactics/tacticals.cmx \ proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printer.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx library/global.cmx \ @@ -3448,7 +3451,7 @@ contrib/jprover/jlogic.cmo: contrib/jprover/opname.cmi \ contrib/jprover/jterm.cmi contrib/jprover/jlogic.cmi contrib/jprover/jlogic.cmx: contrib/jprover/opname.cmx \ contrib/jprover/jterm.cmx contrib/jprover/jlogic.cmi -contrib/jprover/jprover.cmo: lib/util.cmi pretyping/termops.cmi \ +contrib/jprover/jprover.cmo: parsing/grammar.cma lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ proofs/refiner.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ @@ -3458,7 +3461,7 @@ contrib/jprover/jprover.cmo: lib/util.cmi pretyping/termops.cmi \ contrib/jprover/jall.cmi tactics/hipattern.cmi tactics/hiddentac.cmi \ library/global.cmi interp/genarg.cmi pretyping/evarutil.cmi \ parsing/egrammar.cmi toplevel/cerrors.cmi -contrib/jprover/jprover.cmx: lib/util.cmx pretyping/termops.cmx \ +contrib/jprover/jprover.cmx: parsing/grammar.cma lib/util.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ proofs/refiner.cmx pretyping/reductionops.cmx kernel/reduction.cmx \ @@ -3498,30 +3501,64 @@ contrib/omega/coq_omega.cmx: lib/util.cmx pretyping/termops.cmx \ tactics/equality.cmx kernel/environ.cmx kernel/declarations.cmx \ interp/coqlib.cmx tactics/contradiction.cmx kernel/closure.cmx \ pretyping/clenv.cmx lib/bigint.cmx -contrib/omega/g_omega.cmo: lib/util.cmi tactics/tacinterp.cmi \ +contrib/omega/g_omega.cmo: parsing/grammar.cma lib/util.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo proofs/refiner.cmi parsing/pptactic.cmi lib/pp.cmi \ parsing/pcoq.cmi parsing/egrammar.cmi contrib/omega/coq_omega.cmo \ toplevel/cerrors.cmi -contrib/omega/g_omega.cmx: lib/util.cmx tactics/tacinterp.cmx \ +contrib/omega/g_omega.cmx: parsing/grammar.cma lib/util.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \ parsing/pcoq.cmx parsing/egrammar.cmx contrib/omega/coq_omega.cmx \ toplevel/cerrors.cmx contrib/omega/omega.cmo: lib/util.cmi kernel/names.cmi contrib/omega/omega.cmx: lib/util.cmx kernel/names.cmx -contrib/ring/g_quote.cmo: lib/util.cmi tactics/tacinterp.cmi \ +contrib/recdef/recdef.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi \ + toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \ + kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ + proofs/tactic_debug.cmi pretyping/tacred.cmi proofs/tacmach.cmi \ + tactics/tacinterp.cmi kernel/safe_typing.cmi pretyping/reductionops.cmi \ + pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ + pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \ + parsing/pcoq.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \ + library/nameops.cmi library/libnames.cmi library/lib.cmi \ + tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \ + pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \ + kernel/entries.cmi tactics/elim.cmi parsing/egrammar.cmi \ + tactics/eauto.cmi library/declare.cmi kernel/declarations.cmi \ + library/decl_kinds.cmo interp/coqlib.cmi interp/constrintern.cmi \ + toplevel/command.cmi kernel/closure.cmi toplevel/cerrors.cmi \ + tactics/auto.cmi +contrib/recdef/recdef.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx \ + toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ + kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ + proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ + tactics/tacinterp.cmx kernel/safe_typing.cmx pretyping/reductionops.cmx \ + pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ + pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \ + parsing/pcoq.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \ + library/nameops.cmx library/libnames.cmx library/lib.cmx \ + tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \ + pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \ + kernel/entries.cmx tactics/elim.cmx parsing/egrammar.cmx \ + tactics/eauto.cmx library/declare.cmx kernel/declarations.cmx \ + library/decl_kinds.cmx interp/coqlib.cmx interp/constrintern.cmx \ + toplevel/command.cmx kernel/closure.cmx toplevel/cerrors.cmx \ + tactics/auto.cmx +contrib/ring/g_quote.cmo: parsing/grammar.cma lib/util.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo contrib/ring/quote.cmo parsing/pptactic.cmi lib/pp.cmi \ parsing/pcoq.cmi interp/genarg.cmi parsing/egrammar.cmi \ toplevel/cerrors.cmi -contrib/ring/g_quote.cmx: lib/util.cmx tactics/tacinterp.cmx \ +contrib/ring/g_quote.cmx: parsing/grammar.cma lib/util.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx contrib/ring/quote.cmx parsing/pptactic.cmx lib/pp.cmx \ parsing/pcoq.cmx interp/genarg.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx -contrib/ring/g_ring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ +contrib/ring/g_ring.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi lib/util.cmi \ tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ contrib/ring/ring.cmo proofs/refiner.cmi contrib/ring/quote.cmo \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi interp/genarg.cmi \ parsing/egrammar.cmi toplevel/cerrors.cmi -contrib/ring/g_ring.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ +contrib/ring/g_ring.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx lib/util.cmx \ tactics/tacticals.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ contrib/ring/ring.cmx proofs/refiner.cmx contrib/ring/quote.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx interp/genarg.cmx \ @@ -3564,11 +3601,11 @@ contrib/romega/const_omega.cmo: lib/util.cmi kernel/term.cmi \ contrib/romega/const_omega.cmx: lib/util.cmx kernel/term.cmx \ library/nametab.cmx kernel/names.cmx library/libnames.cmx \ interp/coqlib.cmx lib/bigint.cmx -contrib/romega/g_romega.cmo: lib/util.cmi tactics/tacinterp.cmi \ +contrib/romega/g_romega.cmo: parsing/grammar.cma lib/util.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo contrib/romega/refl_omega.cmo proofs/refiner.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi parsing/egrammar.cmi \ toplevel/cerrors.cmi -contrib/romega/g_romega.cmx: lib/util.cmx tactics/tacinterp.cmx \ +contrib/romega/g_romega.cmx: parsing/grammar.cma lib/util.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx contrib/romega/refl_omega.cmx proofs/refiner.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx @@ -3582,11 +3619,11 @@ contrib/romega/refl_omega.cmx: lib/util.cmx kernel/term.cmx \ parsing/printer.cmx lib/pp.cmx contrib/omega/omega.cmx kernel/names.cmx \ proofs/logic.cmx interp/coqlib.cmx contrib/romega/const_omega.cmx \ lib/bigint.cmx -contrib/rtauto/g_rtauto.cmo: lib/util.cmi tactics/tacinterp.cmi \ +contrib/rtauto/g_rtauto.cmo: parsing/grammar.cma lib/util.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo contrib/rtauto/refl_tauto.cmi proofs/refiner.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi parsing/egrammar.cmi \ toplevel/cerrors.cmi -contrib/rtauto/g_rtauto.cmx: lib/util.cmx tactics/tacinterp.cmx \ +contrib/rtauto/g_rtauto.cmx: parsing/grammar.cma lib/util.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx contrib/rtauto/refl_tauto.cmx proofs/refiner.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx @@ -3608,7 +3645,7 @@ contrib/rtauto/refl_tauto.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/names.cmx library/goptions.cmx lib/explore.cmx pretyping/evd.cmx \ kernel/environ.cmx interp/coqlib.cmx kernel/closure.cmx \ contrib/rtauto/refl_tauto.cmi -contrib/setoid_ring/newring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ +contrib/setoid_ring/newring.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ @@ -3623,7 +3660,7 @@ contrib/setoid_ring/newring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ parsing/egrammar.cmi library/declare.cmi library/decl_kinds.cmo \ interp/coqlib.cmi interp/constrintern.cmi kernel/closure.cmi \ toplevel/cerrors.cmi -contrib/setoid_ring/newring.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ +contrib/setoid_ring/newring.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/typing.cmx interp/topconstr.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ @@ -3646,15 +3683,15 @@ contrib/subtac/eterm.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tacticals.cmx contrib/subtac/subtac_utils.cmx lib/pp.cmx \ lib/options.cmx kernel/names.cmx library/global.cmx pretyping/evd.cmx \ pretyping/evarutil.cmx kernel/environ.cmx contrib/subtac/eterm.cmi -contrib/subtac/g_eterm.cmo: lib/util.cmi proofs/tacmach.cmi \ +contrib/subtac/g_eterm.cmo: parsing/grammar.cma lib/util.cmi proofs/tacmach.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi contrib/subtac/eterm.cmi \ parsing/egrammar.cmi toplevel/cerrors.cmi -contrib/subtac/g_eterm.cmx: lib/util.cmx proofs/tacmach.cmx \ +contrib/subtac/g_eterm.cmx: parsing/grammar.cma lib/util.cmx proofs/tacmach.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx contrib/subtac/eterm.cmx \ parsing/egrammar.cmx toplevel/cerrors.cmx -contrib/subtac/g_subtac.cmo: toplevel/vernacinterp.cmi \ +contrib/subtac/g_subtac.cmo: parsing/grammar.cma toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo toplevel/vernacentries.cmi lib/util.cmi \ interp/topconstr.cmi kernel/term.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo contrib/subtac/subtac_obligations.cmi \ @@ -3662,7 +3699,7 @@ contrib/subtac/g_subtac.cmo: toplevel/vernacinterp.cmi \ lib/pp.cmi parsing/pcoq.cmi lib/options.cmi kernel/names.cmi \ library/nameops.cmi library/libnames.cmi interp/genarg.cmi \ parsing/egrammar.cmi toplevel/cerrors.cmi -contrib/subtac/g_subtac.cmx: toplevel/vernacinterp.cmx \ +contrib/subtac/g_subtac.cmx: parsing/grammar.cma toplevel/vernacinterp.cmx \ toplevel/vernacexpr.cmx toplevel/vernacentries.cmx lib/util.cmx \ interp/topconstr.cmx kernel/term.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx contrib/subtac/subtac_obligations.cmx \ @@ -3962,20 +3999,16 @@ contrib/xml/xmlcommand.cmx: contrib/xml/xml.cmx toplevel/vernac.cmx \ kernel/environ.cmx library/declare.cmx kernel/declarations.cmx \ library/decl_kinds.cmx config/coq_config.cmx contrib/xml/cic2acic.cmx \ contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx contrib/xml/xmlcommand.cmi -contrib/xml/xmlentries.cmo: contrib/xml/xmlcommand.cmi \ +contrib/xml/xmlentries.cmo: parsing/grammar.cma contrib/xml/xmlcommand.cmi \ toplevel/vernacinterp.cmi lib/util.cmi lib/pp.cmi parsing/pcoq.cmi \ parsing/lexer.cmi interp/genarg.cmi parsing/extend.cmi \ parsing/egrammar.cmi toplevel/cerrors.cmi -contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ +contrib/xml/xmlentries.cmx: parsing/grammar.cma contrib/xml/xmlcommand.cmx \ toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \ parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx \ parsing/egrammar.cmx toplevel/cerrors.cmx contrib/xml/xml.cmo: contrib/xml/xml.cmi contrib/xml/xml.cmx: contrib/xml/xml.cmi -doc/refman/euclid.cmo: doc/refman/euclid.cmi -doc/refman/euclid.cmx: doc/refman/euclid.cmi -doc/refman/heapsort.cmo: doc/refman/heapsort.cmi -doc/refman/heapsort.cmx: doc/refman/heapsort.cmi ide/utils/config_file.cmo: ide/utils/config_file.cmi ide/utils/config_file.cmx: ide/utils/config_file.cmi ide/utils/configwin_html_config.cmo: ide/utils/configwin_types.cmo \ @@ -4020,147 +4053,15 @@ tools/coqdoc/pretty.cmo: tools/coqdoc/output.cmi tools/coqdoc/index.cmi \ tools/coqdoc/cdglobals.cmo tools/coqdoc/pretty.cmi tools/coqdoc/pretty.cmx: tools/coqdoc/output.cmx tools/coqdoc/index.cmx \ tools/coqdoc/cdglobals.cmx tools/coqdoc/pretty.cmi -tactics/tauto.cmo: parsing/grammar.cma -tactics/tauto.cmx: parsing/grammar.cma -tactics/eqdecide.cmo: parsing/grammar.cma -tactics/eqdecide.cmx: parsing/grammar.cma -tactics/extraargs.cmo: parsing/grammar.cma -tactics/extraargs.cmx: parsing/grammar.cma -tactics/extratactics.cmo: parsing/grammar.cma -tactics/extratactics.cmx: parsing/grammar.cma -tactics/eauto.cmo: parsing/grammar.cma -tactics/eauto.cmx: parsing/grammar.cma -toplevel/whelp.cmo: parsing/grammar.cma -toplevel/whelp.cmx: parsing/grammar.cma -tactics/hipattern.cmo: parsing/grammar.cma parsing/q_constr.cmo -tactics/hipattern.cmx: parsing/grammar.cma parsing/q_constr.cmo -contrib/omega/g_omega.cmo: parsing/grammar.cma -contrib/omega/g_omega.cmx: parsing/grammar.cma -contrib/romega/g_romega.cmo: parsing/grammar.cma -contrib/romega/g_romega.cmx: parsing/grammar.cma -contrib/ring/g_quote.cmo: parsing/grammar.cma -contrib/ring/g_quote.cmx: parsing/grammar.cma -contrib/ring/g_ring.cmo: parsing/grammar.cma -contrib/ring/g_ring.cmx: parsing/grammar.cma -contrib/dp/g_dp.cmo: parsing/grammar.cma -contrib/dp/g_dp.cmx: parsing/grammar.cma -contrib/setoid_ring/newring.cmo: parsing/grammar.cma -contrib/setoid_ring/newring.cmx: parsing/grammar.cma -contrib/field/field.cmo: parsing/grammar.cma -contrib/field/field.cmx: parsing/grammar.cma -contrib/fourier/g_fourier.cmo: parsing/grammar.cma -contrib/fourier/g_fourier.cmx: parsing/grammar.cma -contrib/extraction/g_extraction.cmo: parsing/grammar.cma -contrib/extraction/g_extraction.cmx: parsing/grammar.cma -contrib/xml/xmlentries.cmo: parsing/grammar.cma -contrib/xml/xmlentries.cmx: parsing/grammar.cma -contrib/jprover/jprover.cmo: parsing/grammar.cma -contrib/jprover/jprover.cmx: parsing/grammar.cma -contrib/cc/g_congruence.cmo: parsing/grammar.cma -contrib/cc/g_congruence.cmx: parsing/grammar.cma -contrib/funind/tacinv.cmo: parsing/grammar.cma -contrib/funind/tacinv.cmx: parsing/grammar.cma -contrib/first-order/g_ground.cmo: parsing/grammar.cma -contrib/first-order/g_ground.cmx: parsing/grammar.cma -contrib/subtac/g_subtac.cmo: parsing/grammar.cma -contrib/subtac/g_subtac.cmx: parsing/grammar.cma -contrib/subtac/g_eterm.cmo: parsing/grammar.cma -contrib/subtac/g_eterm.cmx: parsing/grammar.cma -contrib/rtauto/g_rtauto.cmo: parsing/grammar.cma -contrib/rtauto/g_rtauto.cmx: parsing/grammar.cma -contrib/recdef/recdef.cmo: parsing/grammar.cma -contrib/recdef/recdef.cmx: parsing/grammar.cma -contrib/funind/indfun_main.cmo: parsing/grammar.cma -contrib/funind/indfun_main.cmx: parsing/grammar.cma -contrib/interface/debug_tac.cmo: parsing/grammar.cma -contrib/interface/debug_tac.cmx: parsing/grammar.cma -contrib/interface/centaur.cmo: parsing/grammar.cma -contrib/interface/centaur.cmx: parsing/grammar.cma -parsing/lexer.cmo: -parsing/lexer.cmx: -parsing/pcoq.cmo: -parsing/pcoq.cmx: -parsing/q_util.cmo: -parsing/q_util.cmx: -parsing/q_coqast.cmo: -parsing/q_coqast.cmx: -parsing/g_prim.cmo: -parsing/g_prim.cmx: -parsing/g_minicoq.cmo: -parsing/g_minicoq.cmx: -parsing/g_vernac.cmo: parsing/grammar.cma -parsing/g_vernac.cmx: parsing/grammar.cma -parsing/g_proofs.cmo: -parsing/g_proofs.cmx: -parsing/g_xml.cmo: -parsing/g_xml.cmx: -parsing/g_constr.cmo: -parsing/g_constr.cmx: -parsing/g_tactic.cmo: -parsing/g_tactic.cmx: -parsing/g_ltac.cmo: -parsing/g_ltac.cmx: -parsing/argextend.cmo: -parsing/argextend.cmx: -parsing/tacextend.cmo: -parsing/tacextend.cmx: -parsing/vernacextend.cmo: -parsing/vernacextend.cmx: -parsing/q_constr.cmo: -parsing/q_constr.cmx: -parsing/g_decl_mode.cmo: parsing/grammar.cma -parsing/g_decl_mode.cmx: parsing/grammar.cma -toplevel/mltop.cmo: -toplevel/mltop.cmx: -lib/pp.cmo: -lib/pp.cmx: -lib/compat.cmo: -lib/compat.cmx: -contrib/xml/xml.cmo: -contrib/xml/xml.cmx: -contrib/xml/acic2Xml.cmo: -contrib/xml/acic2Xml.cmx: -contrib/xml/proofTree2Xml.cmo: -contrib/xml/proofTree2Xml.cmx: -contrib/interface/line_parser.cmo: -contrib/interface/line_parser.cmx: -tools/coq_makefile.cmo: -tools/coq_makefile.cmx: -tools/coq-tex.cmo: -tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_memory.h kernel/byterun/coq_values.h \ kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_interp.h + kernel/byterun/coq_memory.h kernel/byterun/coq_interp.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /usr/local/lib/ocaml/caml/alloc.h + kernel/byterun/coq_values.h |