X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Fnat_to_num.ma;h=f93f82e8d94674a395a4a8ec8734f58bdf55422f;hb=826883e023c178930ca3dd69567eac23f15ef9c4;hp=6bd7fc4ae2191016c4c460ebef3174985429599e;hpb=5683cf231fa2ac8abade3b70aea1af995cc04379;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
index 6bd7fc4ae..f93f82e8d 100755
--- a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
@@ -75,4 +75,4 @@ nlet rec nat_of_w16_aux n (r:rec_word16 n) on r : nat ≝
 
 ndefinition nat_of_w16 : word16 → nat ≝ λn:word16.nat_of_w16_aux n (w16_to_recw16 n).
 
-ndefinition nat_of_w32 : word32 → nat ≝ λn:word32.(nat65536 * (nat_of_w16 (w32h n))) + (nat_of_w16 (w32l n)).
+ndefinition nat_of_w32 : word32 → nat ≝ λn:word32.(nat65536 * (nat_of_w16 (cnH ? n))) + (nat_of_w16 (cnL ? n)).