diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-04-04 10:52:40 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-04-04 10:52:40 +0100 |
| commit | f8322738c39246be7c83bfcd3dda2344ffaf862b (patch) | |
| tree | b43ab8ef8bd468d9bc4637f0c0ac57692d926e62 /handwritten_support/riscv_extras.v | |
| parent | 12951120dc3d1dab5750d80ae8809943259198e3 (diff) | |
| download | sail-riscv-f8322738c39246be7c83bfcd3dda2344ffaf862b.zip sail-riscv-f8322738c39246be7c83bfcd3dda2344ffaf862b.tar.gz sail-riscv-f8322738c39246be7c83bfcd3dda2344ffaf862b.tar.bz2 | |
Add `sys_enable_writable_misa` and `sys_enable_rvc` to Coq extras file
Diffstat (limited to 'handwritten_support/riscv_extras.v')
| -rw-r--r-- | handwritten_support/riscv_extras.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index ff235a9..cc68a54 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -134,6 +134,9 @@ Definition putchar {T} (_:T) : unit := tt. Require DecimalString. Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). +Axiom sys_enable_writable_misa : unit -> bool. +Axiom sys_enable_rvc : unit -> bool. + (* The constraint solver can do this itself, but a Coq bug puts anonymous_subproof into the term instead of an actual subproof. *) Lemma n_leading_spaces_fact {w__0} : |