From 0d339294fb35ac87e86cd28b61dfefe589d06fa6 Mon Sep 17 00:00:00 2001
From: bertot
Date: Mon, 7 Nov 2005 09:37:13 +0000
Subject: Adds tools to help in defining new general recursive functions

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index ca3d88a983..cf4682acc6 100644
--- a/Makefile
+++ b/Makefile
@@ -73,7 +73,8 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
               -I contrib/interface -I contrib/fourier \
 	      -I contrib/jprover -I contrib/cc \
 	      -I contrib/funind -I contrib/first-order \
-              -I contrib/field -I contrib/subtac -I contrib/rtauto
+              -I contrib/field -I contrib/subtac -I contrib/rtauto \
+              -I contrib/recdef
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
@@ -285,6 +286,9 @@ JPROVERCMO=\
 FUNINDCMO=\
   contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo 
 
+RECDEFCMO=\
+  contrib/recdef/recdef.cmo
+
 FOCMO=\
   contrib/first-order/formula.cmo contrib/first-order/unify.cmo \
   contrib/first-order/sequent.cmo contrib/first-order/rules.cmo \
@@ -310,11 +314,12 @@ RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/g_congruence.ml4 \
   contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \
   contrib/subtac/sparser.ml4 contrib/subtac/g_eterm.ml4 \
-  contrib/rtauto/g_rtauto.ml4
+  contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO)
+	$(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
+        $(RECDEFCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
@@ -1003,6 +1008,8 @@ FOURIERVO=\
 
 FUNINDVO= 
 
+RECDEFVO=contrib/recdef/Recdef.vo
+
 JPROVERVO= 
 
 CCVO=
@@ -1015,7 +1022,7 @@ RTAUTOVO = \
 
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \
-	    $(RTAUTOVO)
+	    $(RTAUTOVO) $(RECDEFVO)
 
 $(CONTRIBVO): states/initial.coq
 
-- 
cgit v1.2.3