X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fbyte8.ma;h=dfff4c8a80e883a04467196392e85de986f19592;hb=130f4d89a3c3d00840f584e7ab0c0dd87d27f91e;hp=fd412e59e70d5e5347de8f1c9e7e5b35fc718e74;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma
index fd412e59e..dfff4c8a8 100644
--- a/helm/software/matita/contribs/assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/assembly/freescale/byte8.ma
@@ -39,8 +39,7 @@ record byte8 : Type ≝
 (* \langle \rangle *)
 notation "〈x,y〉" non associative with precedence 80
  for @{ 'mk_byte8 $x $y }.
-interpretation "mk_byte8" 'mk_byte8 x y = 
- (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
+interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
 
 (* operatore = *)
 definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
@@ -151,7 +150,7 @@ definition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
 (* byte → naturali *)
 definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
 
-coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
+coercion nat_of_byte8.
 
 (* naturali → byte *)
 definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).
@@ -407,12 +406,12 @@ theorem plusb8nc_ok:
  generalize in match (plusb8_ok b1 b2 false);
  elim (plus_b8 b1 b2 false);
  simplify in H ⊢ %;
- change with (nat_of_byte8 t = (b1 + b2) \mod 256);
+ change with (nat_of_byte8 a = (b1 + b2) \mod 256);
  rewrite < plus_n_O in H;
  rewrite > H; clear H;
  rewrite > mod_plus;
- letin K ≝ (eq_nat_of_byte8_mod t); clearbody K;
- letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
+ letin K ≝ (eq_nat_of_byte8_mod a); clearbody K;
+ letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool b) 256 ?); clearbody K';
   [ autobatch | ];
  autobatch paramodulation.
 qed.