...

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

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.