freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / word16.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index 1abaf059971ea2ca5c3486a62a5d26d8f353fcd5..6c1b21865168eb21c2619ea0ff2892657a3d31ee 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -224,7 +224,7 @@ ndefinition div_b8 ≝
 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
 (*    puo' essere sottratto al dividendo *) 
-  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
+  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]].
 
 (* operatore x in [inf,sup] *)
 ndefinition inrange_w16 ≝