Add coq builtins for MIPS

1 files changed, 6 insertions, 3 deletions

diff --git a/lib/smt.sail b/lib/smt.sail
index c9312819..efcbe48c 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -7,7 +7,8 @@ val div = {
   smt: "div",
   ocaml: "quotient",
   lem: "integerDiv",
-  c: "tdiv_int"
+  c: "tdiv_int",
+  coq: "div_with_eq"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
 
 overload operator / = {div}
@@ -16,7 +17,8 @@ val mod = {
   smt: "mod",
   ocaml: "modulus",
   lem: "integerMod",
-  c: "tmod_int"
+  c: "tmod_int",
+  coq: "mod_with_eq"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
 
 overload operator % = {mod}
@@ -25,7 +27,8 @@ val abs_atom = {
   smt : "abs",
   ocaml: "abs_int",
   lem: "abs_int",
-  c: "abs_int"
+  c: "abs_int",
+  coq: "abs_with_eq"
 } : forall 'n. atom('n) -> {'o, 'o = abs_atom('n). atom('o)}
 
 $ifdef TEST