Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.

lib/Integers.v: added more properties for ARM port.
lib/Coqlib.v: added more properties for division and powers of 2.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@928 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 4 insertions, 4 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 22139127..14b8053d 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -351,10 +351,10 @@ Definition sem_binary_operation
 
 Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
   match sz, sg with
-  | I8, Signed => Int.cast8signed i
-  | I8, Unsigned => Int.cast8unsigned i
-  | I16, Signed => Int.cast16signed i
-  | I16, Unsigned => Int.cast16unsigned i 
+  | I8, Signed => Int.sign_ext 8 i
+  | I8, Unsigned => Int.zero_ext 8 i
+  | I16, Signed => Int.sign_ext 16 i
+  | I16, Unsigned => Int.zero_ext 16 i 
   | I32 , _ => i
   end.