From 983f5ce6bd855e058e469de79b14361e2b920086 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 22 Dec 2006 16:32:46 +0000
Subject: [PATCH] legacy development created

---
 helm/software/matita/Makefile                 |  1 +
 .../matita/contribs/CoRN-Decl/preamble.ma     |  2 +-
 .../LAMBDA-TYPES/Level-1/Base/ext/preamble.ma |  2 +-
 .../software/matita/contribs/developments.txt | 12 ++++++
 .../matita/{library => }/legacy/coq.ma        |  0
 helm/software/matita/legacy/makefile          | 39 +++++++++++++++++++
 .../matita/library/library_notation.ma        |  3 +-
 7 files changed, 56 insertions(+), 3 deletions(-)
 create mode 100644 helm/software/matita/contribs/developments.txt
 rename helm/software/matita/{library => }/legacy/coq.ma (100%)
 create mode 100644 helm/software/matita/legacy/makefile

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index ab03a892f..fd96cc5f9 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -201,6 +201,7 @@ distclean: clean
 	$(H)rm -rf .matita
 
 TEST_DIRS = 				\
+	legacy                          \
 	library 			\
 	tests 				\
 	dama				\
diff --git a/helm/software/matita/contribs/CoRN-Decl/preamble.ma b/helm/software/matita/contribs/CoRN-Decl/preamble.ma
index 6ea5e41b0..9d7d5533a 100644
--- a/helm/software/matita/contribs/CoRN-Decl/preamble.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/preamble.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/preamble".
 
-include "legacy/coq.ma".
+include "../../legacy/coq.ma".
 
 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
index b4c69f299..6a41598bb 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble".
 
-include' "legacy/coq.ma".
+include' "../../../../legacy/coq.ma".
 
 (* FG: This is because "and" is a reserved keyword of the parser *)
 alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
diff --git a/helm/software/matita/contribs/developments.txt b/helm/software/matita/contribs/developments.txt
new file mode 100644
index 000000000..4d5044941
--- /dev/null
+++ b/helm/software/matita/contribs/developments.txt
@@ -0,0 +1,12 @@
+Root directories of current matita developments 
+
+software/matita/legacy
+software/matita/library
+software/matita/tests
+software/matita/dama
+software/matita/contribs/CoRN
+software/matita/contribs/PREDICATIVE-TOPOLOGY
+software/matita/contribs/RELATIONAL
+software/matita/contribs/LAMBDA-TYPES/Unified
+software/matita/contribs/LAMBDA-TYPES/Level-1/Base
+software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta
diff --git a/helm/software/matita/library/legacy/coq.ma b/helm/software/matita/legacy/coq.ma
similarity index 100%
rename from helm/software/matita/library/legacy/coq.ma
rename to helm/software/matita/legacy/coq.ma
diff --git a/helm/software/matita/legacy/makefile b/helm/software/matita/legacy/makefile
new file mode 100644
index 000000000..c4020f673
--- /dev/null
+++ b/helm/software/matita/legacy/makefile
@@ -0,0 +1,39 @@
+H=@
+
+RT_BASEDIR=../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+ifneq "$(SRC)" ""
+  XXX="SRC=$(SRC)"
+endif
+
+all: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+	
+preall:
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
+preall.opt:
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)
diff --git a/helm/software/matita/library/library_notation.ma b/helm/software/matita/library/library_notation.ma
index 475fe38f8..f86396f1f 100644
--- a/helm/software/matita/library/library_notation.ma
+++ b/helm/software/matita/library/library_notation.ma
@@ -29,7 +29,8 @@ include "nat/factorization.ma".
 include "nat/times.ma".
 include "nat/fermat_little_theorem.ma".
 include "nat/nat.ma".
-include "legacy/coq.ma".
+(* FG: coq non c'entra con library, o sbaglio? *)
+(* include "legacy/coq.ma". *)
 include "Z/compare.ma".
 include "Z/plus.ma".
 include "Z/times.ma".
-- 
2.39.2