From 1308bdc1fd4785e37f00e4436b2cd9f4c8e8fad7 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 29 May 2019 19:09:45 +0100
Subject: Coq: need a proof for _shr32

---
 lib/arith.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/arith.sail')

diff --git a/lib/arith.sail b/lib/arith.sail
index 1950080a..d04c7988 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -70,7 +70,7 @@ val _shl_int = "shl_int" : (int, int) -> int
 
 overload shl_int = {_shl8, _shl32, _shl_int}
 
-val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
+val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
 
 val _shr_int = "shr_int" : (int, int) -> int
 
-- 
cgit v1.2.3