From bc29be71041b83d3ff452d3dfe95b013f7d7bbe9 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 18 Jan 2007 21:55:14 +0000
Subject: [PATCH] Unified: refactoring

---
 .../LAMBDA-TYPES/Unified/SUB/C/defs.ma        | 10 +++---
 .../LAMBDA-TYPES/Unified/SUB/T/defs.ma        | 31 +++++++++++--------
 2 files changed, 23 insertions(+), 18 deletions(-)

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 2c8a14ff6..2b93d7783 100644
--- 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 798ace41d..df6e1945e 100644
--- 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
 .
-- 
2.39.2