legacy development created

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index ab03a892f002094e57d0169af7a0dfe932ef08a9..fd96cc5f99d7ebd4cf2ba79d9c411731ae073f77 100644 (file)
--- 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 6ea5e41b0e29d08b2882ad653d4241b32a14c21f..9d7d5533ae2f7dfd9559936d97aa87f91b3e3f67 100644 (file)
--- 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 b4c69f299f366435e7fbad576a9d2c8437580691..6a41598bbfd72c017d69cb3cfc17c4ba6e69a411 100644 (file)
--- 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 (file)
index 0000000..4d50449
--- /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/legacy/coq.ma b/helm/software/matita/legacy/coq.ma
new file mode 100644 (file)
index 0000000..9860c63
--- /dev/null
+++ b/helm/software/matita/legacy/coq.ma
@@ -0,0 +1,90 @@
+(**************************************************************************)
+(*       ___                                                             *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/legacy/coq/".
+
+default "equality"
+ cic:/Coq/Init/Logic/eq.ind
+ cic:/Coq/Init/Logic/sym_eq.con
+ cic:/Coq/Init/Logic/trans_eq.con
+ cic:/Coq/Init/Logic/eq_ind.con
+ cic:/Coq/Init/Logic/eq_ind_r.con
+ cic:/Coq/Init/Logic/f_equal.con
+ cic:/matita/legacy/coq/f_equal1.con.
+
+default "true"
+ cic:/Coq/Init/Logic/True.ind. 
+default "false"
+ cic:/Coq/Init/Logic/False.ind. 
+default "absurd"
+ cic:/Coq/Init/Logic/absurd.con. 
+
+(* aritmetic operators *)
+
+interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
+interpretation "Coq's real plus" 'plus x y = (cic:/Coq/Reals/Rdefinitions/Rplus.con x y).
+interpretation "Coq's binary integer plus" 'plus x y = (cic:/Coq/ZArith/BinInt/Zplus.con x y).
+interpretation "Coq's binary positive plus" 'plus x y = (cic:/Coq/NArith/BinPos/Pplus.con x y).
+interpretation "Coq's natural minus" 'minus x y = (cic:/Coq/Init/Peano/minus.con x y).
+interpretation "Coq's real minus" 'minus x y = (cic:/Coq/Reals/Rdefinitions/Rminus.con x y).
+interpretation "Coq's binary integer minus" 'minus x y = (cic:/Coq/ZArith/BinInt/Zminus.con x y).
+interpretation "Coq's binary positive minus" 'minus x y = (cic:/Coq/NArith/BinPos/Pminus.con x y).
+interpretation "Coq's natural times" 'times x y = (cic:/Coq/Init/Peano/mult.con x y).
+interpretation "Coq's real times" 'times x y = (cic:/Coq/Reals/Rdefinitions/Rmult.con x y).
+interpretation "Coq's binary positive times" 'times x y = (cic:/Coq/NArith/BinPos/Pmult.con x y).
+interpretation "Coq's binary integer times" 'times x y = (cic:/Coq/ZArith/BinInt/Zmult.con x y).
+interpretation "Coq's real power" 'power x y = (cic:/Coq/Reals/Rfunctions/pow.con x y).
+interpretation "Coq's integer power" 'power x y = (cic:/Coq/ZArith/Zpower/Zpower.con x y).
+interpretation "Coq's real divide" 'divide x y = (cic:/Coq/Reals/Rdefinitions/Rdiv.con x y).
+interpretation "Coq's real unary minus" 'uminus x = (cic:/Coq/Reals/Rdefinitions/Ropp.con x).
+interpretation "Coq's binary integer negative sign" 'uminus x = (cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/3) x).
+interpretation "Coq's binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/Zopp.con x).
+
+(* logical operators *)
+
+interpretation "Coq's logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y).
+interpretation "Coq's logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y).
+interpretation "Coq's logical not" 'not x = (cic:/Coq/Init/Logic/not.con x).
+interpretation "Coq's exists" 'exists \eta.x = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) _ x).
+
+(* relational operators *)
+
+interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
+interpretation "Coq's real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
+interpretation "Coq's natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
+interpretation "Coq's real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).
+interpretation "Coq's natural 'less than'" 'lt x y = (cic:/Coq/Init/Peano/lt.con x y).
+interpretation "Coq's real 'less than'" 'lt x y = (cic:/Coq/Reals/Rdefinitions/Rlt.con x y).
+interpretation "Coq's natural 'greater than'" 'gt x y = (cic:/Coq/Init/Peano/gt.con x y).
+interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinitions/Rgt.con x y).
+
+interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
+interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
+
+interpretation "Coq's natural 'not less or equal than'"
+ 'nleq x y = (cic:/Coq/Init/Logic/not.con 
+               (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)).
+               
+theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A.
+  x = y \to (f y) = (f x).
+  intros.
+  symmetry.
+  apply cic:/Coq/Init/Logic/f_equal.con.
+  assumption.
+qed.
+(* aliases *)
+
+(* 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/legacy/makefile b/helm/software/matita/legacy/makefile
new file mode 100644 (file)
index 0000000..c4020f6
--- /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/legacy/coq.ma b/helm/software/matita/library/legacy/coq.ma
deleted file mode 100644 (file)
index 9860c63..0000000
--- a/helm/software/matita/library/legacy/coq.ma
+++ /dev/null
@@ -1,90 +0,0 @@
-(**************************************************************************)
-(*       ___                                                             *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
-(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU Lesser General Public License Version 2.1         *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/legacy/coq/".
-
-default "equality"
- cic:/Coq/Init/Logic/eq.ind
- cic:/Coq/Init/Logic/sym_eq.con
- cic:/Coq/Init/Logic/trans_eq.con
- cic:/Coq/Init/Logic/eq_ind.con
- cic:/Coq/Init/Logic/eq_ind_r.con
- cic:/Coq/Init/Logic/f_equal.con
- cic:/matita/legacy/coq/f_equal1.con.
-
-default "true"
- cic:/Coq/Init/Logic/True.ind. 
-default "false"
- cic:/Coq/Init/Logic/False.ind. 
-default "absurd"
- cic:/Coq/Init/Logic/absurd.con. 
-
-(* aritmetic operators *)
-
-interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
-interpretation "Coq's real plus" 'plus x y = (cic:/Coq/Reals/Rdefinitions/Rplus.con x y).
-interpretation "Coq's binary integer plus" 'plus x y = (cic:/Coq/ZArith/BinInt/Zplus.con x y).
-interpretation "Coq's binary positive plus" 'plus x y = (cic:/Coq/NArith/BinPos/Pplus.con x y).
-interpretation "Coq's natural minus" 'minus x y = (cic:/Coq/Init/Peano/minus.con x y).
-interpretation "Coq's real minus" 'minus x y = (cic:/Coq/Reals/Rdefinitions/Rminus.con x y).
-interpretation "Coq's binary integer minus" 'minus x y = (cic:/Coq/ZArith/BinInt/Zminus.con x y).
-interpretation "Coq's binary positive minus" 'minus x y = (cic:/Coq/NArith/BinPos/Pminus.con x y).
-interpretation "Coq's natural times" 'times x y = (cic:/Coq/Init/Peano/mult.con x y).
-interpretation "Coq's real times" 'times x y = (cic:/Coq/Reals/Rdefinitions/Rmult.con x y).
-interpretation "Coq's binary positive times" 'times x y = (cic:/Coq/NArith/BinPos/Pmult.con x y).
-interpretation "Coq's binary integer times" 'times x y = (cic:/Coq/ZArith/BinInt/Zmult.con x y).
-interpretation "Coq's real power" 'power x y = (cic:/Coq/Reals/Rfunctions/pow.con x y).
-interpretation "Coq's integer power" 'power x y = (cic:/Coq/ZArith/Zpower/Zpower.con x y).
-interpretation "Coq's real divide" 'divide x y = (cic:/Coq/Reals/Rdefinitions/Rdiv.con x y).
-interpretation "Coq's real unary minus" 'uminus x = (cic:/Coq/Reals/Rdefinitions/Ropp.con x).
-interpretation "Coq's binary integer negative sign" 'uminus x = (cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/3) x).
-interpretation "Coq's binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/Zopp.con x).
-
-(* logical operators *)
-
-interpretation "Coq's logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y).
-interpretation "Coq's logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y).
-interpretation "Coq's logical not" 'not x = (cic:/Coq/Init/Logic/not.con x).
-interpretation "Coq's exists" 'exists \eta.x = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) _ x).
-
-(* relational operators *)
-
-interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
-interpretation "Coq's real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
-interpretation "Coq's natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
-interpretation "Coq's real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).
-interpretation "Coq's natural 'less than'" 'lt x y = (cic:/Coq/Init/Peano/lt.con x y).
-interpretation "Coq's real 'less than'" 'lt x y = (cic:/Coq/Reals/Rdefinitions/Rlt.con x y).
-interpretation "Coq's natural 'greater than'" 'gt x y = (cic:/Coq/Init/Peano/gt.con x y).
-interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinitions/Rgt.con x y).
-
-interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
-interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
-
-interpretation "Coq's natural 'not less or equal than'"
- 'nleq x y = (cic:/Coq/Init/Logic/not.con 
-               (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)).
-               
-theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A.
-  x = y \to (f y) = (f x).
-  intros.
-  symmetry.
-  apply cic:/Coq/Init/Logic/f_equal.con.
-  assumption.
-qed.
-(* aliases *)
-
-(* 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/library/library_notation.ma b/helm/software/matita/library/library_notation.ma
index 475fe38f849ada0843463b40ad5b430590772676..f86396f1f8ccab3985403dc14a5ed0f0178bf2a6 100644 (file)
--- 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".