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=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=e7665864fa08f343479f722ad629d67c0336a817;hpb=417792b30223b5edd4a9194193c7f34514bd0fa3;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 e7665864f..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
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -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)).