X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Ffintype.ma;h=9b2dbadb94f3da231f4a4a8510ef40434dfdd7bd;hb=a180bddcd4a8f35de3d7292162ba05d0077723aa;hp=8f5de6e0aa85f5d9e445c2b86ed2b7705a4adba3;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index 8f5de6e0a..9b2dbadb9 100644
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -80,8 +80,8 @@ cases b; simplify;
 [2:intros (Hpt); apply H; intros; apply H1; simplify;
    generalize in match (refl_eq ? (cmp d x t));
    generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b1);
-   cases b1; simplify; intros; [2:rewrite > H2] auto.
-|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; auto]
+   cases b1; simplify; intros; [2:rewrite > H2] autobatch.
+|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
    rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin]
 qed.    
     
@@ -103,7 +103,7 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
       generalize in match (refl_eq ? (eqb n p));
       generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b); cases b; clear b; 
       intros (Enp); simplify;
-      [2:rewrite > IH; [1,3: auto]
+      [2:rewrite > IH; [1,3: autobatch]
          rewrite <  ltb_n_Sm in Hm; rewrite > Enp in Hm;
          generalize in match Hm; cases (ltb n p); intros; [reflexivity]
          simplify in H1; destruct H1;