predicative subsets started

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / ac_defs.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
index e4ee22311e194768818e6e9420dc57c3e0e83067..b375c69ada732dd06bc7926a945f3e59baada69b 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
@@ -30,7 +30,7 @@ include "coq.ma".
      of the aceq predicate given inside the category. Then we prove the 
      properties of the equality that usually are axiomatized inside the 
      category structure. This makes categories easier to use
-     *) 
+*) 
 
 record AC: Type \def {
    ac: Type;