metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard
verified publisher icon MetaCoq

Remove eta-expansion in lift_wf_term_it_impl

Open Tragicus opened this issue 6 months ago • 0 comments

https://github.com/rocq-prover/rocq/pull/20730 finds more general solutions to a certain class of unification problems, so with the eta-expansion in lift_wf_term_it_impl, some evars never get instantiated when applying the lemma.

Tragicus avatar Jun 19 '25 13:06 Tragicus