What is the proper replacement for
Logic.refiner ~check:false t in Coq 8.17?
if t doesn't contain metas, then you can write exact_no_check I think
otherwise you have to track the type of metas, replace them with evars and use refine
(if you have trouble porting your code I can have a look)
Thanks. That works fine. The solution was so simple that I somehow missed it.
Guillaume Melquiond has marked this topic as resolved.
Last updated: Nov 29 2023 at 05:01 UTC