From de7648541633d2b98a65ba340b39494ddb66b28e Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Sat, 1 Aug 2009 10:49:14 +0000
Subject: [PATCH]  freescale porting, work in progress

---
 helm/software/matita/contribs/ng_assembly/freescale/word16.ma | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
index 7dd405eeb..86e6629dc 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
@@ -369,7 +369,9 @@ ndefinition w16_to_recw16_aux3 ≝
  ].
 
 nlemma w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉.
- #n; #e; nelim e; #input; napply (w16_S ? input).
+ #n; #e; nelim e;
+ (* napply (exadecim_ind … e); funziona *)
+ #input; napply (w16_S ? input).
 nqed.
 
 nlemma w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉.
-- 
2.39.2