diff options
Diffstat (limited to 'mppa_k1c/Archi.v')
| -rw-r--r-- | mppa_k1c/Archi.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v index 800c9fe5..cdcf58c3 100644 --- a/mppa_k1c/Archi.v +++ b/mppa_k1c/Archi.v @@ -14,7 +14,7 @@ (* *) (* *********************************************************************) -(** Architecture-dependent parameters for RISC-V *) +(** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *) Require Import ZArith List. (*From Flocq*) |