Introduce and use the platform-specific Archi module giving:

- endianness
- alignment constraints for 8-byte types
    (which is 4 for x86 ABI and 8 for other ABIs)
- NaN handling options (superceding the Nan module, removed).


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

1 files changed, 13 insertions, 5 deletions

diff --git a/ia32/Nan.v b/ia32/Archi.v
index f3e777e..a2e136c 100644
--- a/ia32/Nan.v
+++ b/ia32/Archi.v
@@ -14,13 +14,21 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+(** Architecture-dependent parameters for IA32 *)
+
+Require Import ZArith.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
-Require Import Floats.
-Require Import ZArith.
-Require Import Integers.
 
-Program Definition default_pl : bool * nan_pl 53 := (true, nat_iter 51 xO xH).
+Definition big_endian := false.
+
+Notation align_int64 := 4%Z (only parsing).
+Notation align_float64 := 4%Z (only parsing).
+
+Program Definition default_pl : bool * nan_pl 53 := 
+  (true, nat_iter 51 xO xH).
 
 Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
-  false.                        (** always choose first NaN *)
+  false.                        (**r always choose first NaN *)
+
+Global Opaque big_endian default_pl choose_binop_pl.