aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-03-18 14:17:00 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-03-18 14:17:00 +0000
commit65f1600d6c405792bcb6831549622ce4afcd7621 (patch)
tree0b90157ff3f5cc651eefb0d5020ea0d682edc42e /Makefile
parent19ae95167aa57280c6f5397b67aea771cbd8b77c (diff)
appel de Simplify depuis Coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6854 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 0cb6223e3..3ed55298e 100644
--- a/Makefile
+++ b/Makefile
@@ -246,7 +246,7 @@ RINGCMO=\
contrib/ring/ring.cmo contrib/ring/g_ring.cmo
DPCMO=\
- contrib/dp/dp.cmo contrib/dp/g_dp.cmo
+ contrib/dp/dp_simplify.cmo contrib/dp/dp.cmo contrib/dp/g_dp.cmo
FIELDCMO=\
contrib/field/field.cmo