summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBrian Campbell2020-08-29 22:31:59 +0100
committerBrian Campbell2020-09-07 13:40:24 +0100
commit300b517adb31ea4239812c1c47b59cef8a250c48 (patch)
tree4cdad9d8c0336e2f22ee04fb0b130dc5075cad4d
parent56ac810880fa48e9992dffba050f2f3acad0018c (diff)
Correct external declaration in mono_rewrites
-rw-r--r--lib/mono_rewrites.sail3
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 1e7fe58f..3efc028a 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -175,7 +175,8 @@ val _builtin_unsigned = {
ocaml: "uint",
lem: "uint",
interpreter: "uint",
- c: "sail_uint"
+ c: "sail_unsigned",
+ coq: "uint"
} : forall 'n. bits('n) -> {'m, 0 <= 'm < 2 ^ 'n. int('m)}
/* There are different implementation choices for division and remainder, but