aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Archi.v
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/Archi.v')
-rw-r--r--mppa_k1c/Archi.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index a1664262..bbe66c5b 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -20,7 +20,7 @@ Require Import ZArith.
Require Import Fappli_IEEE.
Require Import Fappli_IEEE_bits.
-Parameter ptr64 : bool.
+Definition ptr64 := true.
Definition big_endian := false.