Set `simpl never` for `Pos` and `N`.
Previously, we set simpl never for just Pos.mul and N.add. That's pretty inconsistent and annoying. For example:
Eval simpl in (2 + x)%positive.
(*
= match x with
| q~1 => match q with
| q0~1 => (Pos.succ q0)~0
| q0~0 => q0~1
| 1 => 2
end~1
| q~0 => match q with
| q0~1 => (Pos.succ q0)~0
| q0~0 => q0~1
| 1 => 2
end~0
| 1 => 3
end
: positive
*)
I copied the list of simpl never declarations for Z and removed the operations (e.g., opp) that are not available for N or Pos.
Edited by Robbert Krebbers