diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-22 18:25:19 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-22 18:25:19 -0800 |
| commit | eaa9c30a44e6eedbe54e62994caedbb114924be8 (patch) | |
| tree | a8bcfea84ba09857bac3a5b29f8a106cba9f0bb0 | |
| parent | fadd57c7514709f94b90073640e7e9e600c46539 (diff) | |
| download | sail-riscv-eaa9c30a44e6eedbe54e62994caedbb114924be8.zip sail-riscv-eaa9c30a44e6eedbe54e62994caedbb114924be8.tar.gz sail-riscv-eaa9c30a44e6eedbe54e62994caedbb114924be8.tar.bz2 | |
Fix coq build.
| -rw-r--r-- | handwritten_support/riscv_extras.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 7e350ed..8d7cefc 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -145,6 +145,7 @@ 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. +Axiom sys_enable_fdext : unit -> bool. (* The constraint solver can do this itself, but a Coq bug puts anonymous_subproof into the term instead of an actual subproof. *) |