Elimination principles are now processed in O(1) again

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / aux_bases.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
index a4707a5d5db8a6c89cd11dfa28010b547fe98a81..58898142df2d18944b47cc8d6b660c47f34a7da2 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
@@ -37,7 +37,7 @@ ninductive oct : Type ≝
 | o6: oct
 | o7: oct.
 
-ndefinition oct_ind :
+(*ndefinition oct_ind :
  ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
 λP:oct → Prop.
 λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
@@ -57,7 +57,7 @@ ndefinition oct_rect :
 λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
  match n with
   [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
-
+*)
 (* operatore = *)
 ndefinition eq_oct ≝
 λn1,n2:oct.
@@ -136,7 +136,7 @@ ninductive bitrigesim : Type ≝
 | t1E: bitrigesim
 | t1F: bitrigesim.
 
-ndefinition bitrigesim_ind :
+(*ndefinition bitrigesim_ind :
  ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
                       P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
                       P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
@@ -183,7 +183,7 @@ ndefinition bitrigesim_rect :
   | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
   | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
   | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].  
-
+*)
 (* operatore = *)
 ndefinition eq_bitrig ≝
 λt1,t2:bitrigesim.