renaming

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
index 6eb948342b93a9f61366b0883c88593910ac615a..12438b398e279915d401814e14dbc760145091e1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma
@@ -14,7 +14,10 @@
 
 (* 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/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma
index 1fd2047fddb0b5b605e680bcb3183faa9a1fd3bd..d24466394020dcb303af8f3d01e1cf3bf2723a33 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma
@@ -14,7 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "blt/defs2.ma".
+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".
 

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
index 436b497c98c85cd02d8d9b7d9fe141545d25e108..0047b1438745658b2e7298be65a77e608a57192b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma
@@ -14,6 +14,8 @@
 
 (* 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".
@@ -21,6 +23,8 @@ 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".
 

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
index e6b75198a10ac06cdecfb7368271cebcc501b28d..18de7f71a5c1166f833154775b213ed097b2d93a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma
@@ -14,6 +14,8 @@
 
 (* 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".

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
index 4ae6d51568bb9027e06bcae22a25551428cf6e7a..3dc03da0b1c4ace660c3f977a8ffab6fdde85309 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma
@@ -14,6 +14,8 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs".
+
 include "preamble.ma".
 
 

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
index f9cec902e5dd5facde8e61d071ea1f53622aad89..29357a88a0621f5afaca3d657af34a164d6ec446 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma
@@ -14,7 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "plist/defs2.ma".
+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/root b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root
index 229adbd73f3d32cbff7c6eb11549e013f11efe37..ef1f7b21ec4075d6319a6ffe9180720002cc402c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root
@@ -1,2 +1 @@
 baseuri=cic:/matita/LAMBDA-TYPES/Base-2
-include_paths= ../Base-1 ../../../legacy

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma
index d1a0ca8b4e8175f94ee354f9f44e7bf4662bb0ae..1adab3e2b050a62a4238eb4ecc35d13002acc6da 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma
@@ -14,13 +14,15 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "ext/tactics2.ma".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory".
 
-include "ext/arith2.ma".
+include "ext/tactics.ma".
 
-include "types/props2.ma".
+include "ext/arith.ma".
 
-include "blt/props2.ma".
+include "types/props.ma".
 
-include "plist/props2.ma".
+include "blt/props.ma".
+
+include "plist/props.ma".
 

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
index 594edd269d6934a5992b5eeca4629904ece283cb..87c3378c25ffdad97091d0d100aee518a47e38a0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma
@@ -14,6 +14,8 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs".
+
 include "preamble.ma".
 
 
@@ -23,6 +25,9 @@ include "preamble.ma".
 (* object and4 not inlined *)
 
 
+(* object and5 not inlined *)
+
+
 (* object or3 not inlined *)
 
 

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
index 10b502461e8aba43f9fda9efa0b3513a8e60d45e..d79bfc46b3227350be1ccee85fc2144f3a5f91d4 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma
@@ -14,7 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "types/defs2.ma".
+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".