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 /src | |
| parent | 3e2cd8de57d4bc865f6b8299dd4e5689b5e8b875 (diff) | |
Coq: some library compatibility changes
Diffstat (limited to 'src')
| -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 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"] |