From: Enrico Tassi Date: Mon, 22 Sep 2008 11:30:58 +0000 (+0000) Subject: fixed auto invocation X-Git-Tag: make_still_working~4753 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cbb17fc4b8fe935a576af81838f767fe138a2611;p=helm.git fixed auto invocation --- diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma index c1a8d5816..3478ef628 100644 --- a/helm/software/matita/library/decidable_kit/decidable.ma +++ b/helm/software/matita/library/decidable_kit/decidable.ma @@ -137,7 +137,7 @@ qed. lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m. intros (n m); apply bool_to_eq; split; intros (H); -[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch] +[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type] rewrite > (eqb_true_to_eq ? ? H1); autobatch |2:cases (b2pT ? ? (lebP ? ?) H); [ elim n; [reflexivity|assumption]