diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-26 17:32:16 +0000 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-26 17:32:16 +0000 |
| commit | 4809371012e7394853f01b179d088497212cf480 (patch) | |
| tree | f93fcc481bd58263e4e7168ba604c8d0f1d32384 /handwritten_support | |
| parent | fa707da94d0329e7d1b7520d876ad85953f2fdd5 (diff) | |
| download | sail-riscv-4809371012e7394853f01b179d088497212cf480.zip sail-riscv-4809371012e7394853f01b179d088497212cf480.tar.gz sail-riscv-4809371012e7394853f01b179d088497212cf480.tar.bz2 | |
Fix RV32 Coq build
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/mem_metadata.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v index ddb26e4..0e53888 100644 --- a/handwritten_support/mem_metadata.v +++ b/handwritten_support/mem_metadata.v @@ -4,8 +4,8 @@ Require Import Sail2_operators_mwords. Require Import Sail2_prompt_monad. Require Import Sail2_prompt. -Definition write_ram {rv e} wk (addr : mword 64) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk 64 addr size v. +Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v. -Definition read_ram {rv e} rk (addr : mword 64) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e := - read_mem rk 64 addr size >>= fun data => - returnm (data, tt).
\ No newline at end of file +Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e := + read_mem rk a addr size >>= fun data => + returnm (data, tt). |