fixed many scripts that broke for various reasons

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

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 3c7489ba3aa384d98f80c007253e8c8c131dfe47..4ab768fce53332f0d635b2e559b87c52c74e41d4 100644 (file)
--- 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;