freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index e75c80bd653c71c53955c2e2c2ea20d375eff6bd..62de47a89eb50603f63def979c402ab6f0c385e3 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -713,10 +713,10 @@ ndefinition ror_ex ≝
  | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
- match n with
-  [ O ⇒ e
-  | S n' ⇒ ror_ex_n (ror_ex e) n' ].
+nlet rec ror_ex_n (e:exadecim) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+  [ qu_O ⇒ e
+  | qu_S q' n' ⇒ ror_ex_n (ror_ex e) q' n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_ex ≝
@@ -762,10 +762,10 @@ ndefinition rol_ex ≝
  | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
- match n with
-  [ O ⇒ e
-  | S n' ⇒ rol_ex_n (rol_ex e) n' ].
+nlet rec rol_ex_n (e:exadecim) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+  [ qu_O ⇒ e
+  | qu_S q' n' ⇒ rol_ex_n (rol_ex e) q' n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_ex ≝