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: Oct 13 2024 at 01:02 UTC