Ported demodulation on clauses

[helm.git] / helm / software / matita / Makefile

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 8bd708eb79ecee997915b0d7b310b625e5e1a1fd..d8d81bf3713159caa7007221f6cd0922f7a13d9f 100644 (file)
--- 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)"
@@ -38,7 +44,9 @@ MLI = \
        matitaInit.mli          \
        matitaGtkMisc.mli       \
        matitaAutoGui.mli       \
+       virtuals.mli            \
        matitaScript.mli        \
+       predefined_virtuals.mli \
        matitaMathView.mli      \
        matitaGui.mli           \
        $(NULL)
@@ -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