Proof of False

[yannl35133]

Description of the problem

PR coming soon.

Small Rocq / Coq file to reproduce the bug

Definition oops : False :=
  (fix rec (x : unit) : False :=
  let f (b : False) := match b with end in
  let g x := x in
  f (rec ((ltac:(fix rec' 1; exact g) :> unit -> unit) x))) tt.

Version of Rocq / Coq where this bug occurs

9.1

Interface of Rocq / Coq where this bug occurs

No response

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

No response

[ppedrot]

This was introduced in 8.16 probably by e02b384.