From 2281410e38ef99d025ea77194585a9bc019fdaa9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 3 Jan 2008 16:26:12 +0000 Subject: Imported Upstream version 8.1.pl3+dfsg --- .depend | 351 +++++++++---------------- CHANGES | 7 + Makefile | 20 +- PROBLEMES | 54 ---- TODO | 51 ---- configure | 6 +- contrib/funind/functional_principles_proofs.ml | 282 +++++++++++++------- contrib/funind/invfun.ml | 4 +- contrib/recdef/recdef.ml4 | 11 +- ide/coqide.ml | 14 +- kernel/indtypes.ml | 10 +- kernel/safe_typing.ml | 48 +++- library/lib.ml | 50 ++-- library/nametab.ml | 12 +- pretyping/evarutil.ml | 79 +++--- scripts/coqc.ml | 7 +- tools/coqdoc/output.ml | 17 +- tools/coqdoc/pretty.mll | 35 ++- 18 files changed, 508 insertions(+), 550 deletions(-) delete mode 100644 PROBLEMES delete mode 100644 TODO diff --git a/.depend b/.depend index f8aa692c..c6205347 100644 --- a/.depend +++ b/.depend @@ -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 diff --git a/CHANGES b/CHANGES index d1f6efe1..9967fad5 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,10 @@ +Changes from V8.1pl2 to V8.1pl3 +=============================== + +Bug fixes + +- A critical bug and a few other bugs have been fixed. + Changes from V8.1pl1 to V8.1pl2 =============================== diff --git a/Makefile b/Makefile index b27acbb4..b43a0942 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 10216 2007-10-11 13:44:00Z notin $ +# $Id: Makefile 10314 2007-11-12 15:10:25Z notin $ # Makefile for Coq @@ -1161,7 +1161,7 @@ COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo $(COQDEP): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) BEFOREDEPEND+= tools/coqdep_lexer.ml @@ -1169,23 +1169,23 @@ GALLINACMO=tools/gallina_lexer.cmo tools/gallina.cmo $(GALLINA): $(GALLINACMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO) BEFOREDEPEND+= tools/gallina_lexer.ml $(COQMAKEFILE): tools/coq_makefile.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coq_makefile.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coq_makefile.cmo $(COQTEX): tools/coq-tex.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.cmo BEFOREDEPEND+= tools/coqwc.ml $(COQWC): tools/coqwc.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo BEFOREDEPEND+= tools/coqdoc/pretty.ml tools/coqdoc/index.ml @@ -1195,7 +1195,7 @@ COQDOCCMO=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \ $(COQDOC): $(COQDOCCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO) clean:: rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml @@ -1264,6 +1264,8 @@ install-tools:: LIBFILES=$(THEORIESVO) $(CONTRIBVO) LIBFILESLIGHT=$(THEORIESLIGHTVO) + +GRAMMARCMA=parsing/grammar.cma OBJECTCMA=lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ @@ -1280,7 +1282,7 @@ install-library: $(MKDIR) $(FULLCOQLIB)/states cp states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib - cp $(OBJECTCMA) $(OBJECTCMXA) $(FULLCOQLIB) + cp $(OBJECTCMA) $(OBJECTCMXA) $(GRAMMARCMA) $(FULLCOQLIB) install-library-light: $(MKDIR) $(FULLCOQLIB) @@ -1758,7 +1760,7 @@ depend: dependp4 ml4filesml $(BEFOREDEPEND) for f in $(ML4FILES); do \ bn=`dirname $$f`/`basename $$f .ml4`; \ deps=`$(CAMLP4DEPS) $$f`; \ - if [[ $${deps} != "" ]]; then \ + if [ -n "$${deps}" ]; then \ /bin/mv -f .depend .depend.tmp; \ sed -e "\|^$${bn}.cmo|s|^$${bn}.cmo: \(.*\)$$|$${bn}.cmo: $${deps} \1|" \ -e "\|^$${bn}.cmx|s|^$${bn}.cmx: \(.*\)$$|$${bn}.cmx: $${deps} \1|" \ diff --git a/PROBLEMES b/PROBLEMES deleted file mode 100644 index 4e522a8a..00000000 --- a/PROBLEMES +++ /dev/null @@ -1,54 +0,0 @@ -Intuition plante en 7.1 à certains endroits où il réussissait en 6.3. -Y a-t-il une explication ? (cf contrib sheaves de Chicli - HH) - ----------------------------------------------------------------------- -Theorem toto : (A:Prop)A->A. -Refine [A;x]?. -produit le message "type_of: this is not a well-typed term. Please report." - ----------------------------------------------------------------------- -"Intro until 1" plante avec le message -"Error: Internal tactic intro cannot be applied to intro until #GENTERM 1" ---> intro est répété + GENTERM - ----------------------------------------------------------------------- -La synthèse du ? dans l'exemple suivant se fait en V6 mais pas en V7: - -Inductive Prod : Type := Pair : Set->Set->Prod. -Definition Pfst := [p:Prod](let (x, _) = p in x). -Variable P : Prod->Type. -Variable i : Set->(P (Pair nat nat)). -Variable j : (X:Prod)(Pfst X)->(P X)->Prop. -Variable k : nat. -Variable l : (P (Pair nat nat)). -Check (!j ? k (i nat)). (* Marche en V6, pas en V7 *) -Check (!j ? k l). (* Ne marche ni en V6 !!! ni en V7 *) - ----------------------------------------------------------------------- -Des CASTEDCOMMAND s'affiche dans les scripts de preuves. - ----------------------------------------------------------------------- -Probleme d'affichage des scripts de preuve (disparition des THEN) -Compute affiche Cbv Beta Iota - ----------------------------------------------------------------------- -Variable + Record => clash. Exemple: - -Section S. -Variable F:Set. -Record R [ F:Set; x:F ] : Set := { c : x=x }. - => Error: new_isevar_sign: two vars have the same name - ----------------------------------------------------------------------- -Declaration de Local a l'interieur d'un but ... - ----------------------------------------------------------------------- -Certains Clear deviennent impossible car la variable apparait dans -un lemme local, c'est plutot sain ... - ----------------------------------------------------------------------- -l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les -binding je pense) d'ou des erreurs de syntaxe ... pure_numarg est -plus sûr -REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la -syntaxe, elle est incompatible avec L_tac. diff --git a/TODO b/TODO deleted file mode 100644 index dc80e4c3..00000000 --- a/TODO +++ /dev/null @@ -1,51 +0,0 @@ -Langage: - -Distribution: - -Environnement: - -- Porter SearchIsos - -Noyau: - -Tactic: - -- Que contradiction raisonne a isomorphisme pres de False - -Vernac: - -- Print / Print Proof en fait identiques ; Print ne devrait pas afficher - les constantes opaques (devrait afficher qqchose comme ) - -Theories: - -- Rendre transparent tous les theoremes prouvant {A}+{B} -- Faire demarrer PolyList.nth a` l'indice 0 - Renommer l'actuel nth en nth1 ?? - -Doc: - -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibilite V6) - -- Ajouter let dans les règles du CIC - -> FAIT, mais reste a documenter le let dans les inductifs - et les champs manifestes dans les Record -- revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) - -- Préciser la clarification syntaxique de IntroPattern -- preciser que Goal vient en dernier dans une clause pattern list et - qu'il doit apparaitre si il y a un "in" - -- Omega Time debranche mais Omega System et Omega Action remarchent ? -- Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter -- Documenter Dependent Rewrite et CutRewrite ? -- Ajouter les motifs sous-termes de ltac - -- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) diff --git a/configure b/configure index e964539a..2cfbf7c4 100755 --- a/configure +++ b/configure @@ -6,8 +6,8 @@ # ################################## -VERSION=8.1pl2 -DATE="Oct. 2007" +VERSION=8.1pl3 +DATE="Dec. 2007" # a local which command for sh which () { @@ -866,4 +866,4 @@ echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'." -# $Id: configure 10215 2007-10-11 13:13:51Z herbelin $ +# $Id: configure 10375 2007-12-13 15:02:01Z notin $ diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index dec7273b..975cf60b 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -46,10 +46,10 @@ let observe_tac_stream s tac g = let observe_tac s tac g = observe_tac_stream (str s) tac g -let tclTRYD tac = - if !Options.debug || do_observe () - then (fun g -> try (* do_observe_tac "" *)tac g with _ -> tclIDTAC g) - else tac +(* let tclTRYD tac = *) +(* if !Options.debug || do_observe () *) +(* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *) +(* else tac *) let list_chop ?(msg="") n l = @@ -136,11 +136,11 @@ let change_hyp_with_using msg hyp_id t tac : tactic = fun g -> let prov_id = pf_get_new_id hyp_id g in tclTHENS - (observe_tac msg (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t)) + ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t)) [tclTHENLIST [ - observe_tac "change_hyp_with_using thin" (thin [hyp_id]); - observe_tac "change_hyp_with_using rename " (h_rename prov_id hyp_id) + (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); + (* observe_tac "change_hyp_with_using rename " *) (h_rename prov_id hyp_id) ]] g exception TOREMOVE @@ -179,7 +179,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = let nochange msg = begin - observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); +(* observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); *) failwith "NoChange"; end in @@ -195,7 +195,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = in if not (closed0 t1) then nochange "not a closed lhs"; let rec compute_substitution sub t1 t2 = - observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); +(* observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *) if isRel t2 then let t2 = destRel t2 in @@ -386,11 +386,12 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = List.rev_map mkVar (rec_pte_id::context_hyps_ids) ) in - observe_tac "rec hyp " +(* observe_tac "rec hyp " *) (tclTHENS (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x) - [observe_tac "prove rec hyp" (prove_rec_hyp eq_hyps); - observe_tac "prove rec hyp" + [ + (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); +(* observe_tac "prove rec hyp" *) (refine to_refine) ]) g @@ -399,7 +400,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = in tclTHENLIST [ - observe_tac "hyp rec" +(* observe_tac "hyp rec" *) (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp); scan_type context popped_t' ] @@ -440,7 +441,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = in tclTHENLIST[ change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp - (observe_tac "prove_trivial" prove_trivial); + ((* observe_tac "prove_trivial" *) prove_trivial); scan_type context popped_t' ] else if is_trivial_eq t_x @@ -456,7 +457,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = "prove_trivial_eq" hyp_id real_type_of_hyp - (observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1)))); + ((* observe_tac "prove_trivial_eq" *) (prove_trivial_eq hyp_id context (args.(0),args.(1)))); scan_type context popped_t' ] else @@ -505,7 +506,7 @@ let clean_goal_with_heq ptes_infos continue_tac dyn_infos = tclTHENLIST [ tac ; - observe_tac "clean_hyp_with_heq continue" (continue_tac new_infos) + (* observe_tac "clean_hyp_with_heq continue" *) (continue_tac new_infos) ] g @@ -523,7 +524,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = introduction_no_check heq_id; (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; - observe_tac "after_introduction" (fun g' -> + (* observe_tac "after_introduction" *)(fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_type_of g' (mkVar heq_id) in (* compute the new value of the body *) @@ -572,7 +573,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id tclTHENLIST[ forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); thin [hid]; - h_rename prov_hid hid + (h_rename prov_hid hid) ] g ) ( (* @@ -619,9 +620,9 @@ let build_proof : tactic = let rec build_proof_aux do_finalize dyn_infos : tactic = fun g -> - (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) - match kind_of_term dyn_infos.info with | Case(ci,ct,t,cb) -> + match kind_of_term dyn_infos.info with + | Case(ci,ct,t,cb) -> let do_finalize_t dyn_info' = fun g -> let t = dyn_info'.info in @@ -674,7 +675,7 @@ let build_proof nb_rec_hyps = List.length new_hyps } in - observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' +(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' (* build_proof do_finalize new_infos g' *) ) g | _ -> @@ -757,7 +758,7 @@ let build_proof | Rel _ -> anomaly "Free var in goal conclusion !" and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - (build_proof_aux do_finalize dyn_infos) g + observe_tac "build_proof" (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -783,14 +784,14 @@ let build_proof {dyn_infos with info = arg } g in - observe_tac "build_proof_args" (tac ) g + (* observe_tac "build_proof_args" *) (tac ) g in let do_finish_proof dyn_infos = (* tclTRYD *) (clean_goal_with_heq ptes_infos finish_proof dyn_infos) in - observe_tac "build_proof" + (* observe_tac "build_proof" *) (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) @@ -863,8 +864,8 @@ let generalize_non_dep hyp g = in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN - (observe_tac "h_generalize" (h_generalize (List.map mkVar to_revert) )) - (observe_tac "thin" (thin to_revert)) + ((* observe_tac "h_generalize" *) (h_generalize (List.map mkVar to_revert) )) + ((* observe_tac "thin" *) (thin to_revert)) g let id_of_decl (na,_,_) = (Nameops.out_name na) @@ -905,11 +906,11 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = tclTHENSEQ [ tclDO (nb_params + rec_args_num + 1) intro; - observe_tac "" (fun g -> + (* observe_tac "" *) (fun g -> let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ - [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id); - observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings)); + [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); + (* observe_tac "h_case" *) (h_case (mkVar rec_id,Rawterm.NoBindings)); intros_reflexivity] g ) ] @@ -1138,7 +1139,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in if other_fix_infos = [] then - observe_tac ("h_fix") (h_fix (Some this_fix_info.name) (this_fix_info.idx +1)) + (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1)) else h_mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos @@ -1146,10 +1147,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let first_tac : tactic = (* every operations until fix creations *) tclTHENSEQ - [ observe_tac "introducing params" (intros_using (List.rev_map id_of_decl princ_info.params)); - observe_tac "introducing predictes" (intros_using (List.rev_map id_of_decl princ_info.predicates)); - observe_tac "introducing branches" (intros_using (List.rev_map id_of_decl princ_info.branches)); - observe_tac "building fixes" mk_fixes; + [ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params)); + (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates)); + (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches)); + (* observe_tac "building fixes" *) mk_fixes; ] in let intros_after_fixes : tactic = @@ -1162,7 +1163,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let nb_args = fix_info.nb_realargs in tclTHENSEQ [ - observe_tac ("introducing args") (tclDO nb_args intro); + (* observe_tac ("introducing args") *) (tclDO nb_args intro); (fun g -> (* replacement of the function by its body *) let args = nLastHyps nb_args g in let fix_body = fix_info.body_with_param in @@ -1180,7 +1181,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in tclTHENSEQ [ - observe_tac "do_replace" +(* observe_tac "do_replace" *) (do_replace full_params (fix_info.idx + List.length princ_params) @@ -1205,7 +1206,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : nb_rec_hyps = List.length branches } in - observe_tac "cleaning" (clean_goal_with_heq + (* observe_tac "cleaning" *) (clean_goal_with_heq (Idmap.map prove_rec_hyp ptes_to_fix) do_prove dyn_infos) @@ -1215,7 +1216,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) (* ); *) - observe_tac "instancing" (instanciate_hyps_with_args prove_tac + (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id)) ] @@ -1295,18 +1296,28 @@ and h_intros = Recdef.h_intros and list_rewrite = Recdef.list_rewrite and evaluable_of_global_reference = Recdef.evaluable_of_global_reference + + + + let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with | None -> anomaly "No tcc proof !!" | Some lemma -> fun gls -> - let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in +(* let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in *) +(* let ids = hid::pf_ids_of_hyps gls in *) tclTHENSEQ [ - generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); +(* generalize [lemma]; *) +(* h_intro hid; *) +(* Elim.h_decompose_and (mkVar hid); *) tclTRY(list_rewrite true eqs); +(* (fun g -> *) +(* let ids' = pf_ids_of_hyps g in *) +(* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) +(* rewrite *) +(* ) *) Eauto.gen_eauto false (false,5) [] (Some []) ] gls @@ -1314,6 +1325,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> + let eqs = List.map mkVar eqs in let rewrite = tclFIRST (List.map Equality.rewriteRL eqs ) in @@ -1331,42 +1343,60 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = - +let build_clause eqs = + { + Tacexpr.onhyps = + Some (List.map + (fun id -> ([],id),Tacexpr.InHyp) + eqs + ); + Tacexpr.onconcl = false; + Tacexpr.concl_occs = [] + } -let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic = - match !tcc_lemma_constr with - | None -> tclIDTAC_MESSAGE (str "No tcc proof !!") - | Some lemma -> - fun gls -> - let hid = next_global_ident_away true Recdef.h_id (pf_ids_of_hyps gls) in - (tclTHENSEQ - [ - generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); - backtrack_eqs_until_hrec hrec eqs; - observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) - (tclTHENS (* We must have exactly ONE subgoal !*) - (apply (mkVar hrec)) - [ tclTHENSEQ - [ - thin [hrec]; - apply (Lazy.force acc_inv); - (fun g -> - if is_mes - then - unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g - else tclIDTAC g - ); - observe_tac "rew_and_finish" - (tclTHEN - (tclTRY(Recdef.list_rewrite true eqs)) - (observe_tac "finishing" (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some []))))) +let rec rewrite_eqs_in_eqs eqs = + match eqs with + | [] -> tclIDTAC + | eq::eqs -> + tclTHEN + (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq))) eqs) + (rewrite_eqs_in_eqs eqs) + +let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = + fun gls -> + (tclTHENSEQ + [ + backtrack_eqs_until_hrec hrec eqs; + (* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *) + (tclTHENS (* We must have exactly ONE subgoal !*) + (apply (mkVar hrec)) + [ tclTHENSEQ + [ + keep (tcc_hyps@eqs); + + apply (Lazy.force acc_inv); + (fun g -> + if is_mes + then + unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g + else tclIDTAC g + ); + observe_tac "rew_and_finish" + (tclTHENLIST + [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs)); + rewrite_eqs_in_eqs eqs; + (observe_tac "finishing" + (tclCOMPLETE ( + Eauto.gen_eauto false (false,5) [] (Some [])) + ) + ) ] - ]) + ) + ] ]) - gls - + ]) + gls + let is_valid_hypothesis predicates_name = let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in @@ -1420,13 +1450,14 @@ let prove_principle_for_gen in let real_rec_arg_num = rec_arg_num - princ_info.nparams in let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in - observe ( - str "princ_type := " ++ pr_lconstr princ_type ++ fnl () ++ - str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ - str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ - str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ - str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ - str "npost_rec_arg := " ++ int npost_rec_arg ); +(* observe ( *) +(* str "princ_type := " ++ pr_lconstr princ_type ++ fnl () ++ *) +(* str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ *) + +(* str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ *) +(* str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ *) +(* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *) +(* str "npost_rec_arg := " ++ int npost_rec_arg ); *) let (post_rec_arg,pre_rec_arg) = Util.list_chop npost_rec_arg princ_info.args in @@ -1435,7 +1466,7 @@ let prove_principle_for_gen | (Name id,_,_)::_ -> id | _ -> assert false in - observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); +(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in @@ -1448,19 +1479,17 @@ let prove_principle_for_gen in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = - (observe_tac "prove_rec_arg_acc" + ((* observe_tac "prove_rec_arg_acc" *) (tclCOMPLETE (tclTHEN (forward - (Some ((fun g -> observe_tac "prove wf" (tclCOMPLETE (wf_tac is_mes)) g))) + (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))) (Genarg.IntroIdentifier wf_thm_id) (mkApp (delayed_force well_founded,[|input_type;relation|]))) ( - observe_tac - "apply wf_thm" - (h_apply ((mkApp(mkVar wf_thm_id, - [|mkVar rec_arg_id |])),Rawterm.NoBindings) - ) + (* observe_tac *) +(* "apply wf_thm" *) + h_simplest_apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])) ) ) ) @@ -1468,22 +1497,68 @@ let prove_principle_for_gen g in let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in + let lemma = + match !tcc_lemma_ref with + | None -> anomaly ( "No tcc proof !!") + | Some lemma -> lemma + in + let rec list_diff del_list check_list = + match del_list with + [] -> + [] + | f::r -> + if List.mem f check_list then + list_diff r check_list + else + f::(list_diff r check_list) + in + let tcc_list = ref [] in + let start_tac gls = + let hyps = pf_ids_of_hyps gls in + let hid = + next_global_ident_away true + (id_of_string "prov") + hyps + in + tclTHENSEQ + [ + generalize [lemma]; + h_intro hid; + Elim.h_decompose_and (mkVar hid); + (fun g -> + let new_hyps = pf_ids_of_hyps g in + tcc_list := list_diff new_hyps (hid::hyps); + if !tcc_list = [] + then + begin + tcc_list := [hid]; + tclIDTAC g + end + else thin [hid] g + ) + ] + gls + in tclTHENSEQ - [ + [ + observe_tac "start_tac" start_tac; h_intros (List.rev_map (fun (na,_,_) -> Nameops.out_name na) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); - observe_tac "" (forward + (* observe_tac "" *) (forward (Some (prove_rec_arg_acc)) (Genarg.IntroIdentifier acc_rec_arg_id) (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) ); - observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids))); - observe_tac "h_fix" (h_fix (Some fix_id) (List.length args_ids + 1)); +(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); +(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) +(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) + (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1)); +(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Equality.rewriteLR (mkConst eq_ref); - observe_tac "finish" (fun gl' -> + (* observe_tac "finish" *) (fun gl' -> let body = let _,args = destApp (pf_concl gl') in array_last args @@ -1511,9 +1586,20 @@ let prove_principle_for_gen let pte_info = { proving_tac = (fun eqs -> - observe_tac "new_prove_with_tcc" +(* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *) +(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *) +(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *) +(* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *) +(* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) + + (* observe_tac "new_prove_with_tcc" *) (new_prove_with_tcc - is_mes acc_inv fix_id tcc_lemma_ref (List.map mkVar eqs) + is_mes acc_inv fix_id + !tcc_list + ((List.map + (fun (na,_,_) -> (Nameops.out_name na)) + (princ_info.args@princ_info.params) + )@ (acc_rec_arg_id::eqs)) ) ); is_valid = is_valid_hypothesis predicates_names @@ -1536,7 +1622,7 @@ let prove_principle_for_gen ptes_info (body_info rec_hyps) in - observe_tac "instanciate_hyps_with_args" + (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches) diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 9ec02d4c..c7a3d164 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -569,14 +569,14 @@ let rec reflexivity_with_destruct_cases g = if Equality.discriminable (pf_env g) (project g) t1 t2 then Equality.discr id g else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHEN (Equality.inj [] id) intros_with_rewrite g + then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) in (tclFIRST [ reflexivity; - destruct_case (); + tclTHEN (tclPROGRESS discr_inject) (destruct_case ()); (* We reach this point ONLY if the same value is matched (at least) two times along binding path. diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index a4acd9a9..40832677 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -499,11 +499,12 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs (heq::cond_eqs)] g;; let string_match s = - try - for i = 0 to 3 do - if String.get s i <> String.get "Acc_" i then failwith "string_match" - done; - with Invalid_argument _ -> failwith "string_match" + if String.length s < 3 then failwith "string_match"; + try + for i = 0 to 3 do + if String.get s i <> String.get "Acc_" i then failwith "string_match" + done; + with Invalid_argument _ -> failwith "string_match" let retrieve_acc_var g = (* Julien: I don't like this version .... *) diff --git a/ide/coqide.ml b/ide/coqide.ml index fdc344e8..6cee46a6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 10220 2007-10-12 13:25:54Z notin $ *) +(* $Id: coqide.ml 10229 2007-10-16 18:44:54Z notin $ *) open Preferences open Vernacexpr @@ -2856,10 +2856,10 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); | None -> !flash_info "Active buffer has no name" | Some f -> - let s,res = run_command - av#insert_message - (!current.cmd_coqc ^ " " ^ (Filename.quote f)) - in + let cmd = !current.cmd_coqc ^ " -I " + ^ (Filename.quote (Filename.dirname f)) + ^ " " ^ (Filename.quote f) in + let s,res = run_command av#insert_message cmd in if s = Unix.WEXITED 0 then !flash_info (f ^ " successfully compiled") else begin @@ -2876,7 +2876,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Make Menu *) let make_f () = - let v = get_active_view () in + let v = get_current_view () in let av = out_some v.analyzed_view in match av#filename with | None -> @@ -2942,7 +2942,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/CoqMakefile Menu*) let coq_makefile_f () = - let v = get_active_view () in + let v = get_current_view () in let av = out_some v.analyzed_view in match av#filename with | None -> diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 4fe90ffd..a6fd6d04 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 9633 2007-02-09 18:40:26Z herbelin $ *) +(* $Id: indtypes.ml 10297 2007-11-07 11:05:53Z barras $ *) open Util open Names @@ -29,6 +29,9 @@ let weaker_noccur_between env x nvars t = if noccur_between x nvars t' then Some t' else None +let is_constructor_head t = + isRel(fst(decompose_app t)) + (************************************************************************) (* Various well-formedness check for inductive declarations *) @@ -116,6 +119,7 @@ let is_unit constrsinfos = | _ -> false let rec infos_and_sort env t = + let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (name,c1,c2) -> let (varj,_) = infer_type env c1 in @@ -123,8 +127,8 @@ let rec infos_and_sort env t = let logic = is_logic_type varj in let small = Term.is_small varj.utj_type in (logic,small) :: (infos_and_sort env1 c2) - | Cast (c,_,_) -> infos_and_sort env c - | _ -> [] + | _ when is_constructor_head t -> [] + | _ -> anomaly "infos_and_sort: not a positive constructor" let small_unit constrsinfos = let issmall = List.for_all is_small constrsinfos diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c4d9c991..5f01613c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *) +(* $Id: safe_typing.ml 10276 2007-10-30 11:37:54Z barras $ *) open Util open Names @@ -42,6 +42,11 @@ type module_info = let check_label l labset = if Labset.mem l labset then error_existing_label l +let set_engagement_opt oeng env = + match oeng with + Some eng -> set_engagement eng env + | _ -> env + type library_info = dir_path * Digest.t type safe_environment = @@ -51,6 +56,8 @@ type safe_environment = labset : Labset.t; revsign : module_signature_body; revstruct : module_structure_body; + univ : Univ.constraints; + engagement : engagement option; imports : library_info list; loads : (module_path * module_body) list } @@ -78,6 +85,8 @@ let rec empty_environment = labset = Labset.empty; revsign = []; revstruct = []; + univ = Univ.Constraint.empty; + engagement = None; imports = []; loads = [] } @@ -153,6 +162,8 @@ let add_constant dir l decl senv = labset = Labset.add l senv.labset; revsign = (l,SPBconst cb)::senv.revsign; revstruct = (l,SEBconst cb)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; imports = senv.imports; loads = senv.loads } @@ -180,6 +191,8 @@ let add_mind dir l mie senv = labset = Labset.add l senv.labset; (* TODO: the same as above *) revsign = (l,SPBmind mib)::senv.revsign; revstruct = (l,SEBmind mib)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; imports = senv.imports; loads = senv.loads } @@ -198,6 +211,8 @@ let add_modtype l mte senv = labset = Labset.add l senv.labset; revsign = (l,SPBmodtype mtb)::senv.revsign; revstruct = (l,SEBmodtype mtb)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; imports = senv.imports; loads = senv.loads } @@ -223,6 +238,8 @@ let add_module l me senv = labset = Labset.add l senv.labset; revsign = (l,SPBmodule mspec)::senv.revsign; revstruct = (l,SEBmodule mb)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; imports = senv.imports; loads = senv.loads } @@ -245,6 +262,8 @@ let start_module l senv = labset = Labset.empty; revsign = []; revstruct = []; + univ = Univ.Constraint.empty; + engagement = None; imports = senv.imports; loads = [] } @@ -274,6 +293,7 @@ let end_module l restype senv = let mtb = functorize_type res_tb in mtb, Some mtb, cst in + let cst = Constraint.union cst senv.univ in let mexpr = List.fold_left (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb)) @@ -294,6 +314,7 @@ let end_module l restype senv = in let mp = MPdot (oldsenv.modinfo.modpath, l) in let newenv = oldsenv.env in + let newenv = set_engagement_opt senv.engagement newenv in let newenv = List.fold_left (fun env (mp,mb) -> full_add_module mp mb env) @@ -309,6 +330,9 @@ let end_module l restype senv = labset = Labset.add l oldsenv.labset; revsign = (l,SPBmodule mspec)::oldsenv.revsign; revstruct = (l,SEBmodule mb)::oldsenv.revstruct; + univ = oldsenv.univ; + (* engagement is propagated to the upper level *) + engagement = senv.engagement; imports = senv.imports; loads = senv.loads@oldsenv.loads } @@ -333,6 +357,8 @@ let add_module_parameter mbid mte senv = labset = senv.labset; revsign = []; revstruct = []; + univ = senv.univ; + engagement = senv.engagement; imports = senv.imports; loads = [] } @@ -355,6 +381,8 @@ let start_modtype l senv = labset = Labset.empty; revsign = []; revstruct = []; + univ = Univ.Constraint.empty; + engagement = None; imports = senv.imports; loads = [] } @@ -377,6 +405,10 @@ let end_modtype l senv = in let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in let newenv = oldsenv.env in + (* since universes constraints cannot be stored in the modtype, + they are propagated to the upper level *) + let newenv = add_constraints senv.univ newenv in + let newenv = set_engagement_opt senv.engagement newenv in let newenv = List.fold_left (fun env (mp,mb) -> full_add_module mp mb env) @@ -395,6 +427,8 @@ let end_modtype l senv = labset = Labset.add l oldsenv.labset; revsign = (l,SPBmodtype mtb)::oldsenv.revsign; revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct; + univ = Univ.Constraint.union senv.univ oldsenv.univ; + engagement = senv.engagement; imports = senv.imports; loads = senv.loads@oldsenv.loads } @@ -404,7 +438,9 @@ let current_msid senv = senv.modinfo.msid let add_constraints cst senv = - {senv with env = Environ.add_constraints cst senv.env} + {senv with + env = Environ.add_constraints cst senv.env; + univ = Univ.Constraint.union cst senv.univ } (* Check that the engagement expected by a library matches the initial one *) let check_engagement env c = @@ -415,7 +451,9 @@ let check_engagement env c = error "Needs option -impredicative-set" let set_engagement c senv = - {senv with env = Environ.set_engagement c senv.env} + {senv with + env = Environ.set_engagement c senv.env; + engagement = Some c } (* Libraries = Compiled modules *) @@ -454,6 +492,8 @@ let start_library dir senv = labset = Labset.empty; revsign = []; revstruct = []; + univ = Univ.Constraint.empty; + engagement = None; imports = senv.imports; loads = [] } @@ -475,7 +515,7 @@ let export senv dir = mod_type = MTBsig (modinfo.msid, List.rev senv.revsign); mod_user_type = None; mod_equiv = None; - mod_constraints = Constraint.empty } + mod_constraints = senv.univ } in modinfo.msid, (dir,mb,senv.imports,engagement senv.env) diff --git a/library/lib.ml b/library/lib.ml index 213a1d19..4a4e90c1 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 9488 2007-01-17 11:11:58Z herbelin $ *) +(* $Id: lib.ml 10269 2007-10-29 11:09:43Z notin $ *) open Pp open Util @@ -237,14 +237,18 @@ let end_module id = let oname,nametab = try match find_entry_p is_something_opened with | oname,OpenedModule (_,_,nametab) -> - let sp = fst oname in - let id' = basename sp in - if id<>id' then error "this is not the last opened module"; - oname,nametab - | _,OpenedModtype _ -> - error "there are some open module types" - | _,OpenedSection _ -> - error "there are some open sections" + let id' = basename (fst oname) in + if id<>id' then + errorlabstrm "end_module" (str "last opened module is " ++ pr_id id'); + oname,nametab + | oname,OpenedModtype _ -> + let id' = basename (fst oname) in + errorlabstrm "end_module" + (str "module type " ++ pr_id id' ++ str " is still opened") + | oname,OpenedSection _ -> + let id' = basename (fst oname) in + errorlabstrm "end_module" + (str "section " ++ pr_id id' ++ str " is still opened") | _ -> assert false with Not_found -> error "no opened modules" @@ -271,14 +275,19 @@ let start_modtype id mp nametab = let end_modtype id = let sp,nametab = try match find_entry_p is_something_opened with - | sp,OpenedModtype (_,nametab) -> - let id' = basename (fst sp) in - if id<>id' then error "this is not the last opened module"; - sp,nametab - | _,OpenedModule _ -> - error "there are some open modules" - | _,OpenedSection _ -> - error "there are some open sections" + | oname,OpenedModtype (_,nametab) -> + let id' = basename (fst oname) in + if id<>id' then + errorlabstrm "end_modtype" (str "last opened module type is " ++ pr_id id'); + oname,nametab + | oname,OpenedModule _ -> + let id' = basename (fst oname) in + errorlabstrm "end_modtype" + (str "module " ++ pr_id id' ++ str " is still opened") + | oname,OpenedSection _ -> + let id' = basename (fst oname) in + errorlabstrm "end_modtype" + (str "section " ++ pr_id id' ++ str " is still opened") | _ -> assert false with Not_found -> error "no opened module types" @@ -487,9 +496,10 @@ let close_section id = let oname,fs = try match find_entry_p is_something_opened with | oname,OpenedSection (_,fs) -> - if id <> basename (fst oname) then - error "this is not the last opened section"; - (oname,fs) + let id' = basename (fst oname) in + if id <> id' then + errorlabstrm "close_section" (str "last opened section is " ++ pr_id id'); + (oname,fs) | _ -> assert false with Not_found -> error "no opened section" diff --git a/library/nametab.ml b/library/nametab.ml index 96280e8b..4e4e9b91 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nametab.ml 8642 2006-03-17 10:09:02Z notin $ *) +(* $Id: nametab.ml 10270 2007-10-29 14:48:33Z notin $ *) open Util open Pp @@ -107,8 +107,9 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + Options.if_verbose + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); current | Nothing | Relative _ -> Relative (uname,o) @@ -146,8 +147,9 @@ let rec push_exactly uname o level (current,dirmap) = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + Options.if_verbose + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); current | Nothing | Relative _ -> Relative (uname,o) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6896ca69..16059d94 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 9869 2007-05-29 11:07:04Z herbelin $ *) +(* $Id: evarutil.ml 10374 2007-12-13 13:16:52Z notin $ *) open Util open Pp @@ -331,7 +331,7 @@ let do_restrict_hyps env k evd ev args = exception Dependency_error of identifier -let rec check_and_clear_in_constr evd c ids = +let rec check_and_clear_in_constr evd c ids hist = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of evars *) @@ -347,45 +347,50 @@ let rec check_and_clear_in_constr evd c ids = | Var id' -> check id'; mkVar id' | Evar (e,l) -> - if Evd.is_defined_evar !evd (e,l) then - (* If e is already defined we replace it by its definition *) - let nc = nf_evar (evars_of !evd) c in - (check_and_clear_in_constr evd nc ids) + if (List.mem e hist) then + c else - (* We check for dependencies to elements of ids in the - evar_info corresponding to e and in the instance of - arguments. Concurrently, we build a new evar - corresponding to e where hypotheses of ids have been - removed *) - let evi = Evd.find (evars_of !evd) e in - let nconcl = check_and_clear_in_constr evd (evar_concl evi) ids in - let (nhyps,nargs) = - List.fold_right2 - (fun (id,ob,c) i (hy,ar) -> - if List.mem id ids then - (hy,ar) - else - let d' = (id, - (match ob with - None -> None - | Some b -> Some (check_and_clear_in_constr evd b ids)), - check_and_clear_in_constr evd c ids) in - let i' = check_and_clear_in_constr evd i ids in - (d'::hy, i'::ar) - ) - (evar_context evi) (Array.to_list l) ([],[]) in - let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in - let ev'= e_new_evar evd env ~src:(evar_source e !evd) nconcl in - evd := Evd.evar_define e ev' !evd; - let (e',_) = destEvar ev' in - mkEvar(e', Array.of_list nargs) - | _ -> map_constr (fun c -> check_and_clear_in_constr evd c ids) c + begin + if Evd.is_defined_evar !evd (e,l) then + (* If e is already defined we replace it by its definition *) + let nc = nf_evar (evars_of !evd) c in + (check_and_clear_in_constr evd nc ids hist) + else + (* We check for dependencies to elements of ids in the + evar_info corresponding to e and in the instance of + arguments. Concurrently, we build a new evar + corresponding to e where hypotheses of ids have been + removed *) + let evi = Evd.find (evars_of !evd) e in + let nconcl = check_and_clear_in_constr evd (evar_concl evi) ids (e::hist) in + let (nhyps,nargs) = + List.fold_right2 + (fun (id,ob,c) i (hy,ar) -> + if List.mem id ids then + (hy,ar) + else + let d' = (id, + (match ob with + None -> None + | Some b -> Some (check_and_clear_in_constr evd b ids (e::hist))), + check_and_clear_in_constr evd c ids (e::hist)) in + let i' = check_and_clear_in_constr evd i ids (e::hist) in + (d'::hy, i'::ar) + ) + (evar_context evi) (Array.to_list l) ([],[]) in + let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in + let ev'= e_new_evar evd env ~src:(evar_source e !evd) nconcl in + evd := Evd.evar_define e ev' !evd; + let (e',_) = destEvar ev' in + mkEvar(e', Array.of_list nargs) + end + | _ -> map_constr (fun c -> check_and_clear_in_constr evd c ids hist) c and clear_hyps_in_evi evd evi ids = (* clear_evar_hyps erases hypotheses ids in evi, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occuring in evi *) - let nconcl = try check_and_clear_in_constr evd (evar_concl evi) ids + let nconcl = try check_and_clear_in_constr evd (evar_concl evi) ids [] with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in let (nhyps,_) = let aux (id,ob,c) = @@ -393,8 +398,8 @@ and clear_hyps_in_evi evd evi ids = (id, (match ob with None -> None - | Some b -> Some (check_and_clear_in_constr evd b ids)), - check_and_clear_in_constr evd c ids) + | Some b -> Some (check_and_clear_in_constr evd b ids [])), + check_and_clear_in_constr evd c ids []) with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis " ^ string_of_id id) in diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 676e9e51..cbcb6b4c 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqc.ml 7747 2005-12-28 10:28:41Z herbelin $ *) +(* $Id: coqc.ml 10235 2007-10-18 12:25:03Z notin $ *) (* Afin de rendre Coq plus portable, ce programme Caml remplace le script coqc. @@ -161,7 +161,10 @@ let parse_args () = | ("-v"|"--version") :: _ -> Usage.version () | "-where" :: _ -> - print_endline Coq_config.coqlib; exit 0 + let coqlib = + try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib + in + print_endline coqlib; exit 0 | f :: rem -> if Sys.file_exists f then parse (f::cfiles,args) rem diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 28a0cd6d..2d0bc6c2 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 9976 2007-07-12 11:58:30Z msozeau $ i*) +(*i $Id: output.ml 10248 2007-10-23 13:02:56Z notin $ i*) open Cdglobals open Index @@ -41,8 +41,11 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Unset"; "Variable"; "Variables"; - "Notation"; + "Set"; "Unset"; "Variable"; "Variables"; + "Notation"; "Reserved Notation"; "Tactic Notation"; + "Delimit"; "Bind"; "Open"; "Scope"; + "Boxed"; "Unboxed"; + "Arguments"; (* Program *) "Program Definition"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; @@ -285,8 +288,8 @@ module Html = struct if !index && !current_module <> "Index" then printf "\n\n
\n
Index"; if !header_trailer then begin - printf "
This page has been generated by "; - printf "coqdoc\n" self; + printf "
This page has been generated by "; + printf "coqdoc\n" self; printf "
\n\n\n\n\n" end @@ -420,9 +423,9 @@ module Html = struct let r = sprintf "%s.html#%s" !current_module lab in add_toc_entry (Toc_section (lev, f, r)); stop_item (); - printf "" lab lev; + printf "" lab lev; f (); - printf "\n" lev + printf "\n" lev let rule () = printf "
\n" diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 2bf615d3..e16c7979 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 10074 2007-08-13 12:19:44Z notin $ i*) +(*i $Id: pretty.mll 10248 2007-10-23 13:02:56Z notin $ i*) (*s Utility functions for the scanners *) @@ -224,7 +224,7 @@ let decl_token = let gallina_ext = "Module" - | "Declare" + | "Declare" space+ "Module" | "Transparent" | "Opaque" | "Canonical" @@ -327,25 +327,24 @@ rule coq_bol = parse | space* gallina_kw_to_hide { let s = lexeme lexbuf in if !light && section_or_end s then begin - skip_to_dot lexbuf; - coq_bol lexbuf - end else begin - let s = lexeme lexbuf in - let nbsp = count_spaces s in - indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); - let eol= body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end } + skip_to_dot lexbuf; + coq_bol lexbuf + end else begin + let nbsp = count_spaces s in + indentation nbsp; + let s = String.sub s nbsp (String.length s - nbsp) in + ident s (lexeme_start lexbuf + nbsp); + let eol= body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end } | space* gallina_kw { let s = lexeme lexbuf in - let nbsp = count_spaces s in + let nbsp = count_spaces s in + let s = String.sub s nbsp (String.length s - nbsp) in indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); - let eol= body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } + ident s (lexeme_start lexbuf + nbsp); + let eol= body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space* "(**" space+ "printing" space+ (identifier | token) space+ { let tok = lexeme lexbuf in let s = printing_token lexbuf in -- cgit v1.2.3