aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.coq
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-05-02 20:49:25 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-05-02 20:49:25 +0000
commit5b0f516e7e1f6d2ea8ca0485ffe347a613b01a5c (patch)
treebf106a29e38172fcbd0ee48bc4531c07d46ff5aa /.depend.coq
parent1555e5a4cf7c2662d31d7875f7cc217150b49f4c (diff)
portage Omega (mais toujours pas Zpower et Zlogarithm)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.depend.coq')
-rw-r--r--.depend.coq5
1 files changed, 5 insertions, 0 deletions
diff --git a/.depend.coq b/.depend.coq
index 244665111..f8ba1f558 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -50,6 +50,11 @@ theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theorie
theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo parsing/g_natsyntax.cmo
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/omega/Zpower.vo: contrib/omega/Zpower.v contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
+contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
+contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
tactics/Tauto.vo: tactics/Tauto.v
tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
tactics/Equality.vo: tactics/Equality.v