information on current compilation state added in each file

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index 3cb2391742186f2450bfe3b24fa014e3bae0058c..62fc8bdfa3047eb47b32990fd09771fed91f6b34 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
+++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index 7634cbde1171f65fa92d126eea1c8a872fc2f971..6773470b0bf1cce469498fb0dacb4a6a15bcefda 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma
index c840fbdaf7cddc972b4f3cdade571c5b2aa84dd4..1d6c763abd9105f6e2b670cfa5886fdc63128adf 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma
+++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma
index 6c004073e7390e4c2fe172cb105316be13911763..da2c1f678e3a8d1f711a8b1a162fb762405c89ab 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma
+++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma
index ed0afab4fd054c22d90e60d4b87cea55182842d1..5bc9c2a7d44b0be9422be003316811b3d991947f 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma
+++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
index 68cbd01fa8d962b3d0a829959f45266dfbb971f0..dcdf8464427dc9e941b31ec184315c8cc407a518 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
+++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
index 9a9491923f889afb28808116a23eb121fa77473c..0e6205148d0de93c0de50e48c8d96becc186ed82 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
+++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
index 5d872040a403d9c9466424d9d956742eeb040a65..7469f08afd371eb99e0ad1359e2ec1b8801c8317 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
+++ b/helm/software/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".