Elimination principles are now processed in O(1) again

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
index 7cb39cd91f8a4e6c55314330949a480127545835..8ef0d523407dd0ca5c889ec7f9f4e4f43eee474f 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -76,7 +76,7 @@ full_info_of_word16_aux m borw (opcode_table m).
 ninductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
-ndefinition t_byte8_ind
+(*ndefinition t_byte8_ind
  : Πm:mcu_type.ΠP:t_byte8 m → Prop.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
 λm:mcu_type.λP:t_byte8 m → Prop.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
  match t with [ TByte (b:byte8) ⇒ f b ].
@@ -89,7 +89,7 @@ ndefinition t_byte8_rec
 ndefinition t_byte8_rect
  : Πm:mcu_type.ΠP:t_byte8 m → Type.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝
 λm:mcu_type.λP:t_byte8 m → Type.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m.
- match t with [ TByte (b:byte8) ⇒ f b ].
+ match t with [ TByte (b:byte8) ⇒ f b ].*)
 
 nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
  #m; #b1; #b2; #H;
@@ -173,7 +173,7 @@ ndefinition instr_mode_ind
   | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
   | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
 
-ndefinition instr_mode_rec
+(*ndefinition instr_mode_rec
  : Πi:instr_mode.ΠP:Πj.MA_check j → Set.
    P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) →
    (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) →
@@ -244,7 +244,7 @@ ndefinition instr_mode_rect
   | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b
   | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2
   | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ].
-
+*)
 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
    MA_check i → list (t_byte8 m) *)
 ndefinition args_picker ≝