From 4b0da48602bad97f4f5238eccac9fa3a0bdecda4 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 15 Jul 2005 21:57:22 +0000
Subject: Subtac: traitement correct des existentielles et de la récursion.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7237 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 9e2dd4a45a..ea51ca76f6 100644
--- a/Makefile
+++ b/Makefile
@@ -298,6 +298,8 @@ SUBTACCMO=\
 	contrib/subtac/scoq.cmo \
 	contrib/subtac/sast.cmo \
 	contrib/subtac/infer.cmo \
+	contrib/subtac/sutils.cmo \
+	contrib/subtac/eterm.cmo \
 	contrib/subtac/rewrite.cmo \
 	contrib/subtac/sparser.cmo
 
@@ -306,7 +308,8 @@ RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 
 ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \
   contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \
-  contrib/subtac/sparser.ml4 contrib/rtauto/g_rtauto.cmo
+  contrib/subtac/sparser.ml4 contrib/subtac/g_eterm.ml4 \
+  contrib/rtauto/g_rtauto.ml4
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-- 
cgit v1.2.3