Importing all_ssreflect prevents `rewrite ... in` from compiling

[mcoulont]

Description of the problem

The present issue is opened following a question in Stack Exchange where Tragicus kind of advised me to report here.

The following lemma compiles in Rocq v9.0.0 with rocq-mathcomp-ssreflect v2.4.0:

Lemma xpredT_not_equal_xpred0 {A : Type} (a : A)
(H : @eq (forall _ : A, bool) (fun _ : A => true) (fun _ : A => false))
(H1 : not ( @eq bool ((fun _ : A => true) a) ((fun _ : A => false) a))) :
  False.
Proof.
  rewrite H in H1. apply H1. reflexivity.
Qed.

unless it's preceded with

From mathcomp Require Import all_ssreflect.

Error:

The LHS of H
 xpredT
does not match any subterm of the goal

Why does rewrite -> H in H1 compile and not rewrite H in H1 in the proof?

Small Rocq / Coq file to reproduce the bug

From mathcomp Require Import all_ssreflect.

Lemma xpredT_not_equal_xpred0 {A : Type} (a : A)
(H : @eq (forall _ : A, bool) (fun _ : A => true) (fun _ : A => false))
(H1 : not ( @eq bool ((fun _ : A => true) a) ((fun _ : A => false) a))) :
  False.
Proof.
  rewrite H in H1. apply H1. reflexivity.
Qed.

Version of Rocq / Coq where this bug occurs

9.0.0

Interface of Rocq / Coq where this bug occurs

compilation

Last version of Rocq / Coq where the bug did not occur

No response

[TheoWinterhalter]

Once you import SSReflect, you actually use its rewrite tactic, and no longer the vanilla Rocq one. I think you can recover it by using an arrow explicitly, like rewrite -> h.

[mcoulont]

So what I've reported is the expected behavior?

[CohenCyril]

It is expected, but I do think we should modify this behavior. This has been discussed in mathcomp meetings: using a different name for ssreflect rewrite to avoid this clash. @gares @affeldt-aist @proux01 @Tragicus @pi8027 ...

[proux01]

Well, we'll probably still keep rewrite some time for backward compatibility reasons.
But I'm not sure if the issue here is actually this rewrite overloading or the fact that the pattern matching of the ssreflect rewrite is not able to match the product (adding a pattern selector works fine).