λδ site update

[helm.git] / helm / software / matita / nlibrary / topology / igft4.ma

diff --git a/helm/software/matita/nlibrary/topology/igft4.ma b/helm/software/matita/nlibrary/topology/igft4.ma
index 9dbbbcf6c3e23060b0bfc1980ce4f90bef3d3ecf..f78b46e7945ddea896b16a00fbac5c48cb4edec2 100644 (file)
--- 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;