ported to the new make system

diff --git a/matita/contribs/LOGIC/CLE/defs.ma b/matita/contribs/LOGIC/CLE/defs.ma
index 5b3ba49b73d05e932e7b8ef26bb0492184e982da..03065ada0ccc7a8bfd6fa3cf148969561896de9e 100644 (file)
--- 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 821fd99c2170038c991861b5f664e32a67d48235..c3109a5f67c2792b77c8a408f8985f41cf615d54 100644 (file)
--- 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 7c7aba28a8eaa4e0ca9c44ae1becf26b7343e662..d06a7e29cfdb975221a1c72402abfe7dc6360de3 100644 (file)
--- 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 9053183f969ab3f25f78849be9adb553d916111a..df5ca04f32d6a2534207bea61361f96245dfb9b4 100644 (file)
--- 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 17148e27e38b71b83add4bbacb080d71be5238c8..3289e68a7ad98e6b60aad4e1fe5149c20e49d716 100644 (file)
--- 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 f770bcf8d90d200a9e3c0f7fe07ae8d0e7be3fb6..86d588e3eaabf35095b3e2839761e9f3c4eb2374 100644 (file)
--- 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 1bf18389f3c5ba30915965fbd52aa9e565250829..15560f19c1417607fab0cf3b30d4ca9159a9f573 100644 (file)
--- 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 f272bd5181cabf71a8bad948c362964a3bdece41..68e7d7b1ff39a0f70e91cf1f5555a846e409c257 100644 (file)
--- 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 11868b6ef65f29863125f95f6fbae27f9d90f09a..d136c47ba48f6da1827f017f1ae0769c417ea733 100644 (file)
--- 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 bdd23748faf16e6dae4294381bafbd8a8b07388e..3fdd5de618fa0f1aadcdfaa115abf5671a29621b 100644 (file)
--- 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 1ffe5b20b5dc8259ccebeaffcf2094de31c7f71b..ec6b296799cb1aa052d7567e26a508b276ed6ab2 100644 (file)
--- 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 4f11e8c561cfd1e844641a6741bbf5801e40f2ab..77fe6d5771f812793dbaad6d1194cba72febd459 100644 (file)
--- 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 85a4c3bf9af0512e4ef7599cf0cdaeda1b00ac9b..bee77f1ede68af5d01e99ce4463eedaa7235c2ab 100644 (file)
--- 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 3e7d727edc3c1a6c17fd0ff3909057a0830eb824..c48cfb0789611314d5965a2a5894e7962dcf7491 100644 (file)
--- 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 25cf7c0b5fa2bfbc37d9e8d1e8b6df6cf1d1b240..e3779f8376676bcd3a1a6542cb06246d9ec3c9db 100644 (file)
--- 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 d38d3f120ca6fea326884866dc2fd7c326f1e68d..51935b4e003accf4c4ef5f964849c61ae6d016ac 100644 (file)
--- 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 2c90f33037b2dbb2f3ef1e95854f2bd3ad1395b7..934632cd45f1907280dd3679332a380981e64252 100644 (file)
--- 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 cce6c7800e88d1d24e5c8cff4d12f5d80580317b..7cf152b9473790ae6d2b5449b94daa71af69fdb5 100644 (file)
--- 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 5a844a60adfc098697dd1eea7bf7bd34ee2c9588..8d1b7abdce1b3a5d439b032c0dddc54481e44b6b 100644 (file)
--- 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 5dfcdde5cb1967b492ff83cec1758992f7b430da..7e6439363ec44a6d51a15dad91c5bbea80341915 100644 (file)
--- 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 e5dba4aafa30651ce17480d0a3e8c141154db757..60c38f70c8bb73742f796553ad2123ee0bd8eed5 100644 (file)
--- 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 ec6441dd18cbd5428ac444c680e21f7962262a7b..8943bdaf9d134a0d80d633b77d175d9b3cf9f898 100644 (file)
--- 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 fa2c29ffa6106304b749f1b4a2f5ead00c00dcf2..212f99ec960eb211c8f8b17f821ba883361142b1 100644 (file)
--- 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 09d8269912c6c9fb824c137e8f1efccc20421977..cc06ccb5d5f99ce6d63291c07c24b94bcbbd7d42 100644 (file)
--- 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 f7c44a81fd8ea9bdb0a6a5efc144a8777ea00c9a..335a10bf3ce1f03887f547143bd3280f8ae25f63 100644 (file)
--- 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 (file)
index 0000000..aabbf8f
--- /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 (file)
index e5ac91f..0000000
--- 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 b1e50f8118873ee1e2b2d1b39dcd66e057c45cb8..8aa350f69788741be683c50b1be28df662140c1e 100644 (file)
--- 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 (file)
index 0000000..33cc9a7
--- /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 18fc87b107ddc038b0b997322d0a9a5501283239..535b717aa21326eab8fa99d72316df68ff92c780 100644 (file)
--- 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 013cd67f1d936476f690528b58d934ea24d82e30..af2fa812bd058a3c9582c7122fd6a1e8161b4573 100644 (file)
--- 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 d90adb92627ddcc8bdb08c939b30d8a802bb3421..85dac01a9d92e62cfaf0becd52797ef3878875df 100644 (file)
--- 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 cc3cc3030a44cdf3b4065ada67e42480791ce13f..6918bbc0f95ad6610a93b4e8896382c9712b385d 100644 (file)
--- 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 576a079ae3cb6ae70e44aa60b1fdad08f5222423..1eb0455fe94ca8d5da93f32be17d397275e71cc7 100644 (file)
--- 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 8d8b304c3afce2eb1d9aa75c68b0c59a3cdae2e7..34f4e3491eba32b2d3620690eda0ebf2e4a8d300 100644 (file)
--- 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 03dd7d0efd17551928787b915277bf7294adf7bc..271a7c6e475949614872175a546473b7fefbcebd 100644 (file)
--- 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 b6ac60873ae2788f95fa9569a754f9949319b913..e3ec16898e0766f2a041eab6fcaed38a525bb4c2 100644 (file)
--- 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 a521c9a1dfef29b49f0176f484f0bf4e9eac3383..7fc7988780c1602ed606c7ed159f365070abec56 100644 (file)
--- 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 86d0231658bb79eeff322fe445371cc21beba156..cac07f91a523315ec6d0fe53976ab3abe00188a6 100644 (file)
--- 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 f7fc4305e4a8ce2457230bcb96d56e21669e4e5f..4b70088a2fc54490727ec53677c9d5576dc4a0e3 100644 (file)
--- 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 6d270cab31bd6ff42c26c216260386b7b5ccccea..91beaef0e237d5fd721e90fed5b4b7149ea2fd55 100644 (file)
--- 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 37ca8f6199ae6ef81a83f1832ef06a1c1c8c7057..587470bfc70f9af0374199523a390485589f7f4d 100644 (file)
--- 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 58345281b538793a30aa6b7e7a1789ca941bf671..970d6694c997582627e311474a887931d71f8e45 100644 (file)
--- 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 313362e5d90c55f5c604107e6714f416364178a5..b8abed54d847e7dd12ac3f5b79fcbd2c9e5f0bd3 100644 (file)
--- 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 75a3c58d368083e3ebac90a786b29bc093b6fe38..ed45a35feb2d3ce46481002f614f42a42d7cd7c2 100644 (file)
--- 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 87f61d7d1762d97471a0d73867d84ea60746fe78..45ce72c56284db122ba587c05ef978228b87fd22 100644 (file)
--- 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 (file)
index 0000000..9d79219
--- /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 (file)
index e5ac91f..0000000
--- 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 d52da97017d54775de591a7d91acb3ecebac11c4..e030ad1ad550c32dace1830a720f3f75b1ba17aa 100644 (file)
--- 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 (file)
index 0000000..eadc56b
--- /dev/null
+++ b/matita/contribs/RELATIONAL/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/RELATIONAL