Elimination principles are now processed in O(1) again

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / ascii.ma

diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
index 35894f57059fb31b1356a4bb516efc2d0a04cae1..38d2e7f53af303782a42df74b9cac4574ddaf96c 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
@@ -98,7 +98,7 @@ ninductive ascii : Type ≝
 | ch_y: ascii
 | ch_z: ascii.
 
-ndefinition ascii_ind
+(*ndefinition ascii_ind
  : ΠP:ascii → Prop.
    P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
    P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
@@ -149,7 +149,7 @@ ndefinition ascii_rect
   | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
   | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
   | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
-
+*)
 (* confronto fra ascii *)
 ndefinition eq_ascii ≝
 λc,c':ascii.match c with