diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-16 10:18:21 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-16 10:18:21 +0000 |
| commit | 9cb6bb1624719baa6d0d05f89bc8a537b4111b69 (patch) | |
| tree | 7dd44fa2a5bcf81292cdac4290f38858893f290f /Makefile | |
| parent | 8579b8f77f7196f6a3bfb79c24352f923c0b38c1 (diff) | |
tactiques prouveurs premier ordre dans contrib/dp/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6842 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 10 |
1 files changed, 7 insertions, 3 deletions
@@ -68,7 +68,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I interp -I toplevel -I parsing -I ide/utils \ -I ide -I translate \ -I contrib/omega -I contrib/romega \ - -I contrib/ring -I contrib/xml \ + -I contrib/ring -I contrib/dp -I contrib/xml \ -I contrib/extraction \ -I contrib/interface -I contrib/fourier \ -I contrib/jprover -I contrib/cc \ @@ -229,7 +229,7 @@ USERTACCMX=$(USERTAC:.ml4=.cmx) ML4FILES +=\ contrib/omega/g_omega.ml4 \ contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ - contrib/ring/g_ring.ml4 \ + contrib/ring/g_ring.ml4 contrib/dp/g_dp.ml4 \ contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \ contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4 @@ -245,6 +245,9 @@ RINGCMO=\ contrib/ring/quote.cmo contrib/ring/g_quote.cmo \ contrib/ring/ring.cmo contrib/ring/g_ring.cmo +DPCMO=\ + contrib/dp/dp.cmo contrib/dp/g_dp.cmo + FIELDCMO=\ contrib/field/field.cmo @@ -292,7 +295,7 @@ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \ contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 -CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \ +CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ $(CCCMO) $(FUNINDCMO) $(FOCMO) @@ -996,6 +999,7 @@ $(CONTRIBVO): states/initial.coq contrib: $(CONTRIBVO) $(CONTRIBCMO) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) ring: $(RINGVO) $(RINGCMO) +dp: $(DPCMO) xml: $(XMLVO) $(XMLCMO) extraction: $(EXTRACTIONCMO) field: $(FIELDVO) $(FIELDCMO) |