[rewrite] with evars in the goal: Logic.RefinerError(_).

[RalfJung]

The following file triggers the following error with its last tactic:
Anomaly: cvtac's exception: Logic.RefinerError(_). Please report.

Require Export Program Setoid Utf8.
Require Export mathcomp.ssreflect.ssreflect.

(* -*- mode: coq; coq-prog-args: ("-emacs" "-Q" "." "" "-top" "cmra") -*- *)
(* File reduced by coq-bug-finder from original input, then from 1113 lines to 184 lines *)

Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity).
Notation "(≡)" := equiv (only parsing).
Class Assoc {A} (R : relation A) (f : A → A → A) : Prop :=
  assoc x y z : R (f x (f y z)) (f (f x y) z).

Class Op (A : Type) := op : A → A → A.
Infix "⋅" := op (at level 50, left associativity).
Notation "(⋅)" := op (only parsing).

Structure cmraT := CMRAT {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_op : Op cmra_car;
}.
Existing Instances cmra_op cmra_equiv.

Section cmra.
  Context {A : cmraT}.
  Global Instance cmra_equivalence : Equivalence ((≡) : relation A).
Admitted.
End cmra.


Section cmra_mixin.
  Context {A : cmraT}.
  Global Instance cmra_assoc : Assoc (≡) (@op A _).
Admitted.
End cmra_mixin.
Context {A : cmraT}.
Implicit Types x y z : A.

Lemma L x y z : z ⋅ x ⋅ y ≡ y ⋅ x.
Admitted.

Lemma l x y : x ⋅ y ≡ y ⋅ x.
Proof.
rewrite -L.
rewrite -!assoc.

[gares]

You are right, I've a fix, but it may introduce wanted backward incompatibility. So I'm discussing this on the mailing list