refactoring completed!

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
index cfd51af8aa87f32aac8b51ae9ce27f26a9b3d94d..878e270488784e07866f20f0cb39c09ac5e50821 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/reduction/tpr.ma".
+include "Basic-2/reduction/tpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lpr.ma
index 92f77215c1fb4c55a6f4c4e45f8fa8e4731e3fa9..a08a65377cd58031ee8a49393c1ee8d95f8f3246 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lpr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/reduction/tpr.ma".
+include "Basic-2/reduction/tpr.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
index fbf4d47c4a51a38b025333ee62a297d2dfd91b67..54564f7967f64ff16ecc39507b609f54b6d47e75 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/tps.ma".
+include "Basic-2/substitution/tps.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
index e6fd9645459ec3e57ff10f855cc313eb051d6953..7bb90c2fcb9bb9345df7b7bdda84be9a3adc6220 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/substitution/tps_lift.ma".
-include "lambda-delta/reduction/tpr.ma".
+include "Basic-2/substitution/tps_lift.ma".
+include "Basic-2/reduction/tpr.ma".
 
 (* Relocation properties ****************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
index ee22bfc21f11dfdd0199e52344f767a9a84d7fbf..140eeb33499fcf2bd19400e4f7c6fac335571a95 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
@@ -9,10 +9,10 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/lift_weight.ma".
-include "lambda-delta/substitution/tps_tps.ma".
-include "lambda-delta/reduction/tpr_lift.ma".
-include "lambda-delta/reduction/tpr_tps.ma".
+include "Basic-2/substitution/lift_weight.ma".
+include "Basic-2/substitution/tps_tps.ma".
+include "Basic-2/reduction/tpr_lift.ma".
+include "Basic-2/reduction/tpr_tps.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
index 96bc9b76ebaad9523456f06e711b5ce8e297ed8f..6fae790d80e23ed26bb728d13ea625d6696561e6 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/reduction/lpr.ma".
+include "Basic-2/reduction/lpr.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma
index 29b57405fd5da4fb82d01ef8f9367a8947fa5498..dccc186e1c1c37691e849ea29b06bcea292f4629 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma
@@ -9,8 +9,8 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/leq.ma".
-include "lambda-delta/substitution/lift.ma".
+include "Basic-2/substitution/leq.ma".
+include "Basic-2/substitution/lift.ma".
 
 (* DROPPING *****************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma
index 812fb7e06bf1c449d1b2a2a339c59847d4cb6966..03a8e31ddaf9a7a1cf856f609c7bec2bff3359dd 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/substitution/lift_lift.ma".
-include "lambda-delta/substitution/drop.ma".
+include "Basic-2/substitution/lift_lift.ma".
+include "Basic-2/substitution/drop.ma".
 
 (* DROPPING *****************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma
index b0e28d48e42701b41f2f1c46899ae5ab6949868f..e843982cdd6413d7efb6976cf5ddb72c8512b7ad 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/syntax/length.ma".
+include "Basic-2/syntax/length.ma".
 
 (* LOCAL ENVIRONMENT EQUALITY ***********************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma
index a5b15e1100d74da3278a51f706b50aa1bc729554..c6ec4033ffa7e4b2a262b5d52d3e7cadc9f0880e 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/syntax/term.ma".
+include "Basic-2/syntax/term.ma".
 
 (* RELOCATION ***************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_lift.ma
index 205eab2bfdb84c861c903edd77703be23f845c12..ba69f0f714bd626871f3a365d18b12ebe63c9419 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/substitution/lift.ma".
+include "Basic-2/substitution/lift.ma".
 
 (* RELOCATION ***************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_weight.ma
index eafa007059aab0030d4d0b4de2d9aea2f5b6caea..84c8fef1d9bc9063ddd9034ee2a90ea85710e7c0 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_weight.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_weight.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/syntax/weight.ma".
-include "lambda-delta/substitution/lift.ma".
+include "Basic-2/syntax/weight.ma".
+include "Basic-2/substitution/lift.ma".
 
 (* RELOCATION ***************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
index 56d8f32118d77b893745692aa78b566470ab39c6..cf20a0056515b54bfb68eabad50420f9d3cac023 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/drop.ma".
+include "Basic-2/substitution/drop.ma".
 
 (* PARTIAL SUBSTITUTION ON TERMS ********************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
index 1f8d7a88c0d6e8bb94289881cb4bcc71e54321c5..06d1029459a04da70c1a5243a10d55a4582031f8 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
@@ -9,8 +9,8 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/drop_drop.ma".
-include "lambda-delta/substitution/tps.ma".
+include "Basic-2/substitution/drop_drop.ma".
+include "Basic-2/substitution/tps.ma".
 
 (* PARTIAL SUBSTITUTION ON TERMS ********************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma
index 23cdb39df0d13c43936d3b69aa8bbf3b383ade03..8d093e46bf58e14e7f5ffbeb4fc35835e4431185 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/tps_lift.ma".
+include "Basic-2/substitution/tps_lift.ma".
 
 (* PARTIAL SUBSTITUTION ON TERMS ********************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
index c1faa23f47f3748abaafedcf29b86988327755fd..7143620d18a9743dcdc087a0009582f3c1e67d1c 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/tps_split.ma".
+include "Basic-2/substitution/tps_split.ma".
 
 (* PARTIAL SUBSTITUTION ON TERMS ********************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma
index ea7a45362dac2305b999ac934e5f2b235a474c29..c3613eb0c52207be5b89df100983de3c7f766f9c 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma
@@ -15,8 +15,8 @@
  * [ suggested invocation to start formal specifications with ]
  *)
 
-include "lambda-delta/ground.ma".
-include "lambda-delta/notation.ma".
+include "Ground-2/ground.ma".
+include "Basic-2/notation.ma".
 
 (* BINARY ITEMS *************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/length.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/length.ma
index 91e1bd78c01aa5d8274920530a81698acbe153f9..dfe1261cd17cc21045730feb7558e2a016d61a07 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/length.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/syntax/length.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/syntax/lenv.ma".
+include "Basic-2/syntax/lenv.ma".
 
 (* LENGTH *******************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/lenv.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/lenv.ma
index c3aab910b1abfe44984d8fcc0f42d8c30a3c9cfb..f8fc80668236d31760ad54556139ec78b5c149a4 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/lenv.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/syntax/lenv.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/syntax/term.ma".
+include "Basic-2/syntax/term.ma".
 
 (* LOCAL ENVIRONMENTS *******************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/sh.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/sh.ma
index 32840edff0940c9d5742f14b2c79b9e92df372ec..99d1848fbf22604f1077b67de01c6b06fbde3b43 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/sh.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/syntax/sh.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/ground.ma".
+include "Ground-2/ground.ma".
 
 (* SORT HIERARCHY ***********************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/term.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/term.ma
index fe84e54b42b83efc5ae2eb645b1da4c28b25c04a..b1c18e6e7eaa36afd3b003c84fe4db83df0ea8a1 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/term.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/syntax/term.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/syntax/item.ma".
+include "Basic-2/syntax/item.ma".
 
 (* TERMS ********************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma
index d076dea9d68734c30b00667001d6a4eafd0b5032..82bd97aa0b75404bc69077d612aee15ddf23fe8f 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/syntax/lenv.ma".
+include "Basic-2/syntax/lenv.ma".
 
 (* WEIGHTS ******************************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Ground-2/ground.ma b/matita/matita/contribs/lambda-delta/Ground-2/ground.ma
index ed5876107932d6b84d027e9e97c6115da5fb5cd5..bf266c34722061ae41f8cb65e6f6b7a5f9a75c1c 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Ground-2/ground.ma
+++ b/matita/matita/contribs/lambda-delta/Ground-2/ground.ma
@@ -10,7 +10,7 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/nat.ma".
-include "lambda-delta/xoa_props.ma".
+include "Ground-2/xoa_props.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 

diff --git a/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml b/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml
index d25c5dcca99b364a83cdd7e92be2361120a67bde..f0ba4ec8175d4547c52afa845793cc913331f8fa 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml
+++ b/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml
@@ -10,8 +10,8 @@
 -->
   </section>
   <section name="xoa">
-    <key name="output_dir">lib/lambda-delta</key>
-    <key name="objects">xoa</key>    
+    <key name="output_dir">contribs/lambda-delta/Ground-2</key>
+    <key name="objects">xoa</key>
     <key name="notations">xoa_notation</key>
     <key name="include">basics/pts.ma</key>
     <key name="ex">2 1</key>

diff --git a/matita/matita/contribs/lambda-delta/Ground-2/xoa_props.ma b/matita/matita/contribs/lambda-delta/Ground-2/xoa_props.ma
index f07bc89be410715965dac9ac56f5f8cfcff6d659..f1ed781c30c93bbc1c5ab3f8bce81fecac6b146b 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Ground-2/xoa_props.ma
+++ b/matita/matita/contribs/lambda-delta/Ground-2/xoa_props.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda-delta/xoa_notation.ma".
-include "lambda-delta/xoa.ma".
+include "Ground-2/xoa_notation.ma".
+include "Ground-2/xoa.ma".
 
 lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
 #A0 #P0 #P1 * /2/

diff --git a/matita/matita/contribs/lambda-delta/Makefile b/matita/matita/contribs/lambda-delta/Makefile
index 8feb040dbe38b682bb43678b89f3d305462ba03c..b435949e3914b9916060db81d6976a27fd2e923a 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Makefile
+++ b/matita/matita/contribs/lambda-delta/Makefile
@@ -2,8 +2,8 @@ H       = @
 XOA_DIR = ../../../components/binaries/xoa
 XOA     = xoa.native
 
-CONF    = xoa.conf.xml
-TARGETS = xoa_natation.ma xoa.ma
+CONF    = Ground-2/xoa.conf.xml
+TARGETS = Ground-2/xoa_natation.ma Ground-2/xoa.ma
 
 all: $(TARGETS)