From 763102437580da08cd96d06d05d99dc1a3eda1b1 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 5 Apr 2001 14:29:44 +0000
Subject: mise en place de Correctness; vieille syntaxe Extraction viree de
 g_vernac.ml4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 381b9cfb9e..2c1adf772b 100644
--- a/Makefile
+++ b/Makefile
@@ -277,9 +277,6 @@ parsing: $(PARSING)
 pretyping: $(PRETYPING)
 toplevel: $(TOPLEVEL)
 
-extraction: $(EXTRACTIONCMO)
-correctness: $(CORRECTNESSCMO)
-
 # special binaries for debugging
 
 bin/coq-extraction: $(COQMKTOP) $(CMO) $(USERTACCMO) $(EXTRACTIONCMO)
@@ -429,8 +426,19 @@ clean::
 ###########################################################################
 
 EXTRACTIONVO=contrib/extraction/Extraction.vo
-contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v \
-                                  $(EXTRACTIONCMO)
+contrib/extraction/%.vo: contrib/extraction/%.v
+	$(COQC) -q -byte -bindir bin $(COQINCLUDES) $<
+
+CORRECTNESSVO=contrib/correctness/Arrays.vo				\
+	contrib/correctness/Correctness.vo				\
+	contrib/correctness/Exchange.vo					\
+	contrib/correctness/ArrayPermut.vo				\
+	contrib/correctness/ProgBool.vo contrib/correctness/ProgInt.vo	\
+	contrib/correctness/ProgWf.vo contrib/correctness/Sorted.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 \
@@ -459,6 +467,8 @@ contrib: $(CONTRIBVO)
 omega: $(OMEGAVO)
 ring: $(RINGVO)
 xml: $(XMLVO)
+extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
+correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO)
 
 clean::
 	rm -f contrib/*/*.cm[io] contrib/*/*.vo
-- 
cgit v1.2.3