From 7a29aa43eb607d019699f0a76dc83e7093e5b222 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 26 Sep 2008 08:43:35 +0000
Subject: [PATCH] commented out a line that was making the file fail

---
 helm/software/matita/library/demo/formal_topology.ma | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 41c0d5c53..190e00e5d 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -172,8 +172,9 @@ definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 
 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 
+(*
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;
-   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
  }.
-
+*)
-- 
2.39.2