From 92e53212b1142355777f171bf683066f52135ed7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Jan 2008 13:10:27 +0000 Subject: [PATCH] ported to the new make system --- matita/contribs/LOGIC/CLE/defs.ma | 2 +- matita/contribs/LOGIC/Insert/defs.ma | 2 +- matita/contribs/LOGIC/Insert/fun.ma | 2 +- matita/contribs/LOGIC/Insert/inv.ma | 2 +- matita/contribs/LOGIC/Insert/props.ma | 2 +- matita/contribs/LOGIC/Lift/defs.ma | 2 +- matita/contribs/LOGIC/NTrack/defs.ma | 2 +- matita/contribs/LOGIC/NTrack/inv.ma | 2 +- matita/contribs/LOGIC/NTrack/order.ma | 2 +- matita/contribs/LOGIC/NTrack/props.ma | 2 +- matita/contribs/LOGIC/PEq/defs.ma | 2 +- matita/contribs/LOGIC/PNF/defs.ma | 2 +- matita/contribs/LOGIC/PRed/defs.ma | 2 +- matita/contribs/LOGIC/PRed/wlt.ma | 2 +- matita/contribs/LOGIC/Track/defs.ma | 2 +- matita/contribs/LOGIC/Track/inv.ma | 2 +- matita/contribs/LOGIC/Track/order.ma | 2 +- matita/contribs/LOGIC/Track/pred.ma | 2 +- matita/contribs/LOGIC/WLT/defs.ma | 2 +- matita/contribs/LOGIC/Weight/defs.ma | 2 +- .../contribs/LOGIC/datatypes_defs/Context.ma | 2 +- .../contribs/LOGIC/datatypes_defs/Formula.ma | 2 +- matita/contribs/LOGIC/datatypes_defs/Proof.ma | 2 +- .../contribs/LOGIC/datatypes_defs/Sequent.ma | 2 +- .../contribs/LOGIC/datatypes_props/Sequent.ma | 2 +- matita/contribs/LOGIC/depends | 27 +++++++++++++ matita/contribs/LOGIC/makefile | 39 ------------------- matita/contribs/LOGIC/preamble.ma | 4 +- matita/contribs/LOGIC/root | 2 + matita/contribs/RELATIONAL/NLE/defs.ma | 2 +- matita/contribs/RELATIONAL/NLE/inv.ma | 2 +- matita/contribs/RELATIONAL/NLE/nplus.ma | 2 +- matita/contribs/RELATIONAL/NLE/order.ma | 2 +- matita/contribs/RELATIONAL/NLE/props.ma | 2 +- matita/contribs/RELATIONAL/NPlus/defs.ma | 2 +- matita/contribs/RELATIONAL/NPlus/fun.ma | 2 +- matita/contribs/RELATIONAL/NPlus/inv.ma | 2 +- matita/contribs/RELATIONAL/NPlus/monoid.ma | 2 +- matita/contribs/RELATIONAL/NPlusList/defs.ma | 2 +- matita/contribs/RELATIONAL/NPlusList/props.ma | 2 +- matita/contribs/RELATIONAL/ZEq/defs.ma | 2 +- matita/contribs/RELATIONAL/ZEq/setoid.ma | 2 +- matita/contribs/RELATIONAL/datatypes/Bool.ma | 2 +- matita/contribs/RELATIONAL/datatypes/List.ma | 2 +- matita/contribs/RELATIONAL/datatypes/Nat.ma | 2 +- matita/contribs/RELATIONAL/datatypes/Zah.ma | 2 +- matita/contribs/RELATIONAL/depends | 21 ++++++++++ matita/contribs/RELATIONAL/makefile | 39 ------------------- matita/contribs/RELATIONAL/preamble.ma | 2 +- matita/contribs/RELATIONAL/root | 1 + 50 files changed, 96 insertions(+), 123 deletions(-) create mode 100644 matita/contribs/LOGIC/depends delete mode 100644 matita/contribs/LOGIC/makefile create mode 100644 matita/contribs/LOGIC/root create mode 100644 matita/contribs/RELATIONAL/depends delete mode 100644 matita/contribs/RELATIONAL/makefile create mode 100644 matita/contribs/RELATIONAL/root 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 -- 2.39.2