diff options
| author | coq | 2005-05-25 13:13:15 +0000 |
|---|---|---|
| committer | coq | 2005-05-25 13:13:15 +0000 |
| commit | 8464cd8a8df852799da9cb7a1fd94b8faf3cf9c6 (patch) | |
| tree | 5e14754072c2423caed6c298d54bfe493aedba27 /Makefile | |
| parent | 6dfe936f332da0728380ae3a7f75bc87f6c4c447 (diff) | |
Added subtac contrib.
Added some debug printer in termops.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 21 |
1 files changed, 17 insertions, 4 deletions
@@ -73,7 +73,7 @@ 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/field -I contrib/subtac MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -293,12 +293,22 @@ FOCMO=\ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo +SUBTACCMO=\ + contrib/subtac/natural.cmo \ + contrib/subtac/scoq.cmo \ + contrib/subtac/sast.cmo \ + contrib/subtac/infer.cmo \ + contrib/subtac/top_printer.cmo \ + contrib/subtac/rewrite.cmo \ + contrib/subtac/sparser.cmo + ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \ - contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 + contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \ + contrib/subtac/sparser.ml4 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CCCMO) $(FUNINDCMO) $(FOCMO) + $(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -992,8 +1002,10 @@ JPROVERVO= CCVO=\ contrib/cc/CCSolve.vo +SUBTACVO= + CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ - $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) + $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) $(CONTRIBVO): states/initial.coq @@ -1008,6 +1020,7 @@ fourier: $(FOURIERVO) $(FOURIERCMO) jprover: $(JPROVERVO) $(JPROVERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) +subtac: $(SUBTACVO) $(SUBTACCMO) NEWINITVO=$(INITVO) NEWTHEORIESVO=$(THEORIESVO) |