Anomaly "Uncaught exception Not_found." when destructing an inductive type as a resolvable opaque reference #19994
Labels
kind: anomaly
An uncaught exception has been raised.
kind: bug
An error, flaw, fault or unintended behaviour.
Description of the problem
<+
) by an empty module or module typeKaboom.
Even though the wrapped type is the same as the inductive type (one
eq
anotherby exact eq_refl
), it cannot be destructured (or even pattern matched by hand) this way. A workaround is to make an explicit type cast.Small Rocq / Coq file to reproduce the bug
Version of Rocq / Coq where this bug occurs
8.20
Last version of Rocq / Coq where the bug did not occur
No response
The text was updated successfully, but these errors were encountered: