summaryrefslogtreecommitdiff
path: root/lib/smt.sail
diff options
context:
space:
mode:
Diffstat (limited to 'lib/smt.sail')
-rw-r--r--lib/smt.sail4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/smt.sail b/lib/smt.sail
index c57f7bd1..7006b190 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -8,7 +8,7 @@ val div = {
ocaml: "quotient",
lem: "integerDiv",
c: "tdiv_int",
- coq: "div_with_eq"
+ coq: "ediv_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
overload operator / = {div}
@@ -18,7 +18,7 @@ val mod = {
ocaml: "modulus",
lem: "integerMod",
c: "tmod_int",
- coq: "mod_with_eq"
+ coq: "emod_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
overload operator % = {mod}