1) \ldots here and there

[helm.git] / helm / software / matita / contribs / assembly / freescale / word16.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/word16.ma b/helm/software/matita/contribs/assembly/freescale/word16.ma
index 98d7703b636db370c1b85225f423986b4c3379d2..d5bdd68bf06aed722d91093953f1a36ce053468b 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/assembly/freescale/word16.ma
@@ -39,8 +39,7 @@ record word16 : Type ≝
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
  for @{ 'mk_word16 $x $y }.
-interpretation "mk_word16" 'mk_word16 x y = 
- (cic:/matita/freescale/word16/word16.ind#xpointer(1/1/1) x y).
+interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
 
 (* operatore = *)
 definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).
@@ -151,7 +150,7 @@ definition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
 (* word → naturali *)
 definition nat_of_word16 ≝ λw:word16. 256 * (w16h w) + (nat_of_byte8 (w16l w)).
 
-coercion cic:/matita/freescale/word16/nat_of_word16.con.
+coercion nat_of_word16.
 
 (* naturali → word *)
 definition word16_of_nat ≝