diff options
| author | bertot | 2005-11-07 09:37:13 +0000 |
|---|---|---|
| committer | bertot | 2005-11-07 09:37:13 +0000 |
| commit | 0d339294fb35ac87e86cd28b61dfefe589d06fa6 (patch) | |
| tree | 0d6e961964954650d9d7755810a4020d73dbf1c0 /Makefile | |
| parent | 211b882fe1928841d1477b87e26f12bce7cf87b0 (diff) | |
Adds tools to help in defining new general recursive functions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7527 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 15 |
1 files changed, 11 insertions, 4 deletions
@@ -73,7 +73,8 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I contrib/interface -I contrib/fourier \ -I contrib/jprover -I contrib/cc \ -I contrib/funind -I contrib/first-order \ - -I contrib/field -I contrib/subtac -I contrib/rtauto + -I contrib/field -I contrib/subtac -I contrib/rtauto \ + -I contrib/recdef MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -285,6 +286,9 @@ JPROVERCMO=\ FUNINDCMO=\ contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo +RECDEFCMO=\ + contrib/recdef/recdef.cmo + FOCMO=\ contrib/first-order/formula.cmo contrib/first-order/unify.cmo \ contrib/first-order/sequent.cmo contrib/first-order/rules.cmo \ @@ -310,11 +314,12 @@ 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/subtac/sparser.ml4 contrib/subtac/g_eterm.ml4 \ - contrib/rtauto/g_rtauto.ml4 + contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) + $(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ + $(RECDEFCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -1003,6 +1008,8 @@ FOURIERVO=\ FUNINDVO= +RECDEFVO=contrib/recdef/Recdef.vo + JPROVERVO= CCVO= @@ -1015,7 +1022,7 @@ RTAUTOVO = \ CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \ - $(RTAUTOVO) + $(RTAUTOVO) $(RECDEFVO) $(CONTRIBVO): states/initial.coq |