The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

> (* The actual relations *)
> Add Parametric Relation : Type iso
>      reflexivity proved by ltac:(unfold Reflexive; iso)
>      symmetry proved by ltac:(unfold Symmetric; iso)
>      transitivity proved by ltac:(unfold Transitive; iso)
>        as iso_rel.
>
> Add Parametric Morphism : sum
>      with signature iso ==> iso ==> iso as sum_mor.
>    iso. Defined.
>
> Add Parametric Morphism : prod
>      with signature iso ==> iso ==> iso as prod_mor.
>    iso. Defined.

The problem does not come from ring but from the fact that the system
does not see iso as a setoid equality on Type.

Goal forall A B : Type, iso A B -> iso (A + A) (A + B).
intros A B H.
rewrite H.

Tactic failure: setoid rewrite failed: Unable to satisfy the following 
constraints...


--
Laurent.