diff options
| author | filliatr | 2001-04-10 13:21:45 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-10 13:21:45 +0000 |
| commit | 2bb2d480b547e58deb2ec62791c8990ecac777b0 (patch) | |
| tree | 64dafd639dab62bf0c15cda96b9cab129c9c726a /Makefile | |
| parent | 8eaf1799ec07bf823a366920e39d79e827f94971 (diff) | |
réparation Correctness; options Extraction (changement de syntaxe)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 2 insertions, 5 deletions
@@ -201,7 +201,7 @@ CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ contrib/ring/quote.cmo contrib/ring/ring.cmo \ contrib/xml/xml.cmo \ contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo \ - $(EXTRACTIONCMO) + $(EXTRACTIONCMO) $(CORRECTNESSCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -447,9 +447,6 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo \ contrib/correctness/Tuples.vo # contrib/correctness/ProgramsExtraction.vo -contrib/correctness/%.vo: contrib/correctness/%.v - $(COQC) -q -byte -bindir bin $(COQINCLUDES) $< - OMEGAVO = contrib/omega/Omega.vo contrib/omega/Zlogarithm.vo \ contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \ contrib/omega/Zcomplements.vo @@ -468,7 +465,7 @@ contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) $(COQC) -q -byte -bindir bin $(COQINCLUDES) $< -CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO) +CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO) $(CORRECTNESSVO) $(CONTRIBVO): states/initial.coq |