Scheme Rewriting does not fuly support polymorphic equality

[tabareau]

Description of the problem

When used on a polymorphic equality, Scheme Rewriting does not generate rew_r_dep and sym_involutive.

Small Rocq / Coq file to reproduce the bug

#[universes(polymorphic)]
Inductive peq@{i} (A:Type@{i}) (x:A) : A -> Prop :=
    peq_refl : peq A x x.

Scheme Rewriting for peq.

Check peq_rew_dep.
Check peq_rew_dep.
Fail Check peq_rew_r_dep.
Fail Check peq_sym_involutive.

Version of Rocq / Coq where this bug occurs

9.2

Interface of Rocq / Coq where this bug occurs

No response

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

No response

[tabareau]

Note that peq_rew_r_dep depends on peq_sym_involutive so probable it is only a problem in the generation of peq_sym_involutive.