renaming

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile
index f67b795810858f2816ccd3f5803fec2cde4067ca..125029529c699b8168d0ae27f3c82fc998be8962 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile
@@ -4,7 +4,7 @@ MMAS = $(shell find -name "*.mma")
 MAS = $(MMAS:%.mma=%.ma)
 
 %.ma: %.mma
-       echo -e "$< preamble.ma \npreamble.ma" > depends
+#      echo -e "$< preamble.ma \npreamble.ma" > depends
        ../../../matitac.opt -dump $@ $< 2>/dev/null
        ../../../matitadep.opt
        ../../../matitac.opt $@
@@ -19,8 +19,9 @@ clean:
 clean.opt:
        ../../../matitaclean.opt
        rm -f $(MAS)
+depend:
+       ../../../matitadep
+depend.opt:
+       ../../../matitadep.opt
 
-theory2.ma: theory2.mma ext/tactics2.ma ext/arith2.ma types/props2.ma blt/props2.ma plist/props2.ma 
-types/props2.ma: types/props2.mma types/defs2.ma 
-blt/props2.ma: blt/props2.mma blt/defs2.ma 
-plist/props2.ma: plist/props2.mma plist/defs2.ma 
+include xdepend

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
new file mode 100644 (file)
index 0000000..12438b3
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs".
+
+include "preamble.ma".
+
+
+(* object blt not inlined *)
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma
deleted file mode 100644 (file)
index 12438b3..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs".
-
-include "preamble.ma".
-
-
-(* object blt not inlined *)
-

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
new file mode 100644 (file)
index 0000000..d244663
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props".
+
+include "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".
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma
deleted file mode 100644 (file)
index d244663..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props".
-
-include "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".
-

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
new file mode 100644 (file)
index 0000000..0047b14
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith".
+
+include "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".
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma
deleted file mode 100644 (file)
index 0047b14..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma
+++ /dev/null
@@ -1,114 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith".
-
-include "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".
-

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
new file mode 100644 (file)
index 0000000..18de7f7
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics".
+
+include "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".
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma
deleted file mode 100644 (file)
index 18de7f7..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics".
-
-include "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".
-

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
new file mode 100644 (file)
index 0000000..3dc03da
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs".
+
+include "preamble.ma".
+
+
+(* object PList not inlined *)
+
+
+(* object PConsTail not inlined *)
+
+
+(* object Ss not inlined *)
+
+
+(* object papp not inlined *)
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma
deleted file mode 100644 (file)
index 3dc03da..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs".
-
-include "preamble.ma".
-
-
-(* object PList not inlined *)
-
-
-(* object PConsTail not inlined *)
-
-
-(* object Ss not inlined *)
-
-
-(* object papp not inlined *)
-

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
new file mode 100644 (file)
index 0000000..29357a8
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props".
+
+include "plist/defs.ma".
+
+inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con".
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma
deleted file mode 100644 (file)
index 29357a8..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma
+++ /dev/null
@@ -1,22 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props".
-
-include "plist/defs.ma".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con".
-

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma
new file mode 100644 (file)
index 0000000..1adab3e
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory".
+
+include "ext/tactics.ma".
+
+include "ext/arith.ma".
+
+include "types/props.ma".
+
+include "blt/props.ma".
+
+include "plist/props.ma".
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma
deleted file mode 100644 (file)
index 1adab3e..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory".
-
-include "ext/tactics.ma".
-
-include "ext/arith.ma".
-
-include "types/props.ma".
-
-include "blt/props.ma".
-
-include "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
new file mode 100644 (file)
index 0000000..87c3378
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs".
+
+include "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 *)
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma
deleted file mode 100644 (file)
index 87c3378..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma
+++ /dev/null
@@ -1,83 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs".
-
-include "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 *)
-

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
new file mode 100644 (file)
index 0000000..d79bfc4
--- /dev/null
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props".
+
+include "types/defs.ma".
+
+inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con".
+

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma
deleted file mode 100644 (file)
index d79bfc4..0000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma
+++ /dev/null
@@ -1,22 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props".
-
-include "types/defs.ma".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con".
-