Error: Anomaly "File "pretyping/evarsolve.ml", line 944, characters 61-67: Assertion failed." (with Definitional UIP)

[JasonGross]

Description of the problem

No response

Small Rocq / Coq file to reproduce the bug

Set Definitional UIP.
Module Export IsomorphismDefinitions.
#[export]
Set Universe Polymorphism.
Inductive eq@{s|u|} {α:Type@{s|u}} (a:α) : α -> SProp
:= eq_refl : eq a a.
Arguments eq_rect [α] a P _ y _ : rename.
Section Bug.
Variable (A : Type) (f : A -> A).
Variable (hf : forall x, IsomorphismDefinitions.eq (f x) x).
Variable (P : A -> Type).
Variable (a : A) (H : P (f a)).
Definition bug : P a :=
IsomorphismDefinitions.eq_rect _ _ (fun x _ => P x) H _ (hf a).
End Bug.
End IsomorphismDefinitions.

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

[yannl35133]

May be a duplicate of #21141