fixed according to the new rewrite semantics (fails if no progress)

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index 1b2b1fc42423554734d34cd74fa41b544e1fbfdc..dff89f8d35cc5d5d46a8539a9f8980b57fe2f70f 100644 (file)
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -82,7 +82,7 @@ qed.
 
 lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
 intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
-[1,2,3,4: rewrite > H; [1,2:right|3,4:left] reflexivity
+[1,2,3,4: try rewrite > H; [1,2:right|3,4:left] reflexivity
 |5,6,7,8: unfold Not; intros (H1); [2,3,4: destruct H]; cases H1; destruct H2]
 qed.
 

diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index 6bfa6969f1d38e223c1542b744990e82607e5bf6..82d54131bb494901801a8d3162382a76281b7fd6 100644 (file)
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -137,7 +137,7 @@ intros; cases a; cases b; reflexivity; qed.
 lemma uniq_tail : 
   ∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l).
 intros (d x l); elim l; simplify; [reflexivity]
-apply (cmpP d x t); intros (E); simplify ; rewrite > E; [reflexivity]
+apply (cmpP d x t); intros (E); simplify ; try rewrite > E; [reflexivity]
 rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
 rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
 qed.
@@ -155,9 +155,9 @@ intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3:
     [2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t);  
         intros (H5); simplify;
         [1: rewrite > count_O; [reflexivity]
-            intros (y Hy); rewrite > H5 in H2 H3 H4 ⊢ %; clear H5; clear x; 
+            intros (y Hy); rewrite > H5 in H2 H3 ⊢ %; clear H5; clear x; 
             rewrite > H2 in H4; destruct H4;
-         |2: simplify; rewrite > H5; simplify; apply H; 
+         |2: simplify; apply H; 
              rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); 
              assumption;]
     |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]