diff options
| author | coq | 2006-02-01 16:35:55 +0000 |
|---|---|---|
| committer | coq | 2006-02-01 16:35:55 +0000 |
| commit | d67a33093ae171ab7efec8a90ea7fce924d3dc10 (patch) | |
| tree | 164fae58ac8e3ea49fa88fafc9d37124bc5640a0 /Makefile | |
| parent | 9061e9a6476288252463ace449d6aa0e92f1b232 (diff) | |
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
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 6 insertions, 1 deletions
@@ -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 |