aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
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 \