diff options
Diffstat (limited to 'powerpc/Archi.v')
| -rw-r--r-- | powerpc/Archi.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 10dc5534..5d11aad1 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -27,11 +27,14 @@ Definition big_endian := true. Definition align_int64 := 8%Z. Definition align_float64 := 8%Z. -Definition splitlong := true. +(** Can we use the 64-bit extensions to the PowerPC architecture? *) +Parameter ppc64 : bool. + +Definition splitlong := negb ppc64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. Proof. - unfold splitlong, ptr64; congruence. + reflexivity. Qed. Program Definition default_pl_64 : bool * nan_pl 53 := @@ -51,7 +54,4 @@ Definition float_of_single_preserves_sNaN := true. Global Opaque ptr64 big_endian splitlong default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 - float_of_single_preserves_sNaN. - -(** Can we use the 64-bit extensions to the PowerPC architecture? *) -Parameter ppc64: bool. + float_of_single_preserves_sNaN.
\ No newline at end of file |