diff options
| author | filliatr | 2002-10-07 01:01:53 +0000 |
|---|---|---|
| committer | filliatr | 2002-10-07 01:01:53 +0000 |
| commit | 8b0295dec76d48f71cb12c21c4f665ea0f235ac1 (patch) | |
| tree | 03f5c442f904d91c9631cf8488b37f96f836bea9 | |
| parent | f609333b25231cab07fec19437f81d30a95a04ee (diff) | |
maj
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3093 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 14 | ||||
| -rw-r--r-- | .depend.coq | 1 |
2 files changed, 8 insertions, 7 deletions
@@ -2555,14 +2555,16 @@ contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \ contrib/interface/vtp.cmi contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ parsing/astterm.cmi parsing/coqast.cmi contrib/interface/ctast.cmo \ - tactics/extraargs.cmi parsing/genarg.cmi library/libnames.cmi \ - kernel/names.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo lib/util.cmi \ - toplevel/vernacexpr.cmo contrib/interface/xlate.cmi + tactics/eauto.cmo tactics/extraargs.cmi parsing/genarg.cmi \ + library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo \ + contrib/interface/xlate.cmi contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \ parsing/astterm.cmx parsing/coqast.cmx contrib/interface/ctast.cmx \ - tactics/extraargs.cmx parsing/genarg.cmx library/libnames.cmx \ - kernel/names.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx lib/util.cmx \ - toplevel/vernacexpr.cmx contrib/interface/xlate.cmi + tactics/eauto.cmx tactics/extraargs.cmx parsing/genarg.cmx \ + library/libnames.cmx kernel/names.cmx pretyping/rawterm.cmx \ + proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx \ + contrib/interface/xlate.cmi contrib/jprover/jall.cmo: contrib/jprover/jlogic.cmi \ contrib/jprover/jterm.cmi contrib/jprover/jtunify.cmi \ contrib/jprover/opname.cmi contrib/jprover/jall.cmi diff --git a/.depend.coq b/.depend.coq index 54d0a151d7..031c954ed7 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,5 +1,4 @@ contrib/cc/CC.vo: contrib/cc/CC.v theories/Logic/Eqdep_dec.vo -contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v |