From 0effbdd2468859924363fe00f29c0afcb727f065 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 16 Jul 2018 18:02:09 +0100
Subject: Coq: we also unfold length

---
 src/pretty_print_coq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 62ff2b3b..7a31465d 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -753,7 +753,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_Z_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"]
+let no_Z_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"; "length"]
 
 let is_no_Z_proof_fn env id =
   if Env.is_extern id env "coq"
-- 
cgit v1.2.3