From 476068e4c7ac989e42c84affbeeb95873edac24f Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 8 Feb 2007 15:33:29 +0000
Subject: [PATCH] Unified refactored

---
 .../LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Context/defs.ma   | 2 +-
 .../LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Inc/defs.ma       | 2 +-
 .../LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Lift/defs.ma      | 2 +-
 .../LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Term/defs.ma      | 2 +-
 .../contribs/LAMBDA-TYPES/{Unified => Unified-Sub}/makefile     | 2 +-
 .../LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/preamble.ma       | 0
 6 files changed, 5 insertions(+), 5 deletions(-)
 rename helm/software/matita/contribs/LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Context/defs.ma (97%)
 rename helm/software/matita/contribs/LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Inc/defs.ma (97%)
 rename helm/software/matita/contribs/LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Lift/defs.ma (98%)
 rename helm/software/matita/contribs/LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/Term/defs.ma (98%)
 rename helm/software/matita/contribs/LAMBDA-TYPES/{Unified => Unified-Sub}/makefile (95%)
 rename helm/software/matita/contribs/LAMBDA-TYPES/{Unified/SUB => Unified-Sub}/preamble.ma (100%)

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
similarity index 97%
rename from helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma
rename to helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
index 22763dd4f..7aca13a59 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
@@ -19,7 +19,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Context/defs".
      - contexts: c d
 *)
 
-include "SUB/Term/defs.ma".
+include "Term/defs.ma".
 
 inductive Context: Set \def
    | leaf: Context
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma
similarity index 97%
rename from helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
rename to helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma
index 4c4c9966d..d36f86abd 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Inc/defs".
 (* DISPLACEMENT INCREMENT RELATION
 *)
 
-include "SUB/Term/defs.ma".
+include "Term/defs.ma".
 
 inductive Inc (i:Nat): Bool \to Head \to Nat \to Prop \def
    | inc_bind: \forall r. Inc i true (bind r) (succ i)
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
similarity index 98%
rename from helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
rename to helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
index a6534047a..cf29a3562 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
    - Usage: invoke with positive polarity
 *)
 
-include "SUB/Inc/defs.ma".
+include "Inc/defs.ma".
 
 inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
    | lift_sort   : \forall l,q,i,h. 
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma
similarity index 98%
rename from helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
rename to helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma
index b73935a07..e08209626 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma
@@ -25,7 +25,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Term/defs".
      - terms                : t u
 *)
 
-include "SUB/preamble.ma".
+include "preamble.ma".
 
 inductive Leaf: Set \def
    | sort: Nat \to Leaf
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
similarity index 95%
rename from helm/software/matita/contribs/LAMBDA-TYPES/Unified/makefile
rename to helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
index d53547f4b..489485e6d 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
@@ -1,6 +1,6 @@
 H=@
 
-RT_BASEDIR=../../../
+RT_BASEDIR=/home/fguidi/svn/software/matita/
 OPTIONS=-bench
 MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
 CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
similarity index 100%
rename from helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma
rename to helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
-- 
2.39.2