From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 10 Aug 2011 15:12:59 +0000 (+0000)
Subject: refactoring completed!
X-Git-Tag: make_still_working~2334
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b24e4faf4501e54da29dc70940101eeb160e9c9f;p=helm.git

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 cfd51af8a..878e27048 100644
--- 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 92f77215c..a08a65377 100644
--- 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 fbf4d47c4..54564f796 100644
--- 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 e6fd96454..7bb90c2fc 100644
--- 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 ee22bfc21..140eeb334 100644
--- 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 96bc9b76e..6fae790d8 100644
--- 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 29b57405f..dccc186e1 100644
--- 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 812fb7e06..03a8e31dd 100644
--- 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 b0e28d48e..e843982cd 100644
--- 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 a5b15e110..c6ec4033f 100644
--- 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 205eab2bf..ba69f0f71 100644
--- 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 eafa00705..84c8fef1d 100644
--- 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 56d8f3211..cf20a0056 100644
--- 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 1f8d7a88c..06d102945 100644
--- 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 23cdb39df..8d093e46b 100644
--- 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 c1faa23f4..7143620d1 100644
--- 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 ea7a45362..c3613eb0c 100644
--- 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 91e1bd78c..dfe1261cd 100644
--- 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 c3aab910b..f8fc80668 100644
--- 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 32840edff..99d1848fb 100644
--- 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 fe84e54b4..b1c18e6e7 100644
--- 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 d076dea9d..82bd97aa0 100644
--- 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 ed5876107..bf266c347 100644
--- 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 d25c5dcca..f0ba4ec81 100644
--- 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 f07bc89be..f1ed781c3 100644
--- 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 8feb040db..b435949e3 100644
--- 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)