simplification du make depend; fonctions de stat. util. memoire dans certains modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 116 insertions, 142 deletions

diff --git a/.depend b/.depend
index 3cdc0590c..6414d5df8 100644
--- a/.depend
+++ b/.depend
@@ -4,8 +4,8 @@ kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi 
 kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
-kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/univ.cmi 
+kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 kernel/indtypes.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
@@ -195,8 +195,8 @@ toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
 toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
-toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
-    toplevel/vernacinterp.cmi 
+toplevel/vernacentries.cmi: kernel/environ.cmi kernel/names.cmi \
+    proofs/proof_type.cmi kernel/term.cmi toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_type.cmi 
 contrib/extraction/extraction.cmi: contrib/extraction/miniml.cmi \
@@ -461,6 +461,12 @@ parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi
 parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_minicoq.cmo: kernel/environ.cmi parsing/lexer.cmi kernel/names.cmi \
+    lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    parsing/g_minicoq.cmi 
+parsing/g_minicoq.cmx: kernel/environ.cmx parsing/lexer.cmx kernel/names.cmx \
+    lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+    parsing/g_minicoq.cmi 
 parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
     parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
     parsing/stdlib.cmi parsing/termast.cmi lib/util.cmi \
@@ -501,20 +507,6 @@ parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
     lib/util.cmi parsing/pcoq.cmi 
 parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
     lib/util.cmx parsing/pcoq.cmi 
-parsing/pretty-avec-modif-print-name.cmo: pretyping/classops.cmi \
-    kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
-    kernel/evd.cmi library/global.cmi library/impargs.cmi \
-    kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \
-    library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    parsing/printer.cmi kernel/reduction.cmi kernel/sign.cmi \
-    pretyping/syntax_def.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi 
-parsing/pretty-avec-modif-print-name.cmx: pretyping/classops.cmx \
-    kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
-    kernel/evd.cmx library/global.cmx library/impargs.cmx \
-    kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \
-    library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx \
-    pretyping/syntax_def.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx 
 parsing/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
     library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
@@ -1031,22 +1023,12 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \
     kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
     proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
     kernel/term.cmx lib/util.cmx tactics/tactics.cmi 
-tactics/tauto.cmo: parsing/ast.cmi tactics/auto.cmi proofs/clenv.cmi \
-    kernel/closure.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi tactics/hipattern.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi lib/util.cmi 
-tactics/tauto.cmx: parsing/ast.cmx tactics/auto.cmx proofs/clenv.cmx \
-    kernel/closure.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx tactics/hipattern.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    pretyping/retyping.cmx kernel/sign.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx lib/util.cmx 
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi 
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+    kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx 
 tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi pretyping/pattern.cmi \
     pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi 
 tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx pretyping/pattern.cmx \
@@ -1098,7 +1080,7 @@ toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
 toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi lib/system.cmi \
     toplevel/toplevel.cmi toplevel/vernac.cmi toplevel/coqinit.cmi 
-toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmi \
+toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx lib/system.cmx \
     toplevel/toplevel.cmx toplevel/vernac.cmx toplevel/coqinit.cmi 
 toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
@@ -1109,7 +1091,7 @@ toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
     toplevel/coqtop.cmi 
 toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
     toplevel/errors.cmx library/lib.cmx library/library.cmx \
-    toplevel/mltop.cmi kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    toplevel/mltop.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
     lib/pp.cmx lib/profile.cmx library/states.cmx lib/system.cmx \
     toplevel/toplevel.cmx toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx \
     toplevel/coqtop.cmi 
@@ -1142,7 +1124,7 @@ toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx kernel/indtypes.cmx \
 toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \
     kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi 
-toplevel/fhimsg.cmx: kernel/environ.cmx parsing/g_minicoq.cmi \
+toplevel/fhimsg.cmx: kernel/environ.cmx parsing/g_minicoq.cmx \
     kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/type_errors.cmx lib/util.cmx toplevel/fhimsg.cmi 
 toplevel/himsg.cmo: parsing/ast.cmi kernel/environ.cmi library/global.cmi \
@@ -1176,9 +1158,15 @@ toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/type_errors.cmi lib/util.cmi 
 toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \
-    parsing/g_minicoq.cmi kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/g_minicoq.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx lib/util.cmx 
+toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
+    library/nametab.cmi lib/pp.cmi library/summary.cmi lib/system.cmi \
+    lib/util.cmi toplevel/vernacinterp.cmi toplevel/mltop.cmi 
+toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
+    library/nametab.cmx lib/pp.cmx library/summary.cmx lib/system.cmx \
+    lib/util.cmx toplevel/vernacinterp.cmx toplevel/mltop.cmi 
 toplevel/protectedtoplevel.cmo: toplevel/errors.cmi \
     toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \
     toplevel/vernac.cmi toplevel/vernacinterp.cmi \
@@ -1211,7 +1199,7 @@ toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \
     kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
     lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \
     toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi 
-toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
+toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \
     kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
     lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
@@ -1248,7 +1236,7 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     toplevel/discharge.cmx kernel/environ.cmx pretyping/evarutil.cmx \
     kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \
     library/impargs.cmx library/lib.cmx library/libobject.cmx \
-    library/library.cmx toplevel/metasyntax.cmx toplevel/mltop.cmi \
+    library/library.cmx toplevel/metasyntax.cmx toplevel/mltop.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \
     lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \
     pretyping/pretype_errors.cmx parsing/printer.cmx proofs/proof_trees.cmx \
@@ -1337,3 +1325,17 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
     contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/xml/xmlcommand.cmx 
+tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
+parsing/lexer.cmo: 
+parsing/q_coqast.cmo: 
+parsing/g_prim.cmo: 
+parsing/pcoq.cmo: 
+parsing/g_basevernac.cmo: parsing/grammar.cma
+parsing/g_minicoq.cmo: parsing/grammar.cma
+parsing/g_vernac.cmo: parsing/grammar.cma
+parsing/g_proofs.cmo: parsing/grammar.cma
+parsing/g_cases.cmo: parsing/grammar.cma
+parsing/g_constr.cmo: parsing/grammar.cma
+parsing/g_tactic.cmo: parsing/grammar.cma
+parsing/extend.cmo: parsing/grammar.cma
+toplevel/mltop.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index ce5ebba66..94ccf5671 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,66 +1,14 @@
-tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
-    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi 
-tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
-    kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx 
-parsing/lexer.cmo: parsing/lexer.cmi 
-parsing/lexer.cmx: parsing/lexer.cmi 
-parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
-parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
-parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx 
-parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
-    lib/util.cmi parsing/pcoq.cmi 
-parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
-    lib/util.cmx parsing/pcoq.cmi 
-parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    toplevel/vernac.cmi 
-parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
-    toplevel/vernac.cmx 
-parsing/g_minicoq.cmo: kernel/environ.cmi parsing/lexer.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
-    parsing/g_minicoq.cmi 
-parsing/g_minicoq.cmx: kernel/environ.cmx parsing/lexer.cmx kernel/names.cmx \
-    lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
-    parsing/g_minicoq.cmi 
-parsing/g_vernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi toplevel/vernac.cmi 
-parsing/g_vernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx toplevel/vernac.cmx 
-parsing/g_proofs.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
-    lib/util.cmi toplevel/vernac.cmi 
-parsing/g_proofs.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
-    lib/util.cmx toplevel/vernac.cmx 
-parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
-parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
-parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi toplevel/vernac.cmi 
-parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx toplevel/vernac.cmx 
-parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
-parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
-    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
-toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
-    lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi toplevel/mltop.cmi 
-toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
-    lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx toplevel/mltop.cmi 
-tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
-parsing/lexer.cmo: 
-parsing/q_coqast.cmo: 
-parsing/g_prim.cmo: 
-parsing/pcoq.cmo: 
-parsing/g_basevernac.cmo: parsing/grammar.cma
-parsing/g_minicoq.cmo: parsing/grammar.cma
-parsing/g_vernac.cmo: parsing/grammar.cma
-parsing/g_proofs.cmo: parsing/grammar.cma
-parsing/g_cases.cmo: parsing/grammar.cma
-parsing/g_constr.cmo: parsing/grammar.cma
-parsing/g_tactic.cmo: parsing/grammar.cma
-parsing/extend.cmo: parsing/grammar.cma
-toplevel/mltop.cmo: 
+tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
+parsing/lexer.ml: 
+parsing/q_coqast.ml: 
+parsing/g_prim.ml: 
+parsing/pcoq.ml: 
+parsing/g_basevernac.ml: parsing/grammar.cma
+parsing/g_minicoq.ml: parsing/grammar.cma
+parsing/g_vernac.ml: parsing/grammar.cma
+parsing/g_proofs.ml: parsing/grammar.cma
+parsing/g_cases.ml: parsing/grammar.cma
+parsing/g_constr.ml: parsing/grammar.cma
+parsing/g_tactic.ml: parsing/grammar.cma
+parsing/extend.ml: parsing/grammar.cma
+toplevel/mltop.ml: 
diff --git a/.depend.camlp4.2 b/.depend.camlp4.2
deleted file mode 100644
index 94ccf5671..000000000
--- a/.depend.camlp4.2
+++ /dev/null
@@ -1,14 +0,0 @@
-tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
-parsing/lexer.ml: 
-parsing/q_coqast.ml: 
-parsing/g_prim.ml: 
-parsing/pcoq.ml: 
-parsing/g_basevernac.ml: parsing/grammar.cma
-parsing/g_minicoq.ml: parsing/grammar.cma
-parsing/g_vernac.ml: parsing/grammar.cma
-parsing/g_proofs.ml: parsing/grammar.cma
-parsing/g_cases.ml: parsing/grammar.cma
-parsing/g_constr.ml: parsing/grammar.cma
-parsing/g_tactic.ml: parsing/grammar.cma
-parsing/extend.ml: parsing/grammar.cma
-toplevel/mltop.ml: 
diff --git a/.depend.coq b/.depend.coq
index 9770de1d3..aa7e426e3 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -124,6 +124,8 @@ test-suite/success/mutual_ind.vo: test-suite/success/mutual_ind.v theories/Lists
 test-suite/success/induct.vo: test-suite/success/induct.v theories/Lists/PolyList.vo
 test-suite/success/inds_type_sec.vo: test-suite/success/inds_type_sec.v
 test-suite/success/fix.vo: test-suite/success/fix.v theories/Bool/Bool.vo theories/Zarith/ZArith.vo
+test-suite/success/eqdecide.vo: test-suite/success/eqdecide.v
+test-suite/success/Tauto.vo: test-suite/success/Tauto.v
 test-suite/success/Check.vo: test-suite/success/Check.v
 test-suite/success/Cases.vo: test-suite/success/Cases.v theories/Bool/Bool.vo theories/Arith/Peano_dec.vo theories/Init/Prelude.vo theories/Init/Logic_TypeSyntax.vo theories/Init/Logic_Type.vo
 test-suite/success/Apply.vo: test-suite/success/Apply.v
@@ -131,6 +133,7 @@ test-suite/failure/redef.vo: test-suite/failure/redef.v
 test-suite/failure/positivity.vo: test-suite/failure/positivity.v
 test-suite/failure/illtype1.vo: test-suite/failure/illtype1.v
 test-suite/failure/clash_cons.vo: test-suite/failure/clash_cons.v
+test-suite/failure/Tauto.vo: test-suite/failure/Tauto.v
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
 test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
 contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
@@ -150,13 +153,14 @@ tactics/Tauto.vo: tactics/Tauto.v
 tactics/Refine.vo: tactics/Refine.v
 tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
 tactics/Equality.vo: tactics/Equality.v
+tactics/EqDecide.vo: tactics/EqDecide.v
 tactics/EAuto.vo: tactics/EAuto.v
 tactics/AutoRewrite.vo: tactics/AutoRewrite.v
 syntax/PPTactic.vo: syntax/PPTactic.v
 syntax/PPConstr.vo: syntax/PPConstr.v
 syntax/PPCases.vo: syntax/PPCases.v
 syntax/MakeBare.vo: syntax/MakeBare.v
-states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo
+states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo test-suite/success/Tauto.vo tactics/Inv.vo tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo tactics/EqDecide.vo
 contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
 contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
diff --git a/Makefile b/Makefile
index 33f4c1c8b..fae9c8d68 100644
--- a/Makefile
+++ b/Makefile
@@ -634,32 +634,31 @@ cleanconfig::
 # Dependencies
 ###########################################################################
 
-alldepend: depend dependcoq dependcamlp4
-
-depend: beforedepend
-	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend
+alldepend: depend dependcoq 
 
 dependcoq: beforedepend
 	$(COQDEP) $(COQINCLUDES) */*.v */*/*.v > .depend.coq
 
-# Dependency of camlp4 files: this is tricky.
+# Computing the dependencies in camlp4 files is tricky.
 # We proceed in several steps:
+
 ML4FILESML = $(ML4FILES:.ml4=.ml)
-dependcamlp4:
+
+depend: beforedepend
 # 1. We express dependencies of the .ml files w.r.t their grammars
-	rm -f .depend.camlp4.2
+	rm -f .depend.camlp4
 	for f in $(ML4FILES); do \
-	  printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4.2; \
-	  echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4.2; \
+	  printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \
+	  echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \
 	done
 # 2. Then we are able to produce the .ml files using Makefile.dep
 	$(MAKE) -f Makefile.dep $(ML4FILESML)
 # 3. We compute the dependencies inside the .ml files using ocamldep
-	ocamldep $(DEPFLAGS) $(ML4FILESML) > .depend.camlp4
+	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend
 # 4. We express dependencies of .cmo files w.r.t their grammars
 	for f in $(ML4FILES); do \
-	  printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend.camlp4; \
-	  echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \
+	  printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend; \
+	  echo `$(CAMLP4DEPS) $$f` >> .depend; \
 	done
 # 5. Finally, we erase the generated .ml files
 	rm -f $(ML4FILESML)
@@ -670,4 +669,3 @@ clean::
 
 include .depend
 include .depend.coq
-include .depend.camlp4
diff --git a/Makefile.dep b/Makefile.dep
index 18f4ae29f..2b2905033 100644
--- a/Makefile.dep
+++ b/Makefile.dep
@@ -2,7 +2,7 @@
 # This Makefile is designed to make the .ml files corresponding to .ml4 files
 
 include Makefile
-include .depend.camlp4.2
+include .depend.camlp4
 
 .ml4.ml:
 	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl $< > $@ || rm -f $@
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0c51f085e..cb4b1e003 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -410,3 +410,12 @@ type unsafe_type_judgment = {
   utj_val : constr;
   utj_type : sorts }
 
+(*s Memory use of an environment. *)
+
+open Printf
+
+let mem env =
+  let glb = env.env_globals in 
+  h 0 [< 'sTR (sprintf "%dk (cst = %dk / ind = %dk / unv = %dk)"
+		 (size_kb env) (size_kb glb.env_constants) 
+		 (size_kb glb.env_inductives) (size_kb env.env_universes)) >]
diff --git a/kernel/environ.mli b/kernel/environ.mli
index bde8823f3..65a2bb671 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -177,3 +177,7 @@ type unsafe_judgment = {
 type unsafe_type_judgment = { 
   utj_val : constr;
   utj_type : sorts }
+
+(*s Displays the memory use of an environment. *)
+
+val mem : env -> Pp.std_ppcmds
diff --git a/lib/util.ml b/lib/util.ml
index e7cf32564..b5611c50b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -551,8 +551,14 @@ module Size = struct
     traverse (repr o);
     !count
 
-  let size_b o = (size_w o) * Sys.word_size lsr 3
+  let size_b o = (size_w o) * (Sys.word_size / 8)
+
+  let size_kb o = (size_w o) / (8192 / Sys.word_size)
 
 end
 
+let size_w = Size.size_w
 let size_b = Size.size_b
+let size_kb = Size.size_kb
+
+
diff --git a/lib/util.mli b/lib/util.mli
index fc3c980c6..94d1d44f8 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -159,6 +159,8 @@ val prlist_with_sep :
 val prvect_with_sep :
    (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b array -> 'a Stream.t
 
-(*s Size of ocaml values. *)
+(*s Size of an ocaml value (in words, bytes and kilobytes). *)
 
+val size_w : 'a -> int
 val size_b : 'a -> int
+val size_kb : 'a -> int
diff --git a/library/library.ml b/library/library.ml
index 6ff8a84db..b0c1a2ecd 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -249,3 +249,13 @@ let fmt_modules_state () =
      prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) opened ; 'fNL ;
      'sTR "Loaded Modules: " ;
      prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) loaded ; 'fNL >]
+
+(*s Display the memory use of a module. *)
+
+open Printf
+
+let mem s =
+  let m = find_module s in
+  h 0 [< 'sTR (sprintf "%dk (cenv = %dk / seg = %dk / nmt = %dk)"
+		 (size_kb m) (size_kb m.module_compiled_env) 
+		 (size_kb m.module_declarations) (size_kb m.module_nametab)) >]
diff --git a/library/library.mli b/library/library.mli
index 18ebb9708..43fa04e8b 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -59,3 +59,7 @@ val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
 val get_load_path : unit -> System.load_path
 val add_load_path_entry : System.load_path_entry -> unit
 val remove_path : string -> unit
+
+(*s Displays the memory use of a module. *)
+
+val mem : string -> Pp.std_ppcmds
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index fca4d85fe..37a41cd25 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -664,10 +664,11 @@ let extract_pftreestate pts =
   if subgoals <> [] then
    errorlabstrm "extract_proof"
    [< 'sTR "Attempt to save an incomplete proof" >];
-(* local_strong (whd_betaiotaevar pts.tpf.goal.evar_env (ts_it pts.tpfsigma))*)
-  local_strong (whd_ise (ts_it pts.tpfsigma))
-    pfterm
-
+  (***  
+  let env = Global.env_of_context pts.tpf.goal.evar_hyps in
+  strong whd_betaiotaevar env (ts_it pts.tpfsigma) pfterm
+  ***)
+  local_strong (whd_ise (ts_it pts.tpfsigma)) pfterm
 
 (* Focus on the first leaf proof in a proof-tree state *)
 
diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v
index c933ebedc..d301a7d40 100644
--- a/theories/Zarith/fast_integer.v
+++ b/theories/Zarith/fast_integer.v
@@ -1476,4 +1476,4 @@ Intros x y;Case x;Case y; [
 | Unfold Zcompare; Intros q p; Rewrite <- ZC4; Intros H; Exists (true_sub q p);
   Simpl; Rewrite (ZC1 q p H); Trivial with arith].
 Save.
-End fast_integers.
\ No newline at end of file
+End fast_integers.