aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorfilliatr1999-12-07 14:56:36 +0000
committerfilliatr1999-12-07 14:56:36 +0000
commitf2da732ffd5db2b93a2c8120c668f8b2f6068d3b (patch)
tree6cf46158c757cb654c241728eed3ea03bd04d0d0 /Makefile
parent59263ca55924e2f43097ae2296f541b153981bf8 (diff)
debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 68f8d4a092..0caff0f35c 100644
--- a/Makefile
+++ b/Makefile
@@ -96,6 +96,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \
tactics/wcclausenv.cmo tactics/tacticals.cmo tactics/tactics.cmo \
tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
+# tactics/dhyp.cmo tactics/auto.cmo
TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \