From 1c80d84c47faef38149e87e000c6721f6aa6245e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 9 Jan 2019 13:43:16 +0000
Subject: Coq: the division used in smt.sail should be Euclidean

---
 src/pretty_print_coq.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5cf17056..20db317b 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -239,9 +239,9 @@ let doc_nexp ctx ?(skip_vars=KidSet.empty) nexp =
   and app (Nexp_aux (n,l) as nexp) =
     match n with
     | Nexp_app (Id_aux (Id "div",_), [n1;n2])
-        -> separate space [string "Z.quot"; atomic n1; atomic n2]
+        -> separate space [string "ZEuclid.div"; atomic n1; atomic n2]
     | Nexp_app (Id_aux (Id "mod",_), [n1;n2])
-        -> separate space [string "Z.rem"; atomic n1; atomic n2]
+        -> separate space [string "ZEuclid.modulo"; atomic n1; atomic n2]
     | Nexp_app (Id_aux (Id "abs_atom",_), [n1])
         -> separate space [string "Z.abs"; atomic n1]
     | _ -> atomic nexp
-- 
cgit v1.2.3