Open
Description
Description of the problem
Anomaly Not found (lookup env in irr_flex)
Small Rocq / Coq file to reproduce the bug
Inductive STrue : SProp := SI.
Inductive Box (A : SProp) : A -> Set := box a : Box A a.
Symbol S: bool -> Type -> Set.
Rewrite Rule S_rew :=
S _ (forall (a : ?A), Box STrue ?b) => Box _ (fun a => ?b).
Check fun (x : STrue) =>
(eq_refl : S true (unit -> Box STrue x) = S false (unit -> Box STrue x)).
Definition error (x : STrue) :=
(eq_refl : S true (unit -> Box STrue x) = S false (unit -> Box STrue x)).Version of Rocq / Coq where this bug occurs
8.20, 9.0, master
Interface of Rocq / Coq where this bug occurs
No response
Last version of Rocq / Coq where the bug did not occur
No response