Scripts fixed. They were broken since the change to the behaviour of CicMetaSubst...

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 0c7bd0b641914886a1ad659291da5b12eaff545c..766f9a6a73e457ae1d6e9630c9661b8bacec8eb5 100644 (file)
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -93,6 +93,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -161,6 +162,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -395,6 +397,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
       assumption
     ]
   | intros;
+    unfold f;
     apply index_of_sur
   ] 
 ].

diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index 9c5e1a843c6f1934ca91801b5ade553efbcf3ed5..9223400e7a418c842df929e71340f5e1c931a6d6 100644 (file)
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -84,11 +84,13 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
  [ apply (mk_finType fsort enum Hcut)
  | intros (x); cases x (n Hn); simplify in Hn; clear x;
    generalize in match Hn; generalize in match Hn; clear Hn;
+   unfold enum;
    unfold segment_enum;
    generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
    intros 1 (m); elim m  (Hm Hn p IH Hm Hn); [ simplify in Hm; destruct Hm ]
    simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
-   [1:unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
+   [1:unfold fsort;
+      unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
       unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
       simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
       [2:rewrite > IH; [1,3: autobatch]