simplify_map_eq regression ?
Consider the following code:
Section simplify_map_eq.
Context `{FinMap K M}.
Definition M' := M nat.
Lemma simplify_map_eq_1 (m : M') i x y :
<[i:=x]> m !! i = Some y ->
x = y.
Proof.
intros. simplify_map_eq. (* nothing is simplified *)
unfold M' in *. by simplify_map_eq.
Qed.
End simplify_map_eq.
I think with stdpp 1.3, it wasn't necessary to do the unfold
for simplify_map_eq
to work, but not 100% sure.
In any case, I would still expect the tactic to simplify.