From 15a4250eae08063fc14e2448dcb90e55b4850384 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 23 Feb 2006 18:15:29 +0000
Subject: [PATCH] information on current compilation state added in each file

---
 matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma  | 2 ++
 matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma    | 4 +++-
 matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma    | 4 +++-
 matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma   | 2 ++
 matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma | 6 ++++--
 matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma | 2 ++
 matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma         | 2 ++
 matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma | 2 ++
 8 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index 3cb239174..62fc8bdfa 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: COMPILA *)
+
 (* Project started Wed Oct 12, 2005 ***************************************)
 
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs".
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index 7634cbde1..6773470b0 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: NON COMPILA: dev'essere aggiornato *)
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq".
 
 include "class_defs.ma".
@@ -27,4 +29,4 @@ qed.
 theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
 intros; elim H; clear H.; auto.
 qed.
-*)
\ No newline at end of file
+*)
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma
index c840fbdaf..1d6c763ab 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: NON COMPILA: attendo che l'oggetto "pippo" venga accettato *) 
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_defs".
 
 include "iff.ma".
@@ -58,4 +60,4 @@ definition bsup: \forall (P:COA). P \to P \to P \def
 
 inductive pippo : Prop \def
    | Pippo: let x \def zero in zero = x \to pippo.
-   
\ No newline at end of file
+   
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma
index 6c004073e..da2c1f678 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: NON COMPILA: perche' dipende da coa_defs *)
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_props".
 
 include "coa_defs.ma".
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma
index ed0afab4f..5bc9c2a7d 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma
@@ -12,10 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: NON COMPILA: dev'essere aggiornato *)
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_data".
 
-include "../../library/datatypes/constructors.ma".
-include "../../library/datatypes/bool.ma".
+include "datatypes/constructors.ma".
+include "datatypes/bool.ma".
 include "domain_defs.ma".
 
 (* QUANTIFICATION DOMAINS
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
index 68cbd01fa..dcdf84644 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: COMPILA *)
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs".
 
 include "class_defs.ma".
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
index 9a9491923..0e6205148 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: COMPILA *)
+
 set "baseuri" "cic:/matita/logic/iff".
 
 include "../../library/logic/connectives.ma".
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
index 5d872040a..7469f08af 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: NON COMPILA: dev'essere aggiornato *)
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs".
 
 include "domain_defs.ma".
-- 
2.39.2