From 443e5f39a15752541e54bf70058b9da1aa27c33d Mon Sep 17 00:00:00 2001
From: jforest
Date: Thu, 5 Apr 2007 16:49:53 +0000
Subject: On n'a plus besoin de compiler les anciens fichiers de functionnal
 induction (version P.Courtieu).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9748 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 0d8c825bca..f3ffc9427e 100644
--- a/Makefile
+++ b/Makefile
@@ -285,7 +285,6 @@ JPROVERCMO=\
   contrib/jprover/jprover.cmo
 
 FUNINDCMO=\
-  contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo \
   contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \
   contrib/funind/rawterm_to_relation.cmo \
   contrib/funind/functional_principles_proofs.cmo \
@@ -319,7 +318,7 @@ RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 	contrib/rtauto/g_rtauto.cmo
 
 ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/g_congruence.ml4 \
-	contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \
+	contrib/first-order/g_ground.ml4 \
 	contrib/subtac/g_subtac.ml4 contrib/subtac/g_eterm.ml4 \
 	contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4 \
 	contrib/funind/indfun_main.ml4 
-- 
cgit v1.2.3