X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft3.ma;h=4ab768fce53332f0d635b2e559b87c52c74e41d4;hb=65e8f1ba961ef81c5604168e7f1c891063c1ec76;hp=3c7489ba3aa384d98f80c007253e8c8c131dfe47;hpb=2e6a92bad35a8f8883c498c6a2f36ea3208d4ddd;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 3c7489ba3..4ab768fce 100644
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -214,7 +214,7 @@ ntheorem skipfact_partial:
  ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
  #n; nelim n; /2/;
  #m; nelim m; nnormalize
-     [ #H; @2; nnormalize; //;
+     [ #H; @2; nnormalize; ##[//;##] (* XXX: bug auto *)
        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
    ##| #p; #H1; #H2; @2; nnormalize; //;
        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;