From 1ff56d44750c654daedab1227bf9df02cd8eb102 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 29 Aug 2019 16:54:45 +0100
Subject: Turn the two abs_int declarations into overloads (otherwise Sail uses
 the type from one and the extern from the other)

---
 lib/arith.sail | 4 +++-
 lib/smt.sail   | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/lib/arith.sail b/lib/arith.sail
index 7c002e1c..6b064433 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -96,7 +96,7 @@ val tmod_int = {
   coq: "Z.rem"
 } : (int, int) -> nat
 
-val abs_int = {
+val abs_int_plain = {
   smt : "abs",
   ocaml: "abs_int",
   interpreter: "abs_int",
@@ -105,4 +105,6 @@ val abs_int = {
   coq: "Z.abs"
 } : int -> int
 
+overload abs_int = {abs_int_plain}
+
 $endif
diff --git a/lib/smt.sail b/lib/smt.sail
index f58c008f..93fe0827 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -20,7 +20,7 @@ val emod_int = {
   coq: "emod_with_eq"
 } : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
 
-val abs_int = {
+val abs_int_atom = {
   ocaml: "abs_int",
   interpreter: "abs_int",
   lem: "abs_int",
@@ -28,6 +28,8 @@ val abs_int = {
   coq: "abs_with_eq"
 } : forall 'n. int('n) -> int(abs('n))
 
+overload abs_int = {abs_int_atom}
+
 $ifdef TEST
 
 let __smt_x : int(div(4, 2)) = div(8, 4)
-- 
cgit v1.2.3