diff options
Diffstat (limited to 'mppa_k1c/Archi.v')
| -rw-r--r-- | mppa_k1c/Archi.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v index 113f5d51..96571841 100644 --- a/mppa_k1c/Archi.v +++ b/mppa_k1c/Archi.v @@ -14,10 +14,9 @@ (* *) (* *********************************************************************) -(** Architecture-dependent parameters for RISC-V *) +(** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *) Require Import ZArith. -(*From Flocq*) Require Import Binary Bits. Definition ptr64 := true. |