Closed
Description
While working on an experimental change of semantics of Ltac (rocq-prover/rocq#17087), I realized that the current version of rapply in tlc basically reduce to a single call refine on a evar-free term, due to the indirection to old_refine which fails on the presence of unresolved _.
I tried to fix rapply (by inlining old_refine) and only one example seems to need a fix (LibSet.v, lemma set_in_extens_eq, where typeclass becomes useless), so it seems to be worth. Shall I propose a PR?
Metadata
Metadata
Assignees
Labels
No labels