diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2020-06-15 14:31:42 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2020-06-15 14:34:37 +0100 |
| commit | 2f3d4754770fc54634786937a3b1a6f7bd572af9 (patch) | |
| tree | 5e691de38150c0b32f2d155951127e3ce71d620a /handwritten_support/riscv_extras.v | |
| parent | 60e9b04db40028d93dfa62792af1dd524e5c6a60 (diff) | |
| download | sail-riscv-2f3d4754770fc54634786937a3b1a6f7bd572af9.zip sail-riscv-2f3d4754770fc54634786937a3b1a6f7bd572af9.tar.gz sail-riscv-2f3d4754770fc54634786937a3b1a6f7bd572af9.tar.bz2 | |
Remove obsolete Coq axiom
Diffstat (limited to 'handwritten_support/riscv_extras.v')
| -rw-r--r-- | handwritten_support/riscv_extras.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 7537349..02d5609 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -4,8 +4,6 @@ Require Import List. Import List.ListNotations. Open Scope Z. -Axiom real : Type. - Definition MEM_fence_rw_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_rw tt). Definition MEM_fence_r_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_rw tt). Definition MEM_fence_r_r {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_r tt). |