From 78eff446f542002e24a7ac0d101d0910e15d7b3d Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 8 Feb 2006 13:18:52 +0000
Subject: Julien: + Recursive definition (repository contrib/recdef) can now be
 used with GenFixpoint syntax by just replacing the usual  {struct x}
 annotation by {wf R x} where x is one of the function declared arguments and
 R is a expression well-typed in the x typing environment. + Bug correction in
 new functional induction + For now no induction principle for general
 recursive definition is generated.

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index c726840be5..476fa00f17 100644
--- a/Makefile
+++ b/Makefile
@@ -307,14 +307,15 @@ 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/funind/indfun_main.ml4 \
   contrib/subtac/sparser.ml4 contrib/subtac/g_eterm.ml4 \
-  contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4
+  contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4 \
+   contrib/funind/indfun_main.ml4 
+
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
-        $(RECDEFCMO) $(NEWRINGCMO)
+	$(CCCMO)  $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
+        $(RECDEFCMO) $(FUNINDCMO) $(NEWRINGCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
-- 
cgit v1.2.3