X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fo-algebra.ma;h=61a784605dfbaec75c5254a6e6fa1463bcc466c0;hb=2e97c767bc072f5ba238725ff1f738fc91a0135a;hp=70473755095490011616866e83c78f411fc36a22;hpb=716338697e54d7a7e3602aabdecc2a8a639d683e;p=helm.git

diff --git a/matita/matita/lib/formal_topology/o-algebra.ma b/matita/matita/lib/formal_topology/o-algebra.ma
index 704737550..61a784605 100644
--- a/matita/matita/lib/formal_topology/o-algebra.ma
+++ b/matita/matita/lib/formal_topology/o-algebra.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/core_notation/comprehension_2.ma".
 include "formal_topology/categories.ma".
 (*
 inductive bool : Type[0] := true : bool | false : bool.