# stdpp breaks setoid rewriting

The setoid rewriting mechanism uses a bunch of typeclass machinery to infer `Proper`

instances for the contexts being rewritten in, and it uses `flip`

to talk about contravariance. stdpp breaks its ability to infer lots of cases it ordinarily can, because it makes `flip`

typeclass transparent when the setoid rewriting mechanism is built with the assumption that it is typeclass opaque! In `base.v`

, we have:

`Typeclasses Transparent id compose flip const.`

This nullifies the effect of the very first non-comment non-import line of `Classes/Init.v`

in the Coq stdlib:

`Typeclasses Opaque id const flip compose arrow impl iff not all.`

Here's a minimal demonstration of the problems this causes:

```
From Coq Require Import ssreflect ssrfun ssrbool.
Require Import Morphisms.
Require Import PeanoNat.
Instance plus_proper_le : Proper (le ++> le ++> le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
Require Import stdpp.base.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
Fail setoid_rewrite <- H1 in H2 at 1.
Abort.
Section FlippedInstance.
(* Thus seemingly necessitating: *)
Local Instance plus_proper_le' : Proper (le --> le --> flip le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
End FlippedInstance.
(* But alternatively: *)
Typeclasses Opaque flip.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
```