diff options
| author | Brian Campbell | 2018-06-21 18:08:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-22 15:26:32 +0100 |
| commit | 3d8609d963ee411f777ba18dc24fe57bf39dcaab (patch) | |
| tree | d1aa9ec5b09181a2ed63001fa244a920a8113ba4 /lib/coq/Sail2_prompt.v | |
| parent | b550177c4987f6d20500818a6d6d091bb09b0871 (diff) | |
Coq: library updates, esp extending bitvector multiplies, Undefined
Diffstat (limited to 'lib/coq/Sail2_prompt.v')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 802fc302..336ca8de 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -48,7 +48,7 @@ match b with | BU => Fail "bool_of_bitU" end. -(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e +(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e*) Definition bool_of_bitU_oracle {rv E} (b : bitU) : monad rv bool E := match b with | B0 => returnm false @@ -57,7 +57,7 @@ match b with end. -val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> +(*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec whileM vars cond body = cond vars >>= fun cond_val -> |