aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index af9eb3af1..56a6bd578 100644
--- a/Makefile
+++ b/Makefile
@@ -181,11 +181,12 @@ TACTICS=\
tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
tactics/nbtermdn.cmo tactics/tacticals.cmo \
tactics/hipattern.cmo tactics/tactics.cmo \
+ tactics/evar_tactics.cmo \
tactics/hiddentac.cmo tactics/elim.cmo \
tactics/dhyp.cmo tactics/auto.cmo \
tactics/setoid_replace.cmo tactics/equality.cmo \
tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
- tactics/tacinterp.cmo \
+ tactics/tacinterp.cmo
TOPLEVEL=\
toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \