diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2020-06-15 14:23:09 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2020-06-15 14:34:37 +0100 |
| commit | 60e9b04db40028d93dfa62792af1dd524e5c6a60 (patch) | |
| tree | e64e1b65f6f98a6bf864ff17441682100b2aa3ea /handwritten_support/riscv_extras.v | |
| parent | f2cb2854616297a86a2dd8ab362a42b94970230b (diff) | |
| download | sail-riscv-60e9b04db40028d93dfa62792af1dd524e5c6a60.zip sail-riscv-60e9b04db40028d93dfa62792af1dd524e5c6a60.tar.gz sail-riscv-60e9b04db40028d93dfa62792af1dd524e5c6a60.tar.bz2 | |
Update handwritten Coq support files to match current Sail.
Diffstat (limited to 'handwritten_support/riscv_extras.v')
| -rw-r--r-- | handwritten_support/riscv_extras.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 8d7cefc..7537349 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -1,11 +1,8 @@ -Require Import Sail2_instr_kinds. -Require Import Sail2_values. -Require Import Sail2_operators_mwords. -Require Import Sail2_prompt_monad. -Require Import Sail2_prompt. +Require Import Sail.Base. Require Import String. Require Import List. Import List.ListNotations. +Open Scope Z. Axiom real : Type. |