in the case of coerce_to_sort the whd was done with delta:true, that caused an incred...

[helm.git] / helm / software / matita / library / decidable_kit / fintype.ma

diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index ffd41d20615274559209b572b81d29a9d0884e22..9b2dbadb94f3da231f4a4a8510ef40434dfdd7bd 100644 (file)
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -46,7 +46,7 @@ rewrite < (leb_eqb x n); rewrite > H1; reflexivity;
 qed.
 
 lemma mem_filter :
-  ∀d1,d2:eqType.(*∀y:d1.*)∀x:d2.∀l:list d1.∀p:d1 → option d2.
+  ∀d1,d2:eqType.∀x:d2.∀l:list d1.∀p:d1 → option d2.
   (∀y.mem d1 y l = true → 
     match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
   mem d2 x (filter d1 d2 p l) = false.
@@ -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;