Closed ppedrot closed 4 weeks ago
Exposing the proof terms leads to potentially explosive kernel conversions that are avoided as of today by chance (see coq/coq#19038).
The proofs of basic type formers should probably be made Qed-opaque as well, but the current patch already solves the problem in the above Coq PR.
Exposing the proof terms leads to potentially explosive kernel conversions that are avoided as of today by chance (see coq/coq#19038).
The proofs of basic type formers should probably be made Qed-opaque as well, but the current patch already solves the problem in the above Coq PR.