Old code commented out.

diff --git a/helm/software/matita/nlibrary/topology/igt.ma b/helm/software/matita/nlibrary/topology/igt.ma
index 3dbdda6f03d562b01302648d5c20f0cb9fb8b0f4..df888073357e4966f4bfadc22222b82ca5cd204b 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igt.ma
+++ b/helm/software/matita/nlibrary/topology/igt.ma
@@ -83,6 +83,7 @@ qed.
 
 *)
 
+(************************CSC
 nrecord function_space (A,B: setoid): Type[1] ≝
  { f:1> carr A → carr B}.;
    f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
@@ -245,3 +246,4 @@ definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
   |
   |
 *)
+*******************)
\ No newline at end of file