# Consistently block `simpl` on all `Z` operations

We used to do this some operations (`Z.add`

, `Z.mul`

), but not for others (`Z.sub`

, `Z.of_nat`

); this MR blocks `simpl`

consistently for all operations involving `Z`

that I could think of.

The rationale for blocking everything is that `simpl`

produces very bad results, e.g. try:

```
Require Import ZArith.
Eval simpl in (fun n y => Z.of_nat (S n) + y)%Z.
(*
Yields:
fun (n : nat) (y : Z) =>
match y with
| 0%Z => Z.pos (Pos.of_succ_nat n)
| Z.pos y' => Z.pos (Pos.of_succ_nat n + y')
| Z.neg y' => Z.pos_sub (Pos.of_succ_nat n) y'
end
*)
```

Note that blocking `simpl`

for `Z.of_nat`

used to break `lia`

and `omega`

in the past, see https://github.com/coq/coq/issues/5039. For `lia`

this has been fixed, but for `omega`

not yet. However, in !37 (merged) we decided to use `lia`

everywhere in both std++ and Iris because it's faster, and moreover, I believe the Coq devs intend to deprecate `omega`

in favor of `lia`

in the future. So, I don't think we should care about `omega`

anymore.

I also updated the item "Side-effects" in the README to document that we block `simpl`

on `Z`

operations.

@jjourdan @jung Any objections to this MR?

I have fixes for Iris, iris-examples, Iron, lambdaRust (which are mostly a couple of one-liners). I thus would like to merge this ASAP (so I don't get merge conflicts on my fixes).