diff options
| author | Brian Campbell | 2018-07-16 18:02:09 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-16 18:29:45 +0100 |
| commit | 0effbdd2468859924363fe00f29c0afcb727f065 (patch) | |
| tree | 60d2589168a5235aef9df07cd55d28846123b5f6 /src/pretty_print_coq.ml | |
| parent | 786ff327752c7fd26550d96ed2ba328f0facdb4a (diff) | |
Coq: we also unfold length
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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" |