X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft4.ma;h=f78b46e7945ddea896b16a00fbac5c48cb4edec2;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=9dbbbcf6c3e23060b0bfc1980ce4f90bef3d3ecf;hpb=711a6659027eb658e356bc4c3db3036306c2f19b;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft4.ma b/helm/software/matita/nlibrary/topology/igft4.ma
index 9dbbbcf6c..f78b46e79 100644
--- a/helm/software/matita/nlibrary/topology/igft4.ma
+++ b/helm/software/matita/nlibrary/topology/igft4.ma
@@ -214,7 +214,7 @@ ntheorem skipfact_partial:
   [ @2; nnormalize; //; #y; *; #a; ncases a
   |
  #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;