Stream: Coq devs & plugin devs

Topic: ✔ Logic.refiner


view this post on Zulip Guillaume Melquiond (Dec 05 2022 at 11:30):

What is the proper replacement for Logic.refiner ~check:false t in Coq 8.17?

view this post on Zulip Pierre-Marie Pédrot (Dec 05 2022 at 12:30):

if t doesn't contain metas, then you can write exact_no_check I think

view this post on Zulip Pierre-Marie Pédrot (Dec 05 2022 at 12:31):

otherwise you have to track the type of metas, replace them with evars and use refine

view this post on Zulip Pierre-Marie Pédrot (Dec 05 2022 at 12:33):

(if you have trouble porting your code I can have a look)

view this post on Zulip Guillaume Melquiond (Dec 05 2022 at 13:10):

Thanks. That works fine. The solution was so simple that I somehow missed it.

view this post on Zulip Notification Bot (Dec 05 2022 at 13:10):

Guillaume Melquiond has marked this topic as resolved.


Last updated: May 28 2023 at 16:30 UTC