diff options
| author | bertot | 2006-02-08 13:18:52 +0000 |
|---|---|---|
| committer | bertot | 2006-02-08 13:18:52 +0000 |
| commit | 78eff446f542002e24a7ac0d101d0910e15d7b3d (patch) | |
| tree | 3a10bf23580601878f982b1867189942678eabda /Makefile | |
| parent | 8d5c13b842a22a005268f24f73669c585733b894 (diff) | |
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
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -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) |