maj

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

1 files changed, 2 insertions, 18 deletions

diff --git a/.depend b/.depend
index 01f24a25a5..ac5b3235d3 100644
--- a/.depend
+++ b/.depend
@@ -250,7 +250,7 @@ tactics/equality.cmi: kernel/environ.cmi pretyping/evd.cmi \
     tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \
     proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi tactics/wcclausenv.cmi 
+    tactics/tactics.cmi kernel/term.cmi 
 tactics/extraargs.cmi: parsing/pcoq.cmi proofs/proof_type.cmi \
     proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi 
 tactics/extratactics.cmi: interp/genarg.cmi kernel/names.cmi \
@@ -278,8 +278,7 @@ tactics/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
     interp/topconstr.cmi lib/util.cmi 
 tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi \
     pretyping/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi \
-    tactics/wcclausenv.cmi 
+    kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi 
 tactics/tactics.cmi: proofs/clenv.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evd.cmi library/libnames.cmi \
     kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \
@@ -287,9 +286,6 @@ tactics/tactics.cmi: proofs/clenv.cmi kernel/environ.cmi \
     proofs/tacexpr.cmo proofs/tacmach.cmi pretyping/tacred.cmi \
     tactics/tacticals.cmi kernel/term.cmi interp/topconstr.cmi 
 tactics/termdn.cmi: pretyping/pattern.cmi kernel/term.cmi 
-tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \
-    proofs/evar_refiner.cmi pretyping/evd.cmi kernel/names.cmi \
-    proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
 toplevel/cerrors.cmi: lib/pp.cmi lib/util.cmi 
 toplevel/class.cmi: pretyping/classops.cmi library/decl_kinds.cmo \
     library/declare.cmi library/libnames.cmi kernel/names.cmi \
@@ -1965,18 +1961,6 @@ tactics/termdn.cmo: tactics/dn.cmi library/libnames.cmi library/nameops.cmi \
 tactics/termdn.cmx: tactics/dn.cmx library/libnames.cmx library/nameops.cmx \
     kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx \
     pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx tactics/termdn.cmi 
-tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi \
-    proofs/evar_refiner.cmi pretyping/evd.cmi proofs/logic.cmi \
-    library/nameops.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
-    tactics/wcclausenv.cmi 
-tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
-    proofs/evar_refiner.cmx pretyping/evd.cmx proofs/logic.cmx \
-    library/nameops.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
-    tactics/wcclausenv.cmi 
 tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
 tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo