search

uds-psl / coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.
Mozilla Public License 2.0
111 stars 30 forks source link

Adapt w.r.t. coq/coq#17564. #199

Closed ppedrot closed 1 year ago

ppedrot commented 1 year ago

Should be backwards compatible.

DmxLarchey commented 1 year ago

If I may, why do the e variants need to be introduced here (for the record) ?

yforster commented 1 year ago

I think non-e tactics are not allowed to introduce evars by design. But there was a bug which allowed us to use intros in way that it was generating evars via % - now such uses have to be explicit via e. Did I get this right @ppedrot?

ppedrot commented 1 year ago

Indeed, in Coq master intropatterns can silently introduce evars even though the surrounding tactic should prevent them. This happens when destructing higher-order terms.

ppedrot commented 1 year ago

(You can merge this already since the CI is green.)