diff options
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} : |