aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorcoq2002-10-07 16:56:17 +0000
committercoq2002-10-07 16:56:17 +0000
commit02ae9a0b28366372c9eaad1c25428c65314e6fcb (patch)
tree3526dd0b974d94975edab48075eb6b8117ff2ecb /Makefile
parentfb8c46171399af936caa3fbab8eff0cfc06ec94d (diff)
Lazy manuelles dans le code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile14
1 files changed, 5 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index e660dbea80..32b8315963 100644
--- a/Makefile
+++ b/Makefile
@@ -304,13 +304,10 @@ COQTOPBYTE=bin/coqtop.byte$(EXE)
COQTOPOPT=bin/coqtop.opt$(EXE)
BESTCOQTOP=bin/coqtop.$(BEST)$(EXE)
COQTOP=bin/coqtop$(EXE)
+COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE)
-# COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE)
-
-COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP)
-
-#\
-# $(COQINTERFACE)
+COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \
+ $(COQINTERFACE)
coqbinaries:: ${COQBINARIES}
@@ -393,7 +390,7 @@ clean::
# tests
###########################################################################
-check:: world bin/parser
+check:: world
cd test-suite; ./check -$(BEST) | tee check.log
if grep -F 'Error!' test-suite/check.log ; then false; fi
@@ -623,8 +620,7 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init
CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
$(CORRECTNESSVO) $(FOURIERVO) \
- $(JPROVERVO) $(CCVO)
-# $(INTERFACEV0)
+ $(JPROVERVO) $(INTERFACEV0) $(CCVO)
$(CONTRIBVO): states/initial.coq