The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Hello,

I managed to reduce my issue to the joint example.
I didn't succeed to reduce it further (e.g. using directly Type 
Classes). I still hope someone will be able to tell me what's happening 
here, and whether there is a reason it doesn't work or if it's a bug.

Cheers,
--
Cyril Cohen
Require Import Relation_Definitions Setoid Morphisms.

Variable A : Type.

Structure str := Str { sort :> Type }.

Structure str' := Str' { sort' :> Type }.
Canonical Structure str_str' (T : str) := Str' T.

Variable eqT : forall T : str, T -> T -> Prop.
Variable op : forall T : str', T  -> bool.

Add Parametric Relation (T : str) : T (eqT T)
  reflexivity proved by _
  symmetry proved by _
  transitivity proved by _ as eqT_rel.
Proof. Admitted.

Add Parametric Morphism (T : str) : (op (str_str' T))
with signature (@eqT _ ==> @eq _)%signature as eqT_op.
Admitted.

(* Here comes the problem *)
Goal forall (T : str) (a b : T), eqT _ a b -> 
  op _ b = true -> op _ a = true.
Proof.
intros T a b eab ob.
rewrite eab.
(* rewrite eab. (* <= it doesn't work with op *) *)
Abort.