fixed many scripts that broke for various reasons

[helm.git] / helm / software / matita / nlibrary / logic / cologic.ma

diff --git a/helm/software/matita/nlibrary/logic/cologic.ma b/helm/software/matita/nlibrary/logic/cologic.ma
index ca4921607b6b5d4d5ec1e232f63b3be1ca4a54de..8b9ed3c15d450c622d78eb42294f43a98d145922 100644 (file)
--- a/helm/software/matita/nlibrary/logic/cologic.ma
+++ b/helm/software/matita/nlibrary/logic/cologic.ma
@@ -95,7 +95,7 @@ ntheorem cand_true: ∀c1,c2. ceq c1 (certain true) → ceq (cand c1 c2) c2.
            ##[ nlapply (KK2 EE); #XX; nrewrite > (cand_truer …) in XX; #YY;
                @3;
                
-           ##[ nrewrite > (ccases (cand (maybe xx) (certain true)));
+           rewrite > (ccases (cand (maybe xx) (certain true)));
                nnormalize; @3; @2;