From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 8 Jun 2008 14:08:51 +0000 (+0000)
Subject: generalize no more useful for elim
X-Git-Tag: make_still_working~5061
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fc8cd675d2a0635463e7a5399a17dcbd1360c284;p=helm.git

generalize no more useful for elim
---

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index dff89f8d3..9c2f8890b 100644
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -170,7 +170,7 @@ intros (m n); apply bool_to_eq; split;
 [1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
     rewrite > (eqb_true_to_eq ? ? H1); simplify; 
     rewrite > leb_refl; reflexivity  
-|2: generalize in match m; clear m; elim n 0;
+|2: elim n in m ⊢ % 0;
     [1: simplify; intros; cases n1; reflexivity;
     |2: intros 1 (m); elim m 0;
         [1: intros; apply (p2bT ? ? (orbP ? ?));
diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma
index a38d5eb83..a7db00c72 100644
--- a/helm/software/matita/library/decidable_kit/list_aux.ma
+++ b/helm/software/matita/library/decidable_kit/list_aux.ma
@@ -58,8 +58,7 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ]
   apply (list_ind2 ? ? ? ? ? Hl); [1: intros; reflexivity]
   simplify; intros (tl1 tl2 hd1 hd2 IH H); cases (b2pT ? ? (andbP ? ?) H);
   rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity
-| generalize in match H; clear H; generalize in match l2; clear l2;
-  elim l1 1 (l1 x1);
+| elim l1 in H l2 ⊢ % 1 (l1 x1);
    [ cases l1; simplify; [intros; destruct H | unfold Not; intros; destruct H1;]
    | intros 3 (tl1 IH l2); cases l2;
      [ unfold Not; intros; destruct H1;