From d67a33093ae171ab7efec8a90ea7fce924d3dc10 Mon Sep 17 00:00:00 2001
From: coq
Date: Wed, 1 Feb 2006 16:35:55 +0000
Subject: New version of functional induction / inversion. By Julien Forest,
 Benjamin Gregoire, Gilles Barthe.

For the moment, it is as followed:

If one uses GenFixpoint instead of Fixpoint, then induction principles
are generated on the fly (respecting the match structure written by
the user, with wildcards etc). These principles can be used directly
or by tactics "new functional induction" and "functional inversion".

We will soon make "new functional induction" become "functional
induction", before release of V8.1.


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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 67a803ca22..87d4d9b08d 100644
--- a/Makefile
+++ b/Makefile
@@ -274,7 +274,11 @@ JPROVERCMO=\
   contrib/jprover/jprover.cmo
 
 FUNINDCMO=\
-  contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo 
+  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/new_arg_principle.cmo \
+  contrib/funind/invfun.cmo contrib/funind/indfun.cmo \
+  contrib/funind/indfun_main.cmo
 
 RECDEFCMO=\
   contrib/recdef/recdef.cmo
@@ -303,6 +307,7 @@ 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
 
-- 
cgit v1.2.3