X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FMakefile;h=bbe22f7d159f6610d11a485c4a3c50eeeeb01aa5;hb=378f76d39029c959c67cb1761563156ec68d9002;hp=41590525815a2fbb3f4293e9831a41d6a7c3acaa;hpb=6e1ce1b936a712bea7678d04e55053abc1f5a9cf;p=helm.git

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 415905258..bbe22f7d1 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -5,7 +5,13 @@ include ../Makefile.defs
 NULL =
 H=@
 
-OCAML_FLAGS = -pp $(CAMLP5O) -rectypes
+ifeq ($(ANNOT),true)
+  ANNOTOPTION = -dtypes
+else
+  ANNOTOPTION =
+endif
+
+OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) 
 OCAMLDEP_FLAGS = -pp $(CAMLP5O) 
 PKGS = -package "$(MATITA_REQUIRES)"
 CPKGS = -package "$(MATITA_CREQUIRES)"
@@ -31,23 +37,25 @@ MLI = \
 	lablGraphviz.mli	\
 	matitaTypes.mli		\
 	matitaMisc.mli		\
+	applyTransformation.mli	\
 	matitaEngine.mli	\
 	matitaExcPp.mli 	\
-	applyTransformation.mli	\
 	matitacLib.mli		\
 	matitaInit.mli		\
 	matitaGtkMisc.mli	\
 	matitaAutoGui.mli	\
+	virtuals.mli 		\
 	matitaScript.mli	\
+	predefined_virtuals.mli \
 	matitaMathView.mli 	\
 	matitaGui.mli		\
 	$(NULL)
 CMLI =				\
 	matitaTypes.mli		\
 	matitaMisc.mli		\
+	applyTransformation.mli	\
 	matitaEngine.mli	\
 	matitaExcPp.mli 	\
-	applyTransformation.mli	\
 	matitacLib.mli		\
 	matitaInit.mli		\
 	matitaWiki.mli		\
@@ -61,7 +69,7 @@ ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml)
 # objects for matitac (batch compiler)
 CML = buildTimeConf.ml $(CMLI:%.mli=%.ml)
 MAINCML = $(MAINCMLI:%.mli=%.ml)
-	
+
 PROGRAMS_BYTE = \
 	matita matitac matitadep matitaclean \
 	matitawiki
@@ -179,23 +187,24 @@ distclean: clean
 	$(H)rm -f matita.conf.xml.sample
 	$(H)rm -rf .matita
 
-TEST_DIRS = 				\
-	legacy                          \
-	library 			\
-	tests 				\
-	contribs/dama/dama		\
-	contribs/assembly		\
-	contribs/CoRN	 	        \
-	contribs/RELATIONAL	 	\
-	contribs/LOGIC	       	 	\
-	contribs/PREDICATIVE-TOPOLOGY 	\
+TEST_DIRS = 			\
+	legacy                  \
+	library 		\
+	contribs/character      \
+	tests 			\
+	contribs/dama/dama	\
+	contribs/assembly	\
+	contribs/CoRN	 	\
+	contribs/RELATIONAL	\
+	contribs/LOGIC	       	\
+	contribs/limits 	\
 	$(NULL)
 
 #	library_auto 			
-TEST_DIRS_OPT = 			\
-	$(TEST_DIRS)                    \
+TEST_DIRS_OPT = 		\
+	$(TEST_DIRS)            \
+	contribs/LAMBDA-TYPES 	\
 	$(NULL)
-	#contribs/LAMBDA-TYPES 		\
 
 .PHONY: tests tests.opt cleantests cleantests.opt
 tests: $(foreach d,$(TEST_DIRS),$(d)-test)
@@ -224,9 +233,9 @@ dist_library: install_preliminaries
 	$(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitac -system -noinnertypes)
 	$(H)echo "destroy"
 	$(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitaclean)
-	# sqlite3 only
+# sqlite3 only
 	$(H)cp $(WHERE)/.matita/matita.db  $(WHERE)/metadata.db || true
-	#$(H)rm -rf $(WHERE)/.matita/
+#$(H)rm -rf $(WHERE)/.matita/
 	touch $@
 
 endif
@@ -359,7 +368,7 @@ TAGS:
 	$(H)cd ..; otags -vi -r components/ matita/
 
 .PHONY: depend
-	
+
 depend: 
 	$(H)echo "  OCAMLDEP"
 	$(H)$(OCAMLDEP) *.ml *.mli > .depend