LAMBDA-TYPES: mma's recommitted because inline syntax changed

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma
index cacddb1264388f897d69e7b6881e53b3996ae16c..7cbed8e15540a571164b72b6677907d8130f511b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/C/defs.ma".
 
 include "Basic-2/T/props.ma".
 
-inline procedural "Basic-1/C/props.ma".
+inline "Basic-1/C/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma
index fc2241b6b787f2212d921d6f82e4938646560e35..85ff33c1b31ee51df9df72c0c382a5a9ec3153a6 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/T/defs.ma".
 
-inline procedural "Basic-1/T/dec.ma".
+inline "Basic-1/T/dec.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma
index b55f1b473f992cfe807708ae1e46dada26e21d69..58ffc668a218293a98a84eaabe330de9239c8b21 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/T/defs.ma".
 
-inline procedural "Basic-1/T/props.ma".
+inline "Basic-1/T/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma
index 54c23e5cd47be27c06647ab4c6fa0215aa1d21a1..9e2234b3bf8fc73b6f15d55ab77eb8e5caa6b449 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/aplus/defs.ma".
 
 include "Basic-2/next_plus/props.ma".
 
-inline procedural "Basic-1/aplus/props.ma".
+inline "Basic-1/aplus/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma
index c718804b233fbf0235e6cc0b4add44d682e4d8f9..757c62bde23e0653f281c08ed2db74de5116caa3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/aprem/defs.ma".
 
-inline procedural "Basic-1/aprem/fwd.ma".
+inline "Basic-1/aprem/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma
index 0f465370c9792e7d53c32074bfe91fedbf8f9821..11509ac4bca385a629627b115922db221871fb7f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/aprem/fwd.ma".
 
 include "Basic-2/leq/defs.ma".
 
-inline procedural "Basic-1/aprem/props.ma".
+inline "Basic-1/aprem/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma
index fa502573a85a9f06f0a73c147945875197b81d6d..7a368efa9fa99bbb39f805715452db883bde0199 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma
@@ -20,5 +20,5 @@ include "Basic-2/arity/cimp.ma".
 
 include "Basic-2/aprem/props.ma".
 
-inline procedural "Basic-1/arity/aprem.ma".
+inline "Basic-1/arity/aprem.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma
index fe0eaa3d7835289f2ba5cf27ed2c1435e719065f..ca1bf3cad88be47ee12851ea1dcfe4bc488c25bb 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma
@@ -18,5 +18,5 @@ include "Basic-2/arity/defs.ma".
 
 include "Basic-2/cimp/props.ma".
 
-inline procedural "Basic-1/arity/cimp.ma".
+inline "Basic-1/arity/cimp.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma
index 1f507d36a84a9b0d4a16655002c5a0c252a86f95..7ef60bef211437c2128e796948246f8f6000f53d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma
@@ -20,5 +20,5 @@ include "Basic-2/leq/asucc.ma".
 
 include "Basic-2/getl/drop.ma".
 
-inline procedural "Basic-1/arity/fwd.ma".
+inline "Basic-1/arity/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma
index b3b189574eef3397ddbb2086a0de0dfca9242de6..adde308932a9b32c969f4ff71384a15b4f41dd74 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma
@@ -18,5 +18,5 @@ include "Basic-2/arity/props.ma".
 
 include "Basic-2/drop1/fwd.ma".
 
-inline procedural "Basic-1/arity/lift1.ma".
+inline "Basic-1/arity/lift1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma
index bd9f42ea45f6047fbb51da1c9f15dd97e5cb0c2c..8459c2a3512e539fbb2b9c935d21201b164f7091 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma
@@ -26,5 +26,5 @@ include "Basic-2/pr0/fwd.ma".
 
 include "Basic-2/arity/subst0.ma".
 
-inline procedural "Basic-1/arity/pr3.ma".
+inline "Basic-1/arity/pr3.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma
index 4e8db771353c359a01d73fe760dc5bd4d5a6118c..2d5c30d0d3a0eead789812da624f85b269686b87 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/arity/fwd.ma".
 
-inline procedural "Basic-1/arity/props.ma".
+inline "Basic-1/arity/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma
index 38cc5e1dce01b74f06875829739d3ec145007bdf..ff090fc8265b498353bb783623d8919a487d4382 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma
@@ -26,5 +26,5 @@ include "Basic-2/subst0/fwd.ma".
 
 include "Basic-2/getl/getl.ma".
 
-inline procedural "Basic-1/arity/subst0.ma".
+inline "Basic-1/arity/subst0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma
index 5fcb4195b0698e36bbf272c1b2058ab2c026cad5..d0e22947a13c264d6a1182b223bc8e1271b51ab7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/asucc/defs.ma".
 
-inline procedural "Basic-1/asucc/fwd.ma".
+inline "Basic-1/asucc/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma
index 65d74b41f6ff25a762b5d2ae56315442a16f8ff2..288bce2f2110b2494454724aaf48a48508e1ff94 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/cimp/defs.ma".
 
 include "Basic-2/getl/getl.ma".
 
-inline procedural "Basic-1/cimp/props.ma".
+inline "Basic-1/cimp/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma
index 67fe50f49faf118cc1b8f184b0dcd5045e5f7718..d78b3941add134354fc1cf749a80cf14a6419209 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma
@@ -18,5 +18,5 @@ include "Basic-2/clear/fwd.ma".
 
 include "Basic-2/drop/fwd.ma".
 
-inline procedural "Basic-1/clear/drop.ma".
+inline "Basic-1/clear/drop.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma
index b0262e8a03d75319fce1306fc1c0bd4a775efeae..e56fb51b1c4f497bae01a59939ff07aedf8c5291 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/clear/defs.ma".
 
-inline procedural "Basic-1/clear/fwd.ma".
+inline "Basic-1/clear/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma
index 58a577666780772c47fe0f0ef99c060148697cec..0bd37aee00e13afcc47136eebe4b8fd93e257c58 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/clear/fwd.ma".
 
-inline procedural "Basic-1/clear/props.ma".
+inline "Basic-1/clear/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma
index a9d3ff0d9a8a12626e0279ec60babaed3b83db24..3d2d8f86cd78e5c24dfad271cccf3b74471d28a3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma
@@ -18,5 +18,5 @@ include "Basic-2/clen/defs.ma".
 
 include "Basic-2/getl/props.ma".
 
-inline procedural "Basic-1/clen/getl.ma".
+inline "Basic-1/clen/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma
index 62b9e443440822f288355c915de2b1cee2da12db..8b288f51ffd718d2ad2ceff4c2b0b24294449253 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/cnt/defs.ma".
 
 include "Basic-2/lift/fwd.ma".
 
-inline procedural "Basic-1/cnt/props.ma".
+inline "Basic-1/cnt/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma
index 369818a189e66685775e872232c0f37a5588350d..2d7cdb86d0b158286e7c9150a547bc27b0e8b2b0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma
@@ -22,5 +22,5 @@ include "Basic-2/arity/props.ma".
 
 include "Basic-2/csubv/getl.ma".
 
-inline procedural "Basic-1/csuba/arity.ma".
+inline "Basic-1/csuba/arity.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma
index 0821bfb3f40c197d9e69226f94f2b4df8f5318ec..15098af706dd6a7cc2e335a9c17434a5d5dc3e56 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma
@@ -18,5 +18,5 @@ include "Basic-2/csuba/defs.ma".
 
 include "Basic-2/clear/fwd.ma".
 
-inline procedural "Basic-1/csuba/clear.ma".
+inline "Basic-1/csuba/clear.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma
index cdd71b487b5ff735fbbcad61a40527a47f8b7bac..4aec6957df5c2b04abf6337cde69fa8bd57fff9c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma
@@ -18,5 +18,5 @@ include "Basic-2/csuba/fwd.ma".
 
 include "Basic-2/drop/fwd.ma".
 
-inline procedural "Basic-1/csuba/drop.ma".
+inline "Basic-1/csuba/drop.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma
index 743375c8cc1209085d43c310e808ea319d8c1cb4..2c5a16f23d3ef5760d750fe0424211234be1dfb2 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csuba/defs.ma".
 
-inline procedural "Basic-1/csuba/fwd.ma".
+inline "Basic-1/csuba/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma
index 1003ae3ede884c63e518fe89c1480e215c617aeb..e52f58df93d47e18ff4af8673c7a0bf8fb833501 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma
@@ -20,5 +20,5 @@ include "Basic-2/csuba/clear.ma".
 
 include "Basic-2/getl/clear.ma".
 
-inline procedural "Basic-1/csuba/getl.ma".
+inline "Basic-1/csuba/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma
index b51a48e5a3599a33cf5732f708aba603e4cba6f3..d1ab319452ec1bcf8248173f2f88f07e3223b34e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csuba/defs.ma".
 
-inline procedural "Basic-1/csuba/props.ma".
+inline "Basic-1/csuba/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma
index 672c5c24dc7d1ee4cad5d18f1000c3a00d237348..63fff253295c0cb5be016a691f536c0d6ecebf09 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubc/csuba.ma".
 
-inline procedural "Basic-1/csubc/arity.ma".
+inline "Basic-1/csubc/arity.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma
index 8b2b8f4d4f1532dec51018a39083efb258b01965..1a0cbcf35e10c7cb0bff6ec80854975d54ae0cf6 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubc/fwd.ma".
 
-inline procedural "Basic-1/csubc/clear.ma".
+inline "Basic-1/csubc/clear.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma
index 5c11ce5d0f7c2ae1b36fd4955c3319f151ea7a22..f3465bf35d16f70a1f77ec8ca8a1ed39944163a3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubc/defs.ma".
 
 include "Basic-2/sc3/props.ma".
 
-inline procedural "Basic-1/csubc/csuba.ma".
+inline "Basic-1/csubc/csuba.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma
index 358af78fe69fea476aa1f8cf96dffe1967dad3d8..2a5d715f525d6be6c8121dd21f055479583a971e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubc/fwd.ma".
 
 include "Basic-2/sc3/props.ma".
 
-inline procedural "Basic-1/csubc/drop.ma".
+inline "Basic-1/csubc/drop.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma
index bd910efbe1f5347dda5c3f13a4694fc53355c42c..9863063cfede01421bb193b6a237fc33d199d482 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubc/drop.ma".
 
-inline procedural "Basic-1/csubc/drop1.ma".
+inline "Basic-1/csubc/drop1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma
index ca11e80ceebf118cd19518c6a98c839fdcfc7c38..1d0dd32ab54e01e49d7e2c91fc13c9dba167a03a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubc/defs.ma".
 
-inline procedural "Basic-1/csubc/fwd.ma".
+inline "Basic-1/csubc/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma
index 18370f8cd2880dd2694459087588b831f29142cb..60462e1539f45446abf9ba292fc19ea47a2de8b3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubc/drop.ma".
 
 include "Basic-2/csubc/clear.ma".
 
-inline procedural "Basic-1/csubc/getl.ma".
+inline "Basic-1/csubc/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma
index 8c06dacb997be4f5f247b1bc8916b664cb7f1a4f..ff7a8f4e5ea7a24e1259d1b9c9c6ec224323ed6c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubc/defs.ma".
 
 include "Basic-2/sc3/props.ma".
 
-inline procedural "Basic-1/csubc/props.ma".
+inline "Basic-1/csubc/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma
index be8bfc1964e12b8a2388b4cb93d12c1a754b1643..0b3c214d7b0defbf85121e35aa6861b5e73f4d57 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma
@@ -20,5 +20,5 @@ include "Basic-2/csubst0/fwd.ma".
 
 include "Basic-2/clear/fwd.ma".
 
-inline procedural "Basic-1/csubst0/clear.ma".
+inline "Basic-1/csubst0/clear.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma
index 90eefc18899ab80c5fb026c3bcb4aa48479c99e9..8ec4de71c58a867829fa2a602bb4eefade590ab4 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma
@@ -20,5 +20,5 @@ include "Basic-2/drop/fwd.ma".
 
 include "Basic-2/s/props.ma".
 
-inline procedural "Basic-1/csubst0/drop.ma".
+inline "Basic-1/csubst0/drop.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma
index e44c4945f34533d53448eb265665a45945933bae..85ddb329e822544b142bf555b6d5da317a7934df 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubst0/defs.ma".
 
-inline procedural "Basic-1/csubst0/fwd.ma".
+inline "Basic-1/csubst0/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma
index b2deae890ca671ec3152052a1ab6c6fadee1e311..679c49e9e763b4cf1abfaef12e4d4aedd01938c9 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma
@@ -20,5 +20,5 @@ include "Basic-2/csubst0/drop.ma".
 
 include "Basic-2/getl/fwd.ma".
 
-inline procedural "Basic-1/csubst0/getl.ma".
+inline "Basic-1/csubst0/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma
index f5af7cd6433389cf6e4882d4729d550bee4721c9..fee62c65162f22d4c2d67286e58a77ff52db984e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubst0/defs.ma".
 
-inline procedural "Basic-1/csubst0/props.ma".
+inline "Basic-1/csubst0/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma
index b09e92f45dab427bc41eebe70ef2ada48fe06832..2c9d5bedb0ccf1cfb41765bd2fcdf0dd59d191bd 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma
@@ -20,5 +20,5 @@ include "Basic-2/csubst0/fwd.ma".
 
 include "Basic-2/subst1/props.ma".
 
-inline procedural "Basic-1/csubst1/fwd.ma".
+inline "Basic-1/csubst1/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma
index 92e622951f5fcc6216187334d50aa9494df23ed4..05b80d444a9dec913f674b9e63239e03380eaf6c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma
@@ -22,5 +22,5 @@ include "Basic-2/subst1/props.ma".
 
 include "Basic-2/drop/props.ma".
 
-inline procedural "Basic-1/csubst1/getl.ma".
+inline "Basic-1/csubst1/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma
index ca8d9969c721418e1e1e52f3a70dd48d447ad73a..7480c122d7b9e30da494e83a16398b4e3d7a6cc4 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubst1/defs.ma".
 
 include "Basic-2/subst1/defs.ma".
 
-inline procedural "Basic-1/csubst1/props.ma".
+inline "Basic-1/csubst1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma
index 2502280a87e50f03cf227010cd1d1074b0ad3605..c35e253b44e9daf1d899b04cf5d346c5afd2a428 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubt/defs.ma".
 
 include "Basic-2/clear/fwd.ma".
 
-inline procedural "Basic-1/csubt/clear.ma".
+inline "Basic-1/csubt/clear.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma
index 3aee698d6637fa2e9f6f571083fdd65bef6d8412..3145d010e4650bf02908d6e7326917836b2acbdd 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/ty3/arity.ma".
 
-inline procedural "Basic-1/csubt/csuba.ma".
+inline "Basic-1/csubt/csuba.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma
index 610073d97a8cb6438f2d30880d5252eca460bbe9..7d8d90b332658afad9b1e8f70727300d73d0732f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubt/fwd.ma".
 
 include "Basic-2/drop/fwd.ma".
 
-inline procedural "Basic-1/csubt/drop.ma".
+inline "Basic-1/csubt/drop.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma
index 3cdde9d7117ed01b59bbe3eabfdf7f9e981c140b..195de62cb121057d7aba12bd0a04a5f68a24a315 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubt/defs.ma".
 
-inline procedural "Basic-1/csubt/fwd.ma".
+inline "Basic-1/csubt/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma
index e7d81a5e926fa3c98ad0b516b0bdc72baa931fbf..14299efa2f958379b7bd931270c7e13325216226 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma
@@ -20,5 +20,5 @@ include "Basic-2/csubt/drop.ma".
 
 include "Basic-2/getl/clear.ma".
 
-inline procedural "Basic-1/csubt/getl.ma".
+inline "Basic-1/csubt/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma
index a6d7a967d075da0c09e7acd65c826c7b9782f82d..48152a3673fa0a519c9993b4e2d1c728ac5f344f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubt/getl.ma".
 
 include "Basic-2/pc3/left.ma".
 
-inline procedural "Basic-1/csubt/pc3.ma".
+inline "Basic-1/csubt/pc3.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma
index a663399b7d64f6f3a42f72fed8bcf1e9ba01d20e..59d3c5188efe8ec9c4cab614c414e564a0e9189b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/csubt/defs.ma".
 
-inline procedural "Basic-1/csubt/props.ma".
+inline "Basic-1/csubt/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma
index ee9e065c1f72d3b993075fe4f07b02178a8726df..8bb74616ae721fc0ddfd322f0bc4d0f4043d867d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubt/pc3.ma".
 
 include "Basic-2/csubt/props.ma".
 
-inline procedural "Basic-1/csubt/ty3.ma".
+inline "Basic-1/csubt/ty3.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma
index cb374edc164bd605fe97d03b6e07df46f12976ac..77768e99374effd9c3a01512469ca70b9a993582 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubv/defs.ma".
 
 include "Basic-2/clear/fwd.ma".
 
-inline procedural "Basic-1/csubv/clear.ma".
+inline "Basic-1/csubv/clear.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma
index 9dfe7cca016f322696fc819da6467f7e921f54bd..d0d2b3f76ff52057fd9c3e2429fb78f2b705c9aa 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubv/props.ma".
 
 include "Basic-2/drop/fwd.ma".
 
-inline procedural "Basic-1/csubv/drop.ma".
+inline "Basic-1/csubv/drop.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma
index a9e95aad4a0c6a7935fa4bec3a0bbdf5ef47226c..66c63a6397b7e87d978b50597abb83e38aa7260e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma
@@ -20,5 +20,5 @@ include "Basic-2/csubv/drop.ma".
 
 include "Basic-2/getl/fwd.ma".
 
-inline procedural "Basic-1/csubv/getl.ma".
+inline "Basic-1/csubv/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma
index 13fae5503cf8b033f364e62fde1e5f034c428f09..44d2edf27397e7d59408800f57906bfa8d4f9af4 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/csubv/defs.ma".
 
 include "Basic-2/T/props.ma".
 
-inline procedural "Basic-1/csubv/props.ma".
+inline "Basic-1/csubv/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma
index 1e889f6ff2406239ee97e33b545a7511cc837fa8..d88936b9c4e3844fb03f533f75008c28adcf305f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/drop/defs.ma".
 
-inline procedural "Basic-1/drop/fwd.ma".
+inline "Basic-1/drop/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma
index b21052d8fcf0544c56cb7e35d965f0b0b9c3573b..9af06df85fd2c751e260aaf42bd7c85dd9ec4ba3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma
@@ -20,5 +20,5 @@ include "Basic-2/lift/props.ma".
 
 include "Basic-2/r/props.ma".
 
-inline procedural "Basic-1/drop/props.ma".
+inline "Basic-1/drop/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma
index 771733bbc38aea4ffd74cca2d4364a6791d08a26..78b91b3491da50c04c3b0b83538a7e0fa8e3a659 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/drop1/defs.ma".
 
-inline procedural "Basic-1/drop1/fwd.ma".
+inline "Basic-1/drop1/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma
index b8856b912ceae776493cebb108f6e2ab711c9b45..0b9e358d20226f1551306d3c9c0f1a5c08c3590e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma
@@ -18,5 +18,5 @@ include "Basic-2/drop1/fwd.ma".
 
 include "Basic-2/getl/drop.ma".
 
-inline procedural "Basic-1/drop1/getl.ma".
+inline "Basic-1/drop1/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma
index 18a856e8a83c1bcc36331f4e4e3de9974e4a4511..f4f2204accde5fedec118d5ac9d00859b5473def 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma
@@ -20,5 +20,5 @@ include "Basic-2/drop/props.ma".
 
 include "Basic-2/getl/defs.ma".
 
-inline procedural "Basic-1/drop1/props.ma".
+inline "Basic-1/drop1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma
index 8680a106f071e63f877988017da6a0332b086420..80204275f6954049658556e335076f69b2ad01c5 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma
@@ -20,5 +20,5 @@ include "Basic-2/leq/defs.ma".
 
 include "Basic-2/aplus/props.ma".
 
-inline procedural "Basic-1/ex0/props.ma".
+inline "Basic-1/ex0/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma
index efc47ad2a5f1a77be0a210888d773ff0c4952d4b..8ec7ebe3e91a68537829b16d0909529cfc9ea34d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma
@@ -28,5 +28,5 @@ include "Basic-2/arity/defs.ma".
 
 include "Basic-2/leq/props.ma".
 
-inline procedural "Basic-1/ex1/props.ma".
+inline "Basic-1/ex1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma
index 44299ae27e7aa48e02a0b736f72bdd3c1be09975..56d0d85579186bd3743a9382b192ba3b97fb5f43 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma
@@ -22,5 +22,5 @@ include "Basic-2/pr2/fwd.ma".
 
 include "Basic-2/arity/fwd.ma".
 
-inline procedural "Basic-1/ex2/props.ma".
+inline "Basic-1/ex2/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma
index 81509432b3636fc88ae4bdfc89f372c95d4e1d0c..e5b76348f8ad993b88354c50d2a9a458e66a688e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/flt/defs.ma".
 
 include "Basic-2/C/props.ma".
 
-inline procedural "Basic-1/flt/props.ma".
+inline "Basic-1/flt/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma
index e04ab42fe7ee0d064bfccd33e0be73d265662596..4a60d7191e0903c285a26ec03b6cb746a51ce4b0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/fsubst0/defs.ma".
 
-inline procedural "Basic-1/fsubst0/fwd.ma".
+inline "Basic-1/fsubst0/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma
index 4a94110dc335656212a8c941d87c9152570dbf19..3f69bde5d89b0e84a203e438ff7283919749f131 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma
@@ -18,5 +18,5 @@ include "Basic-2/getl/props.ma".
 
 include "Basic-2/clear/drop.ma".
 
-inline procedural "Basic-1/getl/clear.ma".
+inline "Basic-1/getl/clear.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma
index 8be561b34fadc527ea8cd185ff75b56485f2993f..4085b140e2f4bbe144e0e77e8a78a0be3bfc4ace 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/getl/props.ma".
 
-inline procedural "Basic-1/getl/dec.ma".
+inline "Basic-1/getl/dec.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma
index 519905e392af399a39c4da43af8ae68d015bfa8e..ff4bb646f91867b99eee6c070a7f341d9b90b5a1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma
@@ -18,5 +18,5 @@ include "Basic-2/getl/props.ma".
 
 include "Basic-2/clear/drop.ma".
 
-inline procedural "Basic-1/getl/drop.ma".
+inline "Basic-1/getl/drop.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma
index 7e96ea75f17cafd50172cb118990e7f1e48fdc57..c030693f50e7e2a935ff490a6a8a06667d01d650 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma
@@ -20,5 +20,5 @@ include "Basic-2/clear/props.ma".
 
 include "Basic-2/flt/props.ma".
 
-inline procedural "Basic-1/getl/flt.ma".
+inline "Basic-1/getl/flt.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma
index 09e90498457015ff6ce9f7f69b793e0953257c5b..dfcee95767d58d81c77574b6ca4676c80daee016 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma
@@ -20,5 +20,5 @@ include "Basic-2/drop/fwd.ma".
 
 include "Basic-2/clear/fwd.ma".
 
-inline procedural "Basic-1/getl/fwd.ma".
+inline "Basic-1/getl/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma
index 2bbee600a45df7f64861fd31758c2ffc50e7af67..b5e5163d77a95f1eee32a22b6b915f35d659295a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma
@@ -18,5 +18,5 @@ include "Basic-2/getl/drop.ma".
 
 include "Basic-2/getl/clear.ma".
 
-inline procedural "Basic-1/getl/getl.ma".
+inline "Basic-1/getl/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma
index 65e4f592293d5bc62127a98268ebd15ab6e43312..00ff97539d8dd83e80c1691ac297022968c57509 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma
@@ -20,5 +20,5 @@ include "Basic-2/drop/props.ma".
 
 include "Basic-2/clear/props.ma".
 
-inline procedural "Basic-1/getl/props.ma".
+inline "Basic-1/getl/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma
index b23bf49effb68998272551c48dc112819e726e24..8ae8aaad1e6bea3aaeec352821f730b44c749b68 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/iso/defs.ma".
 
 include "Basic-2/tlist/defs.ma".
 
-inline procedural "Basic-1/iso/fwd.ma".
+inline "Basic-1/iso/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma
index f800970b26efd814a748cb78113080ef3703863c..c689ea1fc83ee9982102424350507b41f2b25cd1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/iso/fwd.ma".
 
-inline procedural "Basic-1/iso/props.ma".
+inline "Basic-1/iso/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma
index 8465e224c11e3402bce91ac0fcc37939d5861910..a89191b08e8ef51363dd53884d9cacc3cc155ad2 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/leq/props.ma".
 
-inline procedural "Basic-1/leq/asucc.ma".
+inline "Basic-1/leq/asucc.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma
index b390962ac02026ffc2a8453400c4f88f1e9026c6..75043713521c28837d8408d9c2d63d503f9a87e5 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/leq/defs.ma".
 
-inline procedural "Basic-1/leq/fwd.ma".
+inline "Basic-1/leq/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma
index 780abb9fcbec64aec761a6db201d07bd198309e7..b2509dd318e7a89601d8de05d962e04d7d93e12c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/leq/fwd.ma".
 
 include "Basic-2/aplus/props.ma".
 
-inline procedural "Basic-1/leq/props.ma".
+inline "Basic-1/leq/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma
index 9111d87fc2f4aedc9c8e21a3459ebd8d506d2b2e..95a454dbefa1be2e52808a37a8d2d493d3f2ff04 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/lift/defs.ma".
 
-inline procedural "Basic-1/lift/fwd.ma".
+inline "Basic-1/lift/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma
index dee77c3f807496d1b911ef4899b047f14abd6021..88f85f5cb5013bd3df7a0b6684791aaf63859763 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/lift/fwd.ma".
 
 include "Basic-2/s/props.ma".
 
-inline procedural "Basic-1/lift/props.ma".
+inline "Basic-1/lift/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma
index ee45a479940d08a63034689d96628b4185776074..51c97298795a2ef710d8248757ae347ef65dae45 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma
@@ -18,5 +18,5 @@ include "Basic-2/lift/fwd.ma".
 
 include "Basic-2/tlt/props.ma".
 
-inline procedural "Basic-1/lift/tlt.ma".
+inline "Basic-1/lift/tlt.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma
index d2823197e1f75f90219b4d34699500ae94965118..3aabe676f333fcf221e7b42a02e4154984b96ef7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/lift1/defs.ma".
 
 include "Basic-2/lift/fwd.ma".
 
-inline procedural "Basic-1/lift1/fwd.ma".
+inline "Basic-1/lift1/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma
index 7e5f7f7a137241bd99d5df1dc72cd3b9f1cb49a4..89bed21665b2dcc564561d81880ea2ae50daeba8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/lift/props.ma".
 
 include "Basic-2/drop1/defs.ma".
 
-inline procedural "Basic-1/lift1/props.ma".
+inline "Basic-1/lift1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma
index 505fdd5671efc3b23272a50b90ff1655add3de77..462e5c57513051d44f3e0514d5ad5292a804d220 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/llt/defs.ma".
 
 include "Basic-2/leq/defs.ma".
 
-inline procedural "Basic-1/llt/props.ma".
+inline "Basic-1/llt/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma
index e08bd778d3f7b84222069648ea0f6216bde2c788..8e6ff559c7aa7444b6f841773222b21bb85e2862 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/next_plus/defs.ma".
 
-inline procedural "Basic-1/next_plus/props.ma".
+inline "Basic-1/next_plus/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma
index 24a7f1b46e7b4175a4982aa7b0fdb34ac6622d0b..356dfa5913ef0e493ff57e72144c70bcdafb7320 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma
@@ -18,5 +18,5 @@ include "Basic-2/nf2/fwd.ma".
 
 include "Basic-2/arity/subst0.ma".
 
-inline procedural "Basic-1/nf2/arity.ma".
+inline "Basic-1/nf2/arity.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma
index ca725c3aeb2b5863da4d341ea7d6787542da8c8b..179da42ffe52c723170b3123d2da1ab88ec9a010 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma
@@ -24,5 +24,5 @@ include "Basic-2/pr0/dec.ma".
 
 include "Basic-2/C/props.ma".
 
-inline procedural "Basic-1/nf2/dec.ma".
+inline "Basic-1/nf2/dec.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma
index 43248cca2c7caf84d76706ec7ff518a0b283f1c4..0f941386e9c0f4601247cf038e15d0d38f9e4caa 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma
@@ -22,5 +22,5 @@ include "Basic-2/subst0/dec.ma".
 
 include "Basic-2/T/props.ma".
 
-inline procedural "Basic-1/nf2/fwd.ma".
+inline "Basic-1/nf2/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma
index b52c08cb7fcccdba9c78b6af31ac2db1b9ed6798..0c6309e1ccc9842d2ce24232a2f9ed6f0cd8bcc3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma
@@ -20,5 +20,5 @@ include "Basic-2/pr3/fwd.ma".
 
 include "Basic-2/iso/props.ma".
 
-inline procedural "Basic-1/nf2/iso.ma".
+inline "Basic-1/nf2/iso.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma
index 8291013c6ead9d49567e5a37b1c46018228b9a61..250c8dd78e8dd0d177aea2876c9ecb56d9162bc4 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma
@@ -18,5 +18,5 @@ include "Basic-2/nf2/props.ma".
 
 include "Basic-2/drop1/fwd.ma".
 
-inline procedural "Basic-1/nf2/lift1.ma".
+inline "Basic-1/nf2/lift1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma
index 7b5a3b036b570210caeb827566eed26253c8513e..00ba3ffabe01a01da06e50c02b5c3cfb73a46ac4 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma
@@ -18,5 +18,5 @@ include "Basic-2/nf2/defs.ma".
 
 include "Basic-2/pr3/pr3.ma".
 
-inline procedural "Basic-1/nf2/pr3.ma".
+inline "Basic-1/nf2/pr3.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma
index 565a5316b890cbbc6959eb5116ea4adc686d9b98..6977bd06933b4e3d9470f0681f206ab775765a16 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/nf2/defs.ma".
 
 include "Basic-2/pr2/fwd.ma".
 
-inline procedural "Basic-1/nf2/props.ma".
+inline "Basic-1/nf2/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma
index a73cc0a9d508b423c057f2af603718fc6080606f..f031a23629bb313212f70a1e90d3f16d272f53c7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/pc1/defs.ma".
 
 include "Basic-2/pr1/pr1.ma".
 
-inline procedural "Basic-1/pc1/props.ma".
+inline "Basic-1/pc1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma
index b8455a1179aa29040eaeec07973f6406c3061f7b..d5ed4097b34e5af7bd651ae2c9e6fefd11d5e896 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma
@@ -18,5 +18,5 @@ include "Basic-2/ty3/arity_props.ma".
 
 include "Basic-2/nf2/fwd.ma".
 
-inline procedural "Basic-1/pc3/dec.ma".
+inline "Basic-1/pc3/dec.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma
index ceb6970c1739cafad87514ed6884b422cbb0b0ac..478c285afcc3f240140cc5c3580c9fa8333d44b3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma
@@ -20,5 +20,5 @@ include "Basic-2/fsubst0/defs.ma".
 
 include "Basic-2/csubst0/getl.ma".
 
-inline procedural "Basic-1/pc3/fsubst0.ma".
+inline "Basic-1/pc3/fsubst0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma
index e547cb96e8707c7f39f5198b0eb88071bf2f91bd..83816ceacb321798302c5ae052f3a0e8e477af64 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/pc3/props.ma".
 
 include "Basic-2/pr3/fwd.ma".
 
-inline procedural "Basic-1/pc3/fwd.ma".
+inline "Basic-1/pc3/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma
index 9be44a05b3e2ea4bf1e28d86f2edc002470be51c..a0102b20126a33d7a980f0c2bb7703a9a757bd22 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/pc3/props.ma".
 
-inline procedural "Basic-1/pc3/left.ma".
+inline "Basic-1/pc3/left.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma
index d3db0ecee70037eaef6f884b6bab61116e433c74..38a00ff31f7a2af9681440a57aaab566d47f1de5 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma
@@ -18,5 +18,5 @@ include "Basic-2/pc3/defs.ma".
 
 include "Basic-2/nf2/pr3.ma".
 
-inline procedural "Basic-1/pc3/nf2.ma".
+inline "Basic-1/pc3/nf2.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma
index 35376ac79f7f4fba89efe9cd2fa32aab90f676b7..0a82a8adce3318a9b1b6b4d5a18d0c3fc854619d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma
@@ -20,5 +20,5 @@ include "Basic-2/pc1/defs.ma".
 
 include "Basic-2/pr3/pr1.ma".
 
-inline procedural "Basic-1/pc3/pc1.ma".
+inline "Basic-1/pc3/pc1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma
index 36c526b0a5beaf4c7ce6368d2f72169c3f88a850..01c5ee4e84da67340fdfb2df7d9e23c6fae9f21f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/pc3/defs.ma".
 
 include "Basic-2/pr3/pr3.ma".
 
-inline procedural "Basic-1/pc3/props.ma".
+inline "Basic-1/pc3/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma
index 8f00fb8e689dcaa1c6b3cb62e2c514b284676b39..1ec4a10d5b75045f6143c56d619c434343111ff9 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma
@@ -18,5 +18,5 @@ include "Basic-2/pc3/props.ma".
 
 include "Basic-2/pr3/subst1.ma".
 
-inline procedural "Basic-1/pc3/subst1.ma".
+inline "Basic-1/pc3/subst1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma
index 5b99aa5160fd81f78a5917c1d77c1ff21398e158..98ae77c9b1ce55da31c8c576e2fa931e4cb2dd82 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma
@@ -18,5 +18,5 @@ include "Basic-2/pc3/props.ma".
 
 include "Basic-2/wcpr0/getl.ma".
 
-inline procedural "Basic-1/pc3/wcpr0.ma".
+inline "Basic-1/pc3/wcpr0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma
index ce38c93bb5c9820d280e84a319c3a057fdb24e31..c88b2b72570b06094f6c30e01f45b450285842f0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma
@@ -22,5 +22,5 @@ include "Basic-2/T/dec.ma".
 
 include "Basic-2/T/props.ma".
 
-inline procedural "Basic-1/pr0/dec.ma".
+inline "Basic-1/pr0/dec.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma
index 7932cb99dc47f48cb4b946ec881d1a4619374a61..2349a51272e57492a3ea28b55db1e1b6a3b3e8bf 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/pr0/props.ma".
 
-inline procedural "Basic-1/pr0/fwd.ma".
+inline "Basic-1/pr0/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma
index 8021fe15f5d75495912bbfd01af74c9c3137348e..cc88c47e0237950c9d958f4cb1a6da32ce9d3153 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr0/fwd.ma".
 
 include "Basic-2/lift/tlt.ma".
 
-inline procedural "Basic-1/pr0/pr0.ma".
+inline "Basic-1/pr0/pr0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma
index 7cb130986a27fbf9aff7d98f2824714641f44f53..9b8e83a73536cd6827b769043c285115624d45a2 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr0/defs.ma".
 
 include "Basic-2/subst0/subst0.ma".
 
-inline procedural "Basic-1/pr0/props.ma".
+inline "Basic-1/pr0/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma
index 62f059201dba48298e83d506635274dd0db8d05c..a4af1a6953c3a1c80d2720939817469e49555ff5 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr0/props.ma".
 
 include "Basic-2/subst1/defs.ma".
 
-inline procedural "Basic-1/pr0/subst1.ma".
+inline "Basic-1/pr0/subst1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma
index e94793c500a84c7f909a6e64ba91e72f27d63b0e..f05ca1cd35cbe79c03b0cc0012e4880f0bba2c1a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr1/props.ma".
 
 include "Basic-2/pr0/pr0.ma".
 
-inline procedural "Basic-1/pr1/pr1.ma".
+inline "Basic-1/pr1/pr1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma
index 59da19ba943c730c368881ae9f43379b4b6b9c29..5ec9c7f3e0b8b374d982bee30a605a2d4b9e8e19 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma
@@ -22,5 +22,5 @@ include "Basic-2/subst1/props.ma".
 
 include "Basic-2/T/props.ma".
 
-inline procedural "Basic-1/pr1/props.ma".
+inline "Basic-1/pr1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma
index 86b48b79939997d61c0222a108b0e1d815a97615..e3ea2f078d31342b5fd95e2d4303259cab637e20 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr2/props.ma".
 
 include "Basic-2/clen/getl.ma".
 
-inline procedural "Basic-1/pr2/clen.ma".
+inline "Basic-1/pr2/clen.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma
index 5aaaa6b34cfa540214f0e1a087aa8ddac1b301bb..9ec452e995f19b3e505e0d7d2adde5c7d72ec8c6 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma
@@ -22,5 +22,5 @@ include "Basic-2/getl/drop.ma".
 
 include "Basic-2/getl/clear.ma".
 
-inline procedural "Basic-1/pr2/fwd.ma".
+inline "Basic-1/pr2/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma
index f2a69266559ba9cc4a0fc9e72a77bda074dae08e..8879c71e809a7b2afd82fb90c30c22b322d58f3d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma
@@ -20,5 +20,5 @@ include "Basic-2/pr0/pr0.ma".
 
 include "Basic-2/getl/props.ma".
 
-inline procedural "Basic-1/pr2/pr2.ma".
+inline "Basic-1/pr2/pr2.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma
index 7db1b656a60e65362da59467e1c55a1a0facbb6c..b0e27c8fcebe653b0719d68f865b62e366d05cad 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma
@@ -22,5 +22,5 @@ include "Basic-2/getl/drop.ma".
 
 include "Basic-2/getl/clear.ma".
 
-inline procedural "Basic-1/pr2/props.ma".
+inline "Basic-1/pr2/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma
index b0c47c4a342031287add75be67353ac13150af08..61b1612221ab5ce07b38309182701cf08a3afbd7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma
@@ -28,5 +28,5 @@ include "Basic-2/subst1/subst1.ma".
 
 include "Basic-2/getl/drop.ma".
 
-inline procedural "Basic-1/pr2/subst1.ma".
+inline "Basic-1/pr2/subst1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma
index 9445d5d1daf138d5031c131749f108ec3c0bbb67..a29ddcee02d60c5a2b0aa6a826a45b41c2ba2a2c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr3/props.ma".
 
 include "Basic-2/pr2/fwd.ma".
 
-inline procedural "Basic-1/pr3/fwd.ma".
+inline "Basic-1/pr3/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma
index 91b74af6c73cd9041429401604f2ac8e563f6f07..a401d94dce016b759f2c63b63b250d0187b8c357 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma
@@ -20,5 +20,5 @@ include "Basic-2/iso/props.ma".
 
 include "Basic-2/tlist/props.ma".
 
-inline procedural "Basic-1/pr3/iso.ma".
+inline "Basic-1/pr3/iso.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma
index 31599c3c97117140ba5befe74ab854483d8c6b56..6827dfddc2b61b8c955beb2ac0f0858f85c6c31b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr3/defs.ma".
 
 include "Basic-2/pr1/defs.ma".
 
-inline procedural "Basic-1/pr3/pr1.ma".
+inline "Basic-1/pr3/pr1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma
index 866281845e750d03ab2f453d2847052af8f68d20..a393080b66d6bedd6ffff812f0b1ee97319327ba 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr3/props.ma".
 
 include "Basic-2/pr2/pr2.ma".
 
-inline procedural "Basic-1/pr3/pr3.ma".
+inline "Basic-1/pr3/pr3.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma
index 055cd0b15f4125fdfab68e0f1b6a9ff5f752fc16..c87af259a35f4973b081fcd614cf228231b9a4e2 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma
@@ -20,5 +20,5 @@ include "Basic-2/pr2/props.ma".
 
 include "Basic-2/pr1/props.ma".
 
-inline procedural "Basic-1/pr3/props.ma".
+inline "Basic-1/pr3/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma
index bb74e3f7d7d7a7aab427b75a7ab077a0b1e23ce7..73288e8838bd369e68bd7077977b51549332390a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr3/defs.ma".
 
 include "Basic-2/pr2/subst1.ma".
 
-inline procedural "Basic-1/pr3/subst1.ma".
+inline "Basic-1/pr3/subst1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma
index 09a0b32ffb40fae1d3027c5dd79b91cfa299ee8f..6c30039f1d01270324c257b0362bb244c1db09f8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma
@@ -18,5 +18,5 @@ include "Basic-2/pr3/props.ma".
 
 include "Basic-2/wcpr0/getl.ma".
 
-inline procedural "Basic-1/pr3/wcpr0.ma".
+inline "Basic-1/pr3/wcpr0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma
index 1cee8e5f6aaa4a2499126c8a8eb05acf8e4d9449..79edc95f4466a66c2fdf08a8851104d71fa47b0e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/r/defs.ma".
 
 include "Basic-2/s/defs.ma".
 
-inline procedural "Basic-1/r/props.ma".
+inline "Basic-1/r/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma
index e77078ec54e9c5a50e3ab7d43fbe54b9d4bfd050..35f1ad31bdce5e4146d0bf37db708e9b4f18eaec 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/s/defs.ma".
 
-inline procedural "Basic-1/s/props.ma".
+inline "Basic-1/s/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma
index 6d498e3c9af33352a48d956625fa070156308ce2..9fa3eaf9346fb2b433c6f197a4348e8a2b8f055d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma
@@ -22,5 +22,5 @@ include "Basic-2/csubc/drop1.ma".
 
 include "Basic-2/csubc/props.ma".
 
-inline procedural "Basic-1/sc3/arity.ma".
+inline "Basic-1/sc3/arity.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma
index 2a7989263718c1256baa30fd928aac72ebece371..859458266c390da9d0f36d3756e3afe0a2d5ad0d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma
@@ -34,5 +34,5 @@ include "Basic-2/drop1/props.ma".
 
 include "Basic-2/lift1/props.ma".
 
-inline procedural "Basic-1/sc3/props.ma".
+inline "Basic-1/sc3/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma
index 92427e1cd747d16641f5bec918ec2df9e610efe0..a4662eefadfb5e966f4c95b19b981d1d1f703903 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/sn3/defs.ma".
 
 include "Basic-2/pr3/props.ma".
 
-inline procedural "Basic-1/sn3/fwd.ma".
+inline "Basic-1/sn3/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma
index 9839254a9fa440da5bceb443a9212fec16a7b830..e8c0c4de2fe5f5275f759bcc29156293e16ad63e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma
@@ -20,5 +20,5 @@ include "Basic-2/drop1/fwd.ma".
 
 include "Basic-2/lift1/fwd.ma".
 
-inline procedural "Basic-1/sn3/lift1.ma".
+inline "Basic-1/sn3/lift1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma
index 69b9db0368776d5ab0c5a873ea059dc65294803a..81de1d480fc22e19e060554d665b74d04afa56e3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma
@@ -20,5 +20,5 @@ include "Basic-2/nf2/dec.ma".
 
 include "Basic-2/nf2/pr3.ma".
 
-inline procedural "Basic-1/sn3/nf2.ma".
+inline "Basic-1/sn3/nf2.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma
index 9e37a001f761e8ea6b6ea7eea45ee84142a470d4..3244a523752afc6e292eedc4a5353cd92129115f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma
@@ -22,5 +22,5 @@ include "Basic-2/nf2/iso.ma".
 
 include "Basic-2/pr3/iso.ma".
 
-inline procedural "Basic-1/sn3/props.ma".
+inline "Basic-1/sn3/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma
index 164d6ec87e718c8a0be6a3096862fcdc8c17edee..a2600b078c9acb72d5affa30b644c9f2219bf397 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/sty0/defs.ma".
 
-inline procedural "Basic-1/sty0/fwd.ma".
+inline "Basic-1/sty0/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma
index 8cc6b475a3a9aa4a9a907f072b219fdc75f4cc18..403332ea00851ebf4344b726a80c23f7b052ff8f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/sty0/defs.ma".
 
 include "Basic-2/getl/drop.ma".
 
-inline procedural "Basic-1/sty0/props.ma".
+inline "Basic-1/sty0/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma
index 2ed64e8da57d8f62a5bc09b916eff5a5b232df86..062ba4446a159f72e544c831b519b5a83975278f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma
@@ -18,5 +18,5 @@ include "Basic-2/sty1/props.ma".
 
 include "Basic-2/cnt/props.ma".
 
-inline procedural "Basic-1/sty1/cnt.ma".
+inline "Basic-1/sty1/cnt.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma
index bf2b520fa930d562ab6a994512007e3eb6213bc7..f764f229a99509618049293dd0676b2bb9379699 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/sty1/defs.ma".
 
 include "Basic-2/sty0/props.ma".
 
-inline procedural "Basic-1/sty1/props.ma".
+inline "Basic-1/sty1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma
index 37db044610a226b35b3a1dc9be54695912c7336a..27b37067f314e3ec426a558e9425fb57912b2502 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/subst/defs.ma".
 
-inline procedural "Basic-1/subst/fwd.ma".
+inline "Basic-1/subst/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma
index 594ca5f8df7819a5d4b44b02d2ff518cac4217fd..1a45f22b59f0ebf819dd5bb7ad2da12819ee0473 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma
@@ -20,5 +20,5 @@ include "Basic-2/subst0/defs.ma".
 
 include "Basic-2/lift/props.ma".
 
-inline procedural "Basic-1/subst/props.ma".
+inline "Basic-1/subst/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma
index 6c7b887985ac537b0da48001a2f8b2a78595be9d..b6595349c94512dd256b4ca3b66a52888e4a7665 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma
@@ -18,5 +18,5 @@ include "Basic-2/subst0/defs.ma".
 
 include "Basic-2/lift/props.ma".
 
-inline procedural "Basic-1/subst0/dec.ma".
+inline "Basic-1/subst0/dec.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma
index 9e17f7c7357044975769d1a7b80ed621a56b7ef6..3da14bb5ea682965d18749dc1e75d3a145ab1984 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/subst0/defs.ma".
 
 include "Basic-2/lift/props.ma".
 
-inline procedural "Basic-1/subst0/fwd.ma".
+inline "Basic-1/subst0/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma
index 88bbcf44b45bd3c4704073e076b8e31fb03e351e..155ba9e4ff8700eb22da6ef25a4f378c942f4c3a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/subst0/fwd.ma".
 
-inline procedural "Basic-1/subst0/props.ma".
+inline "Basic-1/subst0/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma
index fa45dec2830bf12512b9b72c6ecfb966cbe4b35c..3e87d456004818a8d47d8b1b26d051a2e17a7187 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/subst0/props.ma".
 
-inline procedural "Basic-1/subst0/subst0.ma".
+inline "Basic-1/subst0/subst0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma
index fa103084e7a0d3d77fe880e08d63b9f49c08a5ea..6583c3c9212754c13adf6fb5b12277c95fc0d05b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma
@@ -20,5 +20,5 @@ include "Basic-2/lift/props.ma".
 
 include "Basic-2/lift/tlt.ma".
 
-inline procedural "Basic-1/subst0/tlt.ma".
+inline "Basic-1/subst0/tlt.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma
index 14fce8c8f79f8d2cc3f2a0c5cdf271885c537fe3..78669f892c4810690a943dca15f744e1f56ab9bb 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/subst1/defs.ma".
 
 include "Basic-2/subst0/props.ma".
 
-inline procedural "Basic-1/subst1/fwd.ma".
+inline "Basic-1/subst1/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma
index 3ff04ea10e7aba6fe7195390497db990ed9859b0..35ae5d43de89ce023a77d1520f16d2603706095a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/subst1/defs.ma".
 
 include "Basic-2/subst0/props.ma".
 
-inline procedural "Basic-1/subst1/props.ma".
+inline "Basic-1/subst1/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma
index 83161a5f294d8e5bfd52a742facec2832b8c4764..af3f3576196fb3501ad5feeaad24d34d0ea4ee20 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma
@@ -18,5 +18,5 @@ include "Basic-2/subst1/fwd.ma".
 
 include "Basic-2/subst0/subst0.ma".
 
-inline procedural "Basic-1/subst1/subst1.ma".
+inline "Basic-1/subst1/subst1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma
index 565faf6f79c17246a97730c6b4bbaa30e882a6df..4fcfcb1fbb44825b0640217a3053e587ee086a51 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/tlist/defs.ma".
 
-inline procedural "Basic-1/tlist/props.ma".
+inline "Basic-1/tlist/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma
index 70a1a12f1a03dcb34653b095c4bb0ea448286fc1..75aff34af9da9273ee44304915f7ab499ae356dd 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/tlt/defs.ma".
 
-inline procedural "Basic-1/tlt/props.ma".
+inline "Basic-1/tlt/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma
index 73842ed6db04bc7870a9e2327689e3ec9b507731..a50d253400cf8223af6cdf8c24e7b871bd68db3f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma
@@ -20,5 +20,5 @@ include "Basic-2/arity/pr3.ma".
 
 include "Basic-2/asucc/fwd.ma".
 
-inline procedural "Basic-1/ty3/arity.ma".
+inline "Basic-1/ty3/arity.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma
index 0d89905525d3a071fa4f7c00740bc09e118b4367..65475e81cd33a8e345b339c9c56b7204c5ae0593 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma
@@ -18,5 +18,5 @@ include "Basic-2/ty3/arity.ma".
 
 include "Basic-2/sc3/arity.ma".
 
-inline procedural "Basic-1/ty3/arity_props.ma".
+inline "Basic-1/ty3/arity_props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma
index f6d6c60110b715e337198906a8b9ec6f8efe8b6d..da5291990df5994dca2c80877084bb155e91b9b1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma
@@ -20,5 +20,5 @@ include "Basic-2/getl/flt.ma".
 
 include "Basic-2/getl/dec.ma".
 
-inline procedural "Basic-1/ty3/dec.ma".
+inline "Basic-1/ty3/dec.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma
index 6055c0c1a1e1715b31a40d6c28d04cb39b19d8d5..11b8873da9bbd9c247d23ad0ee661d7c4db9afc0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma
@@ -20,5 +20,5 @@ include "Basic-2/pc3/fsubst0.ma".
 
 include "Basic-2/getl/getl.ma".
 
-inline procedural "Basic-1/ty3/fsubst0.ma".
+inline "Basic-1/ty3/fsubst0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma
index b23abe7ddba0c50064b84c82159b65e0c97df828..c019d001ab77b59b4642398ac2840b3df8e1cc05 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma
@@ -18,5 +18,5 @@ include "Basic-2/ty3/defs.ma".
 
 include "Basic-2/pc3/props.ma".
 
-inline procedural "Basic-1/ty3/fwd.ma".
+inline "Basic-1/ty3/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma
index e5e5c669f9a0d36f6ac69041813fe9030dbf6771..6894ae46601c52817d52125bfb7eb401c580cc77 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma
@@ -20,5 +20,5 @@ include "Basic-2/pc3/nf2.ma".
 
 include "Basic-2/nf2/fwd.ma".
 
-inline procedural "Basic-1/ty3/fwd_nf2.ma".
+inline "Basic-1/ty3/fwd_nf2.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma
index b6ccdfe06c33526c87274dc576eb96093a170933..af79608554edd1508ede5a9a447d8567d6f8842a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma
@@ -20,5 +20,5 @@ include "Basic-2/pc3/nf2.ma".
 
 include "Basic-2/nf2/arity.ma".
 
-inline procedural "Basic-1/ty3/nf2.ma".
+inline "Basic-1/ty3/nf2.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma
index 143c7f1404358285717b97d3ee35c7f4ba01ce5b..dd43847bd42e811a582442c69b4f27a385c05f65 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma
@@ -26,5 +26,5 @@ include "Basic-2/pc3/wcpr0.ma".
 
 include "Basic-2/pc1/props.ma".
 
-inline procedural "Basic-1/ty3/pr3.ma".
+inline "Basic-1/ty3/pr3.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma
index df88edd872b68015385d9ea9f8d29cd791a13abb..a352ace498108c7542a59f0c32754c2398e5f2ac 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/ty3/pr3.ma".
 
-inline procedural "Basic-1/ty3/pr3_props.ma".
+inline "Basic-1/ty3/pr3_props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma
index 3dc7568c2d24ad0ef9fcfdb24970397a986a390a..c5e6cb33ee76911e82a82377b4009900c5dc4dfb 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/ty3/fwd.ma".
 
 include "Basic-2/pc3/fwd.ma".
 
-inline procedural "Basic-1/ty3/props.ma".
+inline "Basic-1/ty3/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma
index ad7ff0cfa64e9ac6be7caebe891e63d06797f813..0c5ebc151b2b6692df1323468839c5a683c01a3c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma
@@ -18,5 +18,5 @@ include "Basic-2/ty3/pr3_props.ma".
 
 include "Basic-2/sty0/fwd.ma".
 
-inline procedural "Basic-1/ty3/sty0.ma".
+inline "Basic-1/ty3/sty0.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma
index acdee271b1dfcf652d9e4e9c5047bfd904105782..97f45a1ec6b069a4324ea6658fa0dbae6771ee41 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma
@@ -20,5 +20,5 @@ include "Basic-2/pc3/subst1.ma".
 
 include "Basic-2/getl/getl.ma".
 
-inline procedural "Basic-1/ty3/subst1.ma".
+inline "Basic-1/ty3/subst1.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma
index 1dc828d8eb55f4f33af0067f984a63dd9c9084ca..0a9a8763806efb400571e7a082ca07b40da2394a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/wcpr0/defs.ma".
 
-inline procedural "Basic-1/wcpr0/fwd.ma".
+inline "Basic-1/wcpr0/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma
index 01c20904e78f6d98c6af8163fec56b3b82437a78..e412692e520f043a55d1c0a62c63dcf129ffd7d8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma
@@ -18,5 +18,5 @@ include "Basic-2/wcpr0/defs.ma".
 
 include "Basic-2/getl/props.ma".
 
-inline procedural "Basic-1/wcpr0/getl.ma".
+inline "Basic-1/wcpr0/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma
index d37a5f89d0c3353c27f88c8c8b83cc61098253c2..e63bb3e82431426e05677ea62c123429b0fa2e1d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/wf3/fwd.ma".
 
-inline procedural "Basic-1/wf3/clear.ma".
+inline "Basic-1/wf3/clear.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma
index 368615dab3cda12a25a617aec947d177560127b4..73bf245a71fc0a6a5f4fb574ec72e98128de3809 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/wf3/defs.ma".
 
-inline procedural "Basic-1/wf3/fwd.ma".
+inline "Basic-1/wf3/fwd.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma
index 1437739af90aa4b0823d7afee566a235d6f2c3e5..fe6e740421b8512c7ec409d01bc8c256bff93d19 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma
@@ -18,5 +18,5 @@ include "Basic-2/wf3/clear.ma".
 
 include "Basic-2/ty3/dec.ma".
 
-inline procedural "Basic-1/wf3/getl.ma".
+inline "Basic-1/wf3/getl.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma
index a26ff78ca43a2c780db21dc2dbfec10abdd633c4..35a6a64745ccda864f49f987ca2282817e5ae33e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma
@@ -18,5 +18,5 @@ include "Basic-2/wf3/ty3.ma".
 
 include "Basic-2/app/defs.ma".
 
-inline procedural "Basic-1/wf3/props.ma".
+inline "Basic-1/wf3/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma
index cf3cbd16018dd21e7bf14328e5a922450e9a91c1..8af324db592a785bf901e289dae786c0a73dd0d7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma
@@ -16,5 +16,5 @@
 
 include "Basic-2/wf3/getl.ma".
 
-inline procedural "Basic-1/wf3/ty3.ma".
+inline "Basic-1/wf3/ty3.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma
index fb23f304781667da2dd84de0480ffddd0c081110..24fd85f9644e041c5050cf84db4a179dab39e536 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma
@@ -16,5 +16,5 @@
 
 include "Ground-2/blt/defs.ma".
 
-inline procedural "Ground-1/blt/props.ma".
+inline "Ground-1/blt/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma
index 8cce7155be12259e3356163d3d5b3918c71e19b4..ab8a4c76e3b0d9fca534eb92e12a54e234d44efe 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma
@@ -16,5 +16,5 @@
 
 include "Ground-2/preamble.ma".
 
-inline procedural "Ground-1/ext/arith.ma".
+inline "Ground-1/ext/arith.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma
index 80924a6d3f60e148d347ab8e1c07d660ef4c4ede..72cacebfcd9d82d3fe5f32bab8a9196d3385dd04 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma
@@ -16,5 +16,5 @@
 
 include "Ground-2/preamble.ma".
 
-inline procedural "Ground-1/ext/tactics.ma".
+inline "Ground-1/ext/tactics.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma
index 97eea3400e95f9bdfdeb66e7949dc5bb4b941832..196cf33a7149f19255c53f71e5943d8f8def44b7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma
@@ -16,5 +16,5 @@
 
 include "Ground-2/plist/defs.ma".
 
-inline procedural "Ground-1/plist/props.ma".
+inline "Ground-1/plist/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma
index e06bb4d91abce45c3ee01399e9a2b4c749887566..49444e73b1822ae5fea0416101de2afd536213d3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma
@@ -16,5 +16,5 @@
 
 include "Ground-2/types/defs.ma".
 
-inline procedural "Ground-1/types/props.ma".
+inline "Ground-1/types/props.ma" procedural.
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma
index bd916f9cbbc34ec329d0c9df4d90a8651759bcbc..e214da177205fa74fa9a19b79db8887870f85047 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma
@@ -16,5 +16,5 @@
 
 include "Legacy-2/coq/defs.ma".
 
-inline procedural "Legacy-1/coq/props.ma".
+inline "Legacy-1/coq/props.ma" procedural.