Unified: refactoring

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma
index 2c8a14ff65f2b0727a0599503f2ef099073e5c9b..2b93d77837c08149c2d82949d0a01945c7033277 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/C/defs".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Context/defs".
 
 (* FLAT CONTEXTS
    - Naming policy:
      - contexts: c d
 *)
 
-include "P/defs.ma".
+include "SUB/T/defs.ma".
 
-inductive C: Set \def
-   | top  : C
-   | entry: C \to Bind \to P \to C
+inductive Context: Set \def
+   | top  : Context
+   | entry: Context \to Bind \to Term \to Context
 .

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
index 798ace41d7340d1128fbeef7af7fb1e9fd7067ba..df6e1945ef8a7f3d71b64f2acba603399b9e5358 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
@@ -14,21 +14,27 @@
 
 (* Project started Tue Aug 22, 2006 ***************************************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/P/defs".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Term/defs".
 
 (* POLARIZED TERMS
    - Naming policy:
-     - natural numbers      : sorts h k, local references i j, lengths l
-     - boolean values       : a b
-     - generic binding items: x
-     - generic flat items   : y
-     - generic head items   : z
-     - terms                : p q
+     - natural numbers      : sorts h k, local references i j, lengths l o
+     - boolean values       : p q
+     - generic leaf items   : m n
+     - generic binding items: r s 
+     - generic flat items   : r s
+     - generic head items   : m n
+     - terms                : t u
 *)
 
 include "../../RELATIONAL/Nat/defs.ma".
 include "../../RELATIONAL/Bool/defs.ma".
 
+inductive Leaf: Set \def
+   | sort: Nat \to Leaf
+   | lref: Nat \to Leaf
+.
+
 inductive Bind: Set \def
    | abbr: Bind
    | abst: Bind
@@ -41,12 +47,11 @@ inductive Flat: Set \def
 .
 
 inductive Head: Set \def
-   | bind: Bind \to Head
-   | flat: Flat \to Head
+   | bind: Bool \to Bind \to Head
+   | flat: Bool \to Flat \to Head
 .
 
-inductive P: Set \def
-   | sort: Nat \to P
-   | lref: Nat \to P
-   | head: Bool \to Head \to P \to P \to P
+inductive Term: Set \def
+   | leaf: Leaf \to Term
+   | head: Head \to Term \to Term \to Term
 .