X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Fdecidable.ma;h=3478ef628e44c5871298100c970e3f36c9b05370;hb=b3e08a6954c8b6946f42f5c7e0bed7912d5ac87c;hp=9c2f8890b59d8a6cf294f693b27ba4dbda7bf194;hpb=fc8cd675d2a0635463e7a5399a17dcbd1360c284;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index 9c2f8890b..3478ef628 100644
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
 (* classical connectives for decidable properties *)
 
 include "decidable_kit/streicher.ma".
@@ -139,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]