diff options
| author | Brian Campbell | 2019-03-01 18:19:27 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-01 18:19:36 +0000 |
| commit | a3558b92aa7395b2c841c737d867bbe02c848e03 (patch) | |
| tree | ef6453108cc5f45c56d39de46f02a2f54945d765 | |
| parent | 3e2cd8de57d4bc865f6b8299dd4e5689b5e8b875 (diff) | |
Coq: some library compatibility changes
| -rw-r--r-- | lib/coq/Sail2_string.v | 3 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 2 |
2 files changed, 4 insertions, 1 deletions
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"] |