summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend351
-rw-r--r--CHANGES7
-rw-r--r--Makefile20
-rw-r--r--PROBLEMES54
-rw-r--r--TODO51
-rwxr-xr-xconfigure6
-rw-r--r--contrib/funind/functional_principles_proofs.ml282
-rw-r--r--contrib/funind/invfun.ml4
-rw-r--r--contrib/recdef/recdef.ml411
-rw-r--r--ide/coqide.ml14
-rw-r--r--kernel/indtypes.ml10
-rw-r--r--kernel/safe_typing.ml48
-rw-r--r--library/lib.ml50
-rw-r--r--library/nametab.ml12
-rw-r--r--pretyping/evarutil.ml79
-rw-r--r--scripts/coqc.ml7
-rw-r--r--tools/coqdoc/output.ml17
-rw-r--r--tools/coqdoc/pretty.mll35
18 files changed, 508 insertions, 550 deletions
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 <opaque>)
-
-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 "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
if !header_trailer then begin
- printf "<hr/><font size=\"-1\">This page has been generated by ";
- printf "<a href=\"%s\">coqdoc</a></font>\n" self;
+ printf "<hr/>This page has been generated by ";
+ printf "<a href=\"%s\">coqdoc</a>\n" self;
printf "</div>\n\n</div>\n\n</body>\n</html>"
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 "<a name=\"%s\"></a><h%d>" lab lev;
+ printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev;
f ();
- printf "</h%d class=\"section\">\n" lev
+ printf "</h%d>\n" lev
let rule () = printf "<hr/>\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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 12:23:50 +0000