diff options
| author | jforest | 2007-04-05 16:49:53 +0000 |
|---|---|---|
| committer | jforest | 2007-04-05 16:49:53 +0000 |
| commit | 443e5f39a15752541e54bf70058b9da1aa27c33d (patch) | |
| tree | 3e8f9a91a0c059c92eba6c445ace4729e70b5b5a /Makefile | |
| parent | 00a231e635d8db8fa60d223c8c24dd744cd5e264 (diff) | |
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
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 3 |
1 files changed, 1 insertions, 2 deletions
@@ -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 |