freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index f2cbdb7583e7959eae5ebbe0182387ca84302d0d..260e49ad05a78b0299149c18bae1d4c2cbcb402f 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -91,10 +91,10 @@ ndefinition ror_b8 ≝
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
-  [ oc_O ⇒ b
-  | oc_S t n' ⇒ ror_b8_n (ror_b8 b) t n' ].
+nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+  [ O ⇒ b
+  | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_b8 ≝
@@ -117,10 +117,10 @@ ndefinition rol_b8 ≝
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
-  [ oc_O ⇒ b
-  | oc_S t n' ⇒ rol_b8_n (rol_b8 b) t n' ].
+nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+  [ O ⇒ b
+  | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_b8 ≝