From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Jan 2008 13:10:27 +0000 (+0000)
Subject: ported to the new make system
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=92e53212b1142355777f171bf683066f52135ed7

ported to the new make system
---

diff --git a/matita/contribs/LOGIC/CLE/defs.ma b/matita/contribs/LOGIC/CLE/defs.ma
index 5b3ba49b7..03065ada0 100644
--- a/matita/contribs/LOGIC/CLE/defs.ma
+++ b/matita/contribs/LOGIC/CLE/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/CLE/defs".
+
 
 (* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS
 *)
diff --git a/matita/contribs/LOGIC/Insert/defs.ma b/matita/contribs/LOGIC/Insert/defs.ma
index 821fd99c2..c3109a5f6 100644
--- a/matita/contribs/LOGIC/Insert/defs.ma
+++ b/matita/contribs/LOGIC/Insert/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Insert/defs".
+
 
 (* INSERT RELATION FOR CONTEXTS
 *)
diff --git a/matita/contribs/LOGIC/Insert/fun.ma b/matita/contribs/LOGIC/Insert/fun.ma
index 7c7aba28a..d06a7e29c 100644
--- a/matita/contribs/LOGIC/Insert/fun.ma
+++ b/matita/contribs/LOGIC/Insert/fun.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Insert/fun".
+
 
 include "CLE/defs.ma".
 include "Insert/inv.ma".
diff --git a/matita/contribs/LOGIC/Insert/inv.ma b/matita/contribs/LOGIC/Insert/inv.ma
index 9053183f9..df5ca04f3 100644
--- a/matita/contribs/LOGIC/Insert/inv.ma
+++ b/matita/contribs/LOGIC/Insert/inv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Insert/inv".
+
 
 (*
 *)
diff --git a/matita/contribs/LOGIC/Insert/props.ma b/matita/contribs/LOGIC/Insert/props.ma
index 17148e27e..3289e68a7 100644
--- a/matita/contribs/LOGIC/Insert/props.ma
+++ b/matita/contribs/LOGIC/Insert/props.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Insert/props".
+
 
 (*
 *)
diff --git a/matita/contribs/LOGIC/Lift/defs.ma b/matita/contribs/LOGIC/Lift/defs.ma
index f770bcf8d..86d588e3e 100644
--- a/matita/contribs/LOGIC/Lift/defs.ma
+++ b/matita/contribs/LOGIC/Lift/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Lift/defs".
+
 
 (* PROOF RELOCATION
 *)
diff --git a/matita/contribs/LOGIC/NTrack/defs.ma b/matita/contribs/LOGIC/NTrack/defs.ma
index 1bf18389f..15560f19c 100644
--- a/matita/contribs/LOGIC/NTrack/defs.ma
+++ b/matita/contribs/LOGIC/NTrack/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/NTrack/defs".
+
 
 (* NORMAL PROOF TREE TRACKS
 *)
diff --git a/matita/contribs/LOGIC/NTrack/inv.ma b/matita/contribs/LOGIC/NTrack/inv.ma
index f272bd518..68e7d7b1f 100644
--- a/matita/contribs/LOGIC/NTrack/inv.ma
+++ b/matita/contribs/LOGIC/NTrack/inv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/NTrack/inv".
+
 
 include "NTrack/defs.ma".
 (*
diff --git a/matita/contribs/LOGIC/NTrack/order.ma b/matita/contribs/LOGIC/NTrack/order.ma
index 11868b6ef..d136c47ba 100644
--- a/matita/contribs/LOGIC/NTrack/order.ma
+++ b/matita/contribs/LOGIC/NTrack/order.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/NTrack/order".
+
 
 include "Track/order.ma".
 include "NTrack/props.ma".
diff --git a/matita/contribs/LOGIC/NTrack/props.ma b/matita/contribs/LOGIC/NTrack/props.ma
index bdd23748f..3fdd5de61 100644
--- a/matita/contribs/LOGIC/NTrack/props.ma
+++ b/matita/contribs/LOGIC/NTrack/props.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/NTrack/props".
+
 
 include "Insert/props.ma".
 include "Track/defs.ma".
diff --git a/matita/contribs/LOGIC/PEq/defs.ma b/matita/contribs/LOGIC/PEq/defs.ma
index 1ffe5b20b..ec6b29679 100644
--- a/matita/contribs/LOGIC/PEq/defs.ma
+++ b/matita/contribs/LOGIC/PEq/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/PEq/defs".
+
 
 (* EQUALITY PREDICATE FOR PROOFS IN CONTEXT
 *)
diff --git a/matita/contribs/LOGIC/PNF/defs.ma b/matita/contribs/LOGIC/PNF/defs.ma
index 4f11e8c56..77fe6d577 100644
--- a/matita/contribs/LOGIC/PNF/defs.ma
+++ b/matita/contribs/LOGIC/PNF/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/PNF/defs".
+
 
 (* NORMAL FORM PREDICATE FOR PROOFS IN CONTEXT
    For cut elimination
diff --git a/matita/contribs/LOGIC/PRed/defs.ma b/matita/contribs/LOGIC/PRed/defs.ma
index 85a4c3bf9..bee77f1ed 100644
--- a/matita/contribs/LOGIC/PRed/defs.ma
+++ b/matita/contribs/LOGIC/PRed/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/PRed/defs".
+
 
 (* SINGLE STEP PARALLEL REDUCTION
    For cut elimination 
diff --git a/matita/contribs/LOGIC/PRed/wlt.ma b/matita/contribs/LOGIC/PRed/wlt.ma
index 3e7d727ed..c48cfb078 100644
--- a/matita/contribs/LOGIC/PRed/wlt.ma
+++ b/matita/contribs/LOGIC/PRed/wlt.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/PRed/wlt".
+
 
 (**)
 
diff --git a/matita/contribs/LOGIC/Track/defs.ma b/matita/contribs/LOGIC/Track/defs.ma
index 25cf7c0b5..e3779f837 100644
--- a/matita/contribs/LOGIC/Track/defs.ma
+++ b/matita/contribs/LOGIC/Track/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Track/defs".
+
 
 (* PROOF TREE TRACKS
 *)
diff --git a/matita/contribs/LOGIC/Track/inv.ma b/matita/contribs/LOGIC/Track/inv.ma
index d38d3f120..51935b4e0 100644
--- a/matita/contribs/LOGIC/Track/inv.ma
+++ b/matita/contribs/LOGIC/Track/inv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Track/inv".
+
 
 include "Track/defs.ma".
 
diff --git a/matita/contribs/LOGIC/Track/order.ma b/matita/contribs/LOGIC/Track/order.ma
index 2c90f3303..934632cd4 100644
--- a/matita/contribs/LOGIC/Track/order.ma
+++ b/matita/contribs/LOGIC/Track/order.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Track/order".
+
 
 include "Insert/fun.ma".
 include "Track/defs.ma".
diff --git a/matita/contribs/LOGIC/Track/pred.ma b/matita/contribs/LOGIC/Track/pred.ma
index cce6c7800..7cf152b94 100644
--- a/matita/contribs/LOGIC/Track/pred.ma
+++ b/matita/contribs/LOGIC/Track/pred.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Track/pred".
+
 
 (**)
 
diff --git a/matita/contribs/LOGIC/WLT/defs.ma b/matita/contribs/LOGIC/WLT/defs.ma
index 5a844a60a..8d1b7abdc 100644
--- a/matita/contribs/LOGIC/WLT/defs.ma
+++ b/matita/contribs/LOGIC/WLT/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/WLT/defs".
+
 
 (* ORDER RELATION BETWEEN PROOFS IN CONTEXT
 *)
diff --git a/matita/contribs/LOGIC/Weight/defs.ma b/matita/contribs/LOGIC/Weight/defs.ma
index 5dfcdde5c..7e6439363 100644
--- a/matita/contribs/LOGIC/Weight/defs.ma
+++ b/matita/contribs/LOGIC/Weight/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/Weight/defs".
+
 
 (* PROOF WEIGHT
    For cut elimination and confluence
diff --git a/matita/contribs/LOGIC/datatypes_defs/Context.ma b/matita/contribs/LOGIC/datatypes_defs/Context.ma
index e5dba4aaf..60c38f70c 100644
--- a/matita/contribs/LOGIC/datatypes_defs/Context.ma
+++ b/matita/contribs/LOGIC/datatypes_defs/Context.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Context".
+
 
 (* FLAT CONTEXTS
    - Naming policy:
diff --git a/matita/contribs/LOGIC/datatypes_defs/Formula.ma b/matita/contribs/LOGIC/datatypes_defs/Formula.ma
index ec6441dd1..8943bdaf9 100644
--- a/matita/contribs/LOGIC/datatypes_defs/Formula.ma
+++ b/matita/contribs/LOGIC/datatypes_defs/Formula.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Formula".
+
 
 (* FORMULAE
    - Naming policy:
diff --git a/matita/contribs/LOGIC/datatypes_defs/Proof.ma b/matita/contribs/LOGIC/datatypes_defs/Proof.ma
index fa2c29ffa..212f99ec9 100644
--- a/matita/contribs/LOGIC/datatypes_defs/Proof.ma
+++ b/matita/contribs/LOGIC/datatypes_defs/Proof.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Proof".
+
 
 (* PROOFS
    - Naming policy:
diff --git a/matita/contribs/LOGIC/datatypes_defs/Sequent.ma b/matita/contribs/LOGIC/datatypes_defs/Sequent.ma
index 09d826991..cc06ccb5d 100644
--- a/matita/contribs/LOGIC/datatypes_defs/Sequent.ma
+++ b/matita/contribs/LOGIC/datatypes_defs/Sequent.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Sequent".
+
 
 (* SEQUENTS
    - Naming policy:
diff --git a/matita/contribs/LOGIC/datatypes_props/Sequent.ma b/matita/contribs/LOGIC/datatypes_props/Sequent.ma
index f7c44a81f..335a10bf3 100644
--- a/matita/contribs/LOGIC/datatypes_props/Sequent.ma
+++ b/matita/contribs/LOGIC/datatypes_props/Sequent.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LOGIC/datatypes_props/Sequent".
+
 
 include "datatypes_defs/Sequent.ma".
 
diff --git a/matita/contribs/LOGIC/depends b/matita/contribs/LOGIC/depends
new file mode 100644
index 000000000..aabbf8f9c
--- /dev/null
+++ b/matita/contribs/LOGIC/depends
@@ -0,0 +1,27 @@
+preamble.ma NLE/defs.ma
+Insert/props.ma Insert/fun.ma
+Insert/inv.ma Insert/defs.ma
+Insert/defs.ma Lift/defs.ma datatypes_defs/Context.ma
+Insert/fun.ma CLE/defs.ma Insert/inv.ma
+datatypes_defs/Context.ma datatypes_defs/Proof.ma datatypes_defs/Sequent.ma
+datatypes_defs/Sequent.ma datatypes_defs/Formula.ma
+datatypes_defs/Proof.ma preamble.ma
+datatypes_defs/Formula.ma preamble.ma
+PRed/wlt.ma PEq/defs.ma PRed/defs.ma WLT/defs.ma
+PRed/defs.ma Insert/defs.ma
+Track/inv.ma Track/defs.ma
+Track/pred.ma PRed/defs.ma Track/inv.ma datatypes_props/Sequent.ma
+Track/defs.ma Insert/defs.ma
+Track/order.ma Insert/fun.ma Track/defs.ma
+Lift/defs.ma datatypes_defs/Proof.ma
+PNF/defs.ma PEq/defs.ma PRed/defs.ma
+datatypes_props/Sequent.ma datatypes_defs/Sequent.ma
+Weight/defs.ma datatypes_defs/Context.ma
+CLE/defs.ma datatypes_defs/Context.ma
+NTrack/props.ma Insert/props.ma NTrack/inv.ma Track/defs.ma
+NTrack/inv.ma NTrack/defs.ma
+NTrack/defs.ma Insert/defs.ma
+NTrack/order.ma NTrack/props.ma Track/order.ma
+PEq/defs.ma datatypes_defs/Context.ma
+WLT/defs.ma Weight/defs.ma
+NLE/defs.ma 
diff --git a/matita/contribs/LOGIC/makefile b/matita/contribs/LOGIC/makefile
deleted file mode 100644
index e5ac91fc8..000000000
--- a/matita/contribs/LOGIC/makefile
+++ /dev/null
@@ -1,39 +0,0 @@
-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) $(@:.opt=)
-	
-preall:
-	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
-
-preall.opt:
-	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)
diff --git a/matita/contribs/LOGIC/preamble.ma b/matita/contribs/LOGIC/preamble.ma
index b1e50f811..8aa350f69 100644
--- a/matita/contribs/LOGIC/preamble.ma
+++ b/matita/contribs/LOGIC/preamble.ma
@@ -14,9 +14,9 @@
 
 (* Project started Sat Apr 7, 2007 ****************************************)
 
-set "baseuri" "cic:/matita/LOGIC/preamble".
+
 
 (* PREAMBLE
 *)
 
-include "../RELATIONAL/NLE/defs.ma".
+include "NLE/defs.ma".
diff --git a/matita/contribs/LOGIC/root b/matita/contribs/LOGIC/root
new file mode 100644
index 000000000..33cc9a789
--- /dev/null
+++ b/matita/contribs/LOGIC/root
@@ -0,0 +1,2 @@
+baseuri=cic:/matita/LOGIC
+include_paths= ../RELATIONAL
diff --git a/matita/contribs/RELATIONAL/NLE/defs.ma b/matita/contribs/RELATIONAL/NLE/defs.ma
index 18fc87b10..535b717aa 100644
--- a/matita/contribs/RELATIONAL/NLE/defs.ma
+++ b/matita/contribs/RELATIONAL/NLE/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NLE/defs".
+
 
 include "NPlus/defs.ma".
 
diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma
index 013cd67f1..af2fa812b 100644
--- a/matita/contribs/RELATIONAL/NLE/inv.ma
+++ b/matita/contribs/RELATIONAL/NLE/inv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NLE/inv".
+
 
 include "NLE/defs.ma".
 
diff --git a/matita/contribs/RELATIONAL/NLE/nplus.ma b/matita/contribs/RELATIONAL/NLE/nplus.ma
index d90adb926..85dac01a9 100644
--- a/matita/contribs/RELATIONAL/NLE/nplus.ma
+++ b/matita/contribs/RELATIONAL/NLE/nplus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NLE/nplus".
+
 
 include "NLE/defs.ma".
 
diff --git a/matita/contribs/RELATIONAL/NLE/order.ma b/matita/contribs/RELATIONAL/NLE/order.ma
index cc3cc3030..6918bbc0f 100644
--- a/matita/contribs/RELATIONAL/NLE/order.ma
+++ b/matita/contribs/RELATIONAL/NLE/order.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NLE/order".
+
 
 include "NLE/inv.ma".
 
diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma
index 576a079ae..1eb0455fe 100644
--- a/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/matita/contribs/RELATIONAL/NLE/props.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
+
 
 include "NLE/order.ma".
 
diff --git a/matita/contribs/RELATIONAL/NPlus/defs.ma b/matita/contribs/RELATIONAL/NPlus/defs.ma
index 8d8b304c3..34f4e3491 100644
--- a/matita/contribs/RELATIONAL/NPlus/defs.ma
+++ b/matita/contribs/RELATIONAL/NPlus/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs".
+
 
 include "datatypes/Nat.ma".
 
diff --git a/matita/contribs/RELATIONAL/NPlus/fun.ma b/matita/contribs/RELATIONAL/NPlus/fun.ma
index 03dd7d0ef..271a7c6e4 100644
--- a/matita/contribs/RELATIONAL/NPlus/fun.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fun.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NPlus/fun".
+
 
 include "NPlus/inv.ma".
 
diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma
index b6ac60873..e3ec16898 100644
--- a/matita/contribs/RELATIONAL/NPlus/inv.ma
+++ b/matita/contribs/RELATIONAL/NPlus/inv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NPlus/inv".
+
 
 include "NPlus/defs.ma".
 
diff --git a/matita/contribs/RELATIONAL/NPlus/monoid.ma b/matita/contribs/RELATIONAL/NPlus/monoid.ma
index a521c9a1d..7fc798878 100644
--- a/matita/contribs/RELATIONAL/NPlus/monoid.ma
+++ b/matita/contribs/RELATIONAL/NPlus/monoid.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NPlus/monoid".
+
 
 include "NPlus/fun.ma".
 
diff --git a/matita/contribs/RELATIONAL/NPlusList/defs.ma b/matita/contribs/RELATIONAL/NPlusList/defs.ma
index 86d023165..cac07f91a 100644
--- a/matita/contribs/RELATIONAL/NPlusList/defs.ma
+++ b/matita/contribs/RELATIONAL/NPlusList/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NPlusList/defs".
+
 
 include "datatypes/List.ma".
 include "NPlus/defs.ma".
diff --git a/matita/contribs/RELATIONAL/NPlusList/props.ma b/matita/contribs/RELATIONAL/NPlusList/props.ma
index f7fc4305e..4b70088a2 100644
--- a/matita/contribs/RELATIONAL/NPlusList/props.ma
+++ b/matita/contribs/RELATIONAL/NPlusList/props.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NPlusList/props".
+
 
 include "NPlusList/defs.ma".
 (*
diff --git a/matita/contribs/RELATIONAL/ZEq/defs.ma b/matita/contribs/RELATIONAL/ZEq/defs.ma
index 6d270cab3..91beaef0e 100644
--- a/matita/contribs/RELATIONAL/ZEq/defs.ma
+++ b/matita/contribs/RELATIONAL/ZEq/defs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/ZEq/defs".
+
 
 include "datatypes/Zah.ma".
 include "NPlus/defs.ma".
diff --git a/matita/contribs/RELATIONAL/ZEq/setoid.ma b/matita/contribs/RELATIONAL/ZEq/setoid.ma
index 37ca8f619..587470bfc 100644
--- a/matita/contribs/RELATIONAL/ZEq/setoid.ma
+++ b/matita/contribs/RELATIONAL/ZEq/setoid.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/ZEq/setoid".
+
 
 include "NPlus/fun.ma".
 include "ZEq/defs.ma".
diff --git a/matita/contribs/RELATIONAL/datatypes/Bool.ma b/matita/contribs/RELATIONAL/datatypes/Bool.ma
index 58345281b..970d6694c 100644
--- a/matita/contribs/RELATIONAL/datatypes/Bool.ma
+++ b/matita/contribs/RELATIONAL/datatypes/Bool.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/datatypes/Bool".
+
 
 include "preamble.ma".
 
diff --git a/matita/contribs/RELATIONAL/datatypes/List.ma b/matita/contribs/RELATIONAL/datatypes/List.ma
index 313362e5d..b8abed54d 100644
--- a/matita/contribs/RELATIONAL/datatypes/List.ma
+++ b/matita/contribs/RELATIONAL/datatypes/List.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/datatypes/List".
+
 
 include "preamble.ma".
 
diff --git a/matita/contribs/RELATIONAL/datatypes/Nat.ma b/matita/contribs/RELATIONAL/datatypes/Nat.ma
index 75a3c58d3..ed45a35fe 100644
--- a/matita/contribs/RELATIONAL/datatypes/Nat.ma
+++ b/matita/contribs/RELATIONAL/datatypes/Nat.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/datatypes/Nat".
+
 
 include "preamble.ma".
 
diff --git a/matita/contribs/RELATIONAL/datatypes/Zah.ma b/matita/contribs/RELATIONAL/datatypes/Zah.ma
index 87f61d7d1..45ce72c56 100644
--- a/matita/contribs/RELATIONAL/datatypes/Zah.ma
+++ b/matita/contribs/RELATIONAL/datatypes/Zah.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/datatypes/Zah".
+
 
 include "datatypes/Nat.ma".
 
diff --git a/matita/contribs/RELATIONAL/depends b/matita/contribs/RELATIONAL/depends
new file mode 100644
index 000000000..9d79219ac
--- /dev/null
+++ b/matita/contribs/RELATIONAL/depends
@@ -0,0 +1,21 @@
+preamble.ma datatypes/constructors.ma logic/connectives.ma logic/equality.ma
+datatypes/Nat.ma preamble.ma
+datatypes/Zah.ma datatypes/Nat.ma
+datatypes/List.ma preamble.ma
+datatypes/Bool.ma preamble.ma
+ZEq/setoid.ma NPlus/fun.ma ZEq/defs.ma
+ZEq/defs.ma NPlus/defs.ma datatypes/Zah.ma
+NLE/nplus.ma NLE/defs.ma
+NLE/props.ma NLE/order.ma
+NLE/inv.ma NLE/defs.ma
+NLE/defs.ma NPlus/defs.ma datatypes/Nat.ma
+NLE/order.ma NLE/inv.ma
+NPlusList/props.ma NPlusList/defs.ma
+NPlusList/defs.ma NPlus/defs.ma datatypes/List.ma
+NPlus/inv.ma NPlus/defs.ma
+NPlus/monoid.ma NPlus/fun.ma
+NPlus/defs.ma datatypes/Nat.ma
+NPlus/fun.ma NPlus/inv.ma
+datatypes/constructors.ma 
+logic/connectives.ma 
+logic/equality.ma 
diff --git a/matita/contribs/RELATIONAL/makefile b/matita/contribs/RELATIONAL/makefile
deleted file mode 100644
index e5ac91fc8..000000000
--- a/matita/contribs/RELATIONAL/makefile
+++ /dev/null
@@ -1,39 +0,0 @@
-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) $(@:.opt=)
-	
-preall:
-	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
-
-preall.opt:
-	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)
diff --git a/matita/contribs/RELATIONAL/preamble.ma b/matita/contribs/RELATIONAL/preamble.ma
index d52da9701..e030ad1ad 100644
--- a/matita/contribs/RELATIONAL/preamble.ma
+++ b/matita/contribs/RELATIONAL/preamble.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/preamble".
+
 
 include "logic/equality.ma".
 include "logic/connectives.ma".
diff --git a/matita/contribs/RELATIONAL/root b/matita/contribs/RELATIONAL/root
new file mode 100644
index 000000000..eadc56b03
--- /dev/null
+++ b/matita/contribs/RELATIONAL/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/RELATIONAL