From a3558b92aa7395b2c841c737d867bbe02c848e03 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 1 Mar 2019 18:19:27 +0000
Subject: Coq: some library compatibility changes

---
 lib/coq/Sail2_string.v  | 3 +++
 src/pretty_print_coq.ml | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index 0a00f8d7..543b0fad 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -188,3 +188,6 @@ Definition decimal_string_of_bv {a} `{Bitvector a} (bv : a) : string :=
 Definition decimal_string_of_bits {n} (bv : mword n) : string := decimal_string_of_bv bv.
 
 
+(* Some aliases for compatibility. *)
+Definition dec_str := string_of_int.
+Definition concat_str := String.append.
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index d323d639..42780012 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1096,7 +1096,7 @@ let condition_produces_constraint exp =
    dependent pair with a proof that the result is the expected integer.  This
    is redundant for basic arithmetic functions and functions which we unfold
    in the constraint solver. *)
-let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"; "length";
+let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "Z.rem"; "length_mword"; "length";
                       "negb"; "andb"; "orb";
                       "Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"]
 
-- 
cgit v1.2.3