Refine's unification fails in a symmetric case

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#1214
From: @roconnor
Reported version: trunk
CC: @pirbo

[coqbot]

Full_Name: Russell O'Connor
Version: 8.0pl3
OS: Linux
Submission from: n138230.science.ru.nl (131.174.138.230)

(* Lemma A and Lemma B are very similar lemmas.  Only the order of parameters
for equality are switched *)

Lemma A : forall x:bool, x=(if x then true else false).
Proof.
destruct x; reflexivity.
Qed.

Lemma B : forall x:bool, (if x then true else false)=x.
Proof.
destruct x; reflexivity.
Qed.

(* true=true correctly unifies with A *)

Goal true=true.
refine (A _).
Qed.

(* However unification fails with B *)

Goal true=true.
refine (B _).
(* Error: The term "B ?417" has type "(if ?417 then true else false) = ?417"
 while it is expected to have type "true = true" *)

(* I would expect unification with B to work as well.  *)

(* Actually, I would like apply A and apply B to both work, but perhaps that is
a separate bug. *)

[coqbot]

Le problème vient du fait que les Case sont considérés systématiquement
comme Rigid. Ainsi, dans le cas du refine (B _) il n'est pas possible de
d'attendre de résoudre ?x = true avant de résoudre if ?x then true else
false.

[ppedrot]

@herbelin Is this bug worth being kept open for such a long time?

[herbelin]

Yes, please, as a wish.

[maximedenes]

Yes, please, as a wish.

Who should I assign it to, then?