diff options
| author | Brian Campbell | 2018-09-05 16:44:44 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-06 17:57:23 +0100 |
| commit | 4e2d59f0af54d316ec343d02f25a065bcff259f8 (patch) | |
| tree | 764caab9829340153a2a2381260ef1bbe1574b3d /lib/coq/Sail2_prompt.v | |
| parent | eae01f8c348235ea552c67ce323a1ada3dbc8b08 (diff) | |
Coq: fix up some barrier/memory definitions for RISC-V
Diffstat (limited to 'lib/coq/Sail2_prompt.v')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 0f2c0955..12c1a9d9 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -128,3 +128,5 @@ Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad r Definition derive_m {rv e} {P Q:Z -> Prop} (x : monad rv {x : Z & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : Z & (ArithFact (Q x))} e := x >>= fun y => returnm (build_ex (projT1 y)). +Definition memea {rv e} {T:Type} (_:T) (_:Z) : monad rv unit e := returnm tt. +Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. |