freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index 416ad623ff02dd76e759b33daac378783ed2e843..bc81cac1707f2705242a0d4b31f287f7bdea9cfc 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -233,9 +233,12 @@ ndefinition div_w16 ≝
 (*    puo' essere sottratto al dividendo *) 
   | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 nat15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 nat15 ]].
 
-(* operatore x in [inf,sup] *)
+(* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_w32 ≝
-λx,inf,sup:word32.(le_w32 inf x) ⊗ (le_w32 x sup).
+λx,inf,sup:word32.
+ match le_w32 inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_w32 inf x) (le_w32 x sup).
 
 (* iteratore sulle word *)
 ndefinition forall_w32 ≝