From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 19 Feb 2008 17:16:12 +0000 (+0000)
Subject: we are moving the devel root one dir level up
X-Git-Tag: make_still_working~5593
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e9753cbccef485911e2c2de1b4cdcae592906b9;p=helm.git

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
index a57a7281e..000000000
--- 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 293c184f5..660e18626 100644
--- 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 3cff54f96..751dcee9c 100644
--- 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 3a087dec7..79cc45e28 100644
--- 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
index 9bb223d98..000000000
--- 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 70a94bfbd..0d0f2a5df 100644
--- 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 7fcdc28ec..79551495d 100644
--- 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 9cfca05ae..5cf9337e4 100644
--- 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 bc480cc23..cfe98b20d 100644
--- 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
index 43a60f943..000000000
--- 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 c62e67982..024efedf4 100644
--- 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 c7c94ce53..3f643ffa1 100644
--- 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 cb8300ade..cddd83fd9 100644
--- 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 b27665600..d6f71f4a5 100644
--- 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 98bb97a68..1744bc276 100644
--- 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 5dfa152ee..63b209e18 100644
--- 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 4e73adbf7..c2e685e64 100644
--- 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 e6b75198a..474b8722a 100644
--- 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 4ae6d5156..b73b56fae 100644
--- 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 130dee88c..9e21e540a 100644
--- 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 c7c94ce53..ee1cbb7dd 100644
--- 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 e6ad43747..0e6405c8f 100644
--- 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 b9abd1c42..1f9e38301 100644
--- 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 93fba67ce..a57a7281e 100644
--- 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
index 000000000..9bb223d98
--- /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
index 000000000..43a60f943
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/root
@@ -0,0 +1,2 @@
+baseuri=cic:/matita/LAMBDA-TYPES/Base-1
+include_paths= ../../../legacy