we are moving the devel root one dir level up

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/Makefile
deleted file mode 100644 (file)
index a57a728..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/Makefile
+++ /dev/null
@@ -1,15 +0,0 @@
-DIR=$(shell basename $$PWD)
-MATITAOPTIONS=-onepass
-
-$(DIR) all:
-       ../../../matitac $(MATITAOPTIONS)
-$(DIR).opt opt all.opt:
-       ../../../matitac.opt $(MATITAOPTIONS)
-clean:
-       ../../../matitaclean
-clean.opt:
-       ../../../matitaclean.opt
-depend:
-       ../../../matitadep
-depend.opt:
-       ../../../matitadep.opt

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma
index 293c184f57d3537be03dc1ca9bcd5c37dec3f365..660e1862663fa61050338099b821826ee447062b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-1/preamble.ma".
 
 definition blt:
  nat \to (nat \to bool)

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma
index 3cff54f9641d8fc1479bf110c698863afdda9dfb..751dcee9c59db4727038f5315f0b7f4269985b49 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "blt/defs.ma".
+include "Base-1/blt/defs.ma".
 
 theorem lt_blt:
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true)))

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma
index 3a087dec7d8e873cd62a4808bfbfaa7a8490d40d..79cc45e2806486b0be2f53bce7f7ca0dd8f05993 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "types/defs.ma".
+include "Base-1/types/defs.ma".
 
-include "blt/defs.ma".
+include "Base-1/blt/defs.ma".
 
-include "plist/defs.ma".
+include "Base-1/plist/defs.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/depends b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/depends
deleted file mode 100644 (file)
index 9bb223d..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/depends
+++ /dev/null
@@ -1,13 +0,0 @@
-definitions.ma blt/defs.ma plist/defs.ma types/defs.ma
-preamble.ma coq.ma
-theory.ma blt/props.ma ext/arith.ma ext/tactics.ma plist/props.ma types/props.ma
-spare.ma theory.ma
-plist/props.ma plist/defs.ma
-plist/defs.ma preamble.ma
-ext/tactics.ma preamble.ma
-ext/arith.ma preamble.ma
-types/props.ma types/defs.ma
-types/defs.ma preamble.ma
-blt/props.ma blt/defs.ma
-blt/defs.ma preamble.ma
-coq.ma 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
index 70a94bfbd44f30216d7bb222c9f01f68c4801b6b..0d0f2a5dfd98a69ce51bcd558054c3c24355eb53 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-1/preamble.ma".
 
 theorem nat_dec:
  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma
index 7fcdc28ec52c47786f5aee0ca9fef4a4aaf29db8..79551495d86e5e699ba5d1ef301cf0a87b74fbe1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-1/preamble.ma".
 
 theorem insert_eq:
  \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma
index 9cfca05ae3b1e206f4c112c67e9de110236fbb05..5cf9337e472f043b0ca2b07b23c9cd2981260556 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-1/preamble.ma".
 
 inductive PList: Set \def
 | PNil: PList

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma
index bc480cc23eb0716ea05a19d2b6ae19770fae0d0b..cfe98b20d8803d5e0456c917880c9674935d42c7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "plist/defs.ma".
+include "Base-1/plist/defs.ma".
 
 theorem papp_ss:
  \forall (is1: PList).(\forall (is2: PList).(eq PList (papp (Ss is1) (Ss 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/root b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/root
deleted file mode 100644 (file)
index 43a60f9..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/root
+++ /dev/null
@@ -1,2 +0,0 @@
-baseuri=cic:/matita/LAMBDA-TYPES/Base-1
-include_paths= ../../../legacy 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma
index c62e679824ff2d01011e2fad78c6e99add9f6e0f..024efedf4ceffb32a7f7a9f3713eaedcb1f8806a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma
@@ -14,5 +14,5 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "theory.ma".
+include "Base-1/theory.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma
index c7c94ce539a43165834ebba46ca7b7a1d5d9608b..3f643ffa1a83c031efba319c89f8e6376d67ec75 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "ext/tactics.ma".
+include "Base-1/ext/tactics.ma".
 
-include "ext/arith.ma".
+include "Base-1/ext/arith.ma".
 
-include "types/props.ma".
+include "Base-1/types/props.ma".
 
-include "blt/props.ma".
+include "Base-1/blt/props.ma".
 
-include "plist/props.ma".
+include "Base-1/plist/props.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
index cb8300ade4c2688b248238d720b59b9344212d7b..cddd83fd9d46b1a49dc249f3e40638fd354e850d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-1/preamble.ma".
 
 inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
 | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
@@ -92,6 +92,14 @@ Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 
 A1 A2 P0 P1 P2 P3))))))).
 
+inductive ex5_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to 
+Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to 
+Prop))): Prop \def
+| ex5_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
+x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to ((P4 x0 
+x1 x2) \to (ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)))))))).
+
 inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to 
 (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 
 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma
index b2766560065aad573f8620f82bacea0fad2275b2..d6f71f4a56de800026b26a4fb827bb7c3e0dc37e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "types/defs.ma".
+include "Base-1/types/defs.ma".
 
 theorem ex2_sym:
  \forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma
index 98bb97a68bdfa2518514f15391c1483ad992e225..1744bc2769d002b5dcc72b1b42365cdfa3140a03 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma
@@ -14,8 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-2/preamble.ma".
 
-
-(* object blt not inlined *)
+inline procedural "Base-1/blt/defs.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma
index 5dfa152eef6794a8fb1383fb4f61b1b21e8b746d..63b209e18a5cbd27819435fff3b2f061171104cb 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma
@@ -14,13 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "blt/defs.ma".
+include "Base-2/blt/defs.ma".
 
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/le_bge.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/blt_lt.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/bge_le.con".
+inline procedural "Base-1/blt/props.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma
index 4e73adbf7bbd024d921608441c51617f4faeaf6e..c2e685e6497fee9e28b8f7a2eed66027c7749254 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma
@@ -14,99 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-2/preamble.ma".
 
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_Sy.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_n_pred.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_O.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con".
+inline procedural "Base-1/ext/arith.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma
index e6b75198a10ac06cdecfb7368271cebcc501b28d..474b8722affa2c3d3be4513b7903639f987b9b28 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma
@@ -14,12 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-2/preamble.ma".
 
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con".
-
-inline procedural 
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.con".
+inline procedural "Base-1/ext/tactics.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma
index 4ae6d51568bb9027e06bcae22a25551428cf6e7a..b73b56faed8a1de53feb0b223e5ae3d5ce031b40 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma
@@ -14,17 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-2/preamble.ma".
 
-
-(* object PList not inlined *)
-
-
-(* object PConsTail not inlined *)
-
-
-(* object Ss not inlined *)
-
-
-(* object papp not inlined *)
+inline procedural "Base-1/plist/defs.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma
index 130dee88cd425695b4defef724f738b2ff6276fc..9e21e540ae949ae57b4da1dc773307bfe683202e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "plist/defs.ma".
+include "Base-2/plist/defs.ma".
 
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con".
+inline procedural "Base-1/plist/props.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma
index c7c94ce539a43165834ebba46ca7b7a1d5d9608b..ee1cbb7dd297cabe1670ef7cbc016e926c3f5ea0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "ext/tactics.ma".
+include "Base-2/ext/tactics.ma".
 
-include "ext/arith.ma".
+include "Base-2/ext/arith.ma".
 
-include "types/props.ma".
+include "Base-2/types/props.ma".
 
-include "blt/props.ma".
+include "Base-2/blt/props.ma".
 
-include "plist/props.ma".
+include "Base-2/plist/props.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma
index e6ad43747fdf76551c6082fbd4b0549d9bee931f..0e6405c8f60ffb6f78c5294bd20f4346bfeb1ef7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma
@@ -14,68 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "preamble.ma".
+include "Base-2/preamble.ma".
 
-
-(* object and3 not inlined *)
-
-
-(* object and4 not inlined *)
-
-
-(* object and5 not inlined *)
-
-
-(* object or3 not inlined *)
-
-
-(* object or4 not inlined *)
-
-
-(* object ex3 not inlined *)
-
-
-(* object ex4 not inlined *)
-
-
-(* object ex_2 not inlined *)
-
-
-(* object ex2_2 not inlined *)
-
-
-(* object ex3_2 not inlined *)
-
-
-(* object ex4_2 not inlined *)
-
-
-(* object ex_3 not inlined *)
-
-
-(* object ex2_3 not inlined *)
-
-
-(* object ex3_3 not inlined *)
-
-
-(* object ex4_3 not inlined *)
-
-
-(* object ex3_4 not inlined *)
-
-
-(* object ex4_4 not inlined *)
-
-
-(* object ex4_5 not inlined *)
-
-
-(* object ex5_5 not inlined *)
-
-
-(* object ex6_6 not inlined *)
-
-
-(* object ex6_7 not inlined *)
+inline procedural "Base-1/types/defs.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma
index b9abd1c42a8cf9763552d211ba42e9a19c24ee09..1f9e3830176e9aac5e7384bf94a22e45a00bb333 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "types/defs.ma".
+include "Base-2/types/defs.ma".
 
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con".
+inline procedural "Base-1/types/props.ma".
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index 93fba67cede85250e940daded0ced5542e40b635..a57a7281eb33a855baac39626b3332c395559f9b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -1,10 +1,15 @@
-GOALS = all opt clean clean.opt
-
-DEVELS = Base-1 LambdaDelta-1 Base-2 Unified-Sub 
-
-$(GOALS): 
-       @$(foreach DEVEL, $(DEVELS), $(MAKE) -k -C $(DEVEL) $@;) 
-
-.PHONY: (GOALS)
-
-.SUFFIXES:
+DIR=$(shell basename $$PWD)
+MATITAOPTIONS=-onepass
+
+$(DIR) all:
+       ../../../matitac $(MATITAOPTIONS)
+$(DIR).opt opt all.opt:
+       ../../../matitac.opt $(MATITAOPTIONS)
+clean:
+       ../../../matitaclean
+clean.opt:
+       ../../../matitaclean.opt
+depend:
+       ../../../matitadep
+depend.opt:
+       ../../../matitadep.opt

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends
new file mode 100644 (file)
index 0000000..9bb223d
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/depends
@@ -0,0 +1,13 @@
+definitions.ma blt/defs.ma plist/defs.ma types/defs.ma
+preamble.ma coq.ma
+theory.ma blt/props.ma ext/arith.ma ext/tactics.ma plist/props.ma types/props.ma
+spare.ma theory.ma
+plist/props.ma plist/defs.ma
+plist/defs.ma preamble.ma
+ext/tactics.ma preamble.ma
+ext/arith.ma preamble.ma
+types/props.ma types/defs.ma
+types/defs.ma preamble.ma
+blt/props.ma blt/defs.ma
+blt/defs.ma preamble.ma
+coq.ma 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/root b/helm/software/matita/contribs/LAMBDA-TYPES/root
new file mode 100644 (file)
index 0000000..43a60f9
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/root
@@ -0,0 +1,2 @@
+baseuri=cic:/matita/LAMBDA-TYPES/Base-1
+include_paths= ../../../legacy