diff options
Diffstat (limited to 'arm/Archi.v')
| -rw-r--r-- | arm/Archi.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/arm/Archi.v b/arm/Archi.v index 6b282022..fedc55f5 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -20,7 +20,7 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. -Definition big_endian := false. +Parameter big_endian: bool. Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). @@ -45,8 +45,7 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p Definition float_of_single_preserves_sNaN := false. -Global Opaque big_endian - default_pl_64 choose_binop_pl_64 +Global Opaque default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. |