From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 9 Mar 2008 17:20:51 +0000 (+0000)
Subject: Scripts fixed. They were broken since the change to the behaviour of CicMetaSubst... 
X-Git-Tag: make_still_working~5551
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e291b4d0a99118cd0a1c5540ef00c25ca37a56d;p=helm.git

Scripts fixed. They were broken since the change to the behaviour of CicMetaSubst.delift w.r.t. definitions in the context.
---

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 0c7bd0b64..766f9a6a7 100644
--- 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 9c5e1a843..9223400e7 100644
--- 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]