Stream: Coq devs & plugin devs

Topic: Logic.refiner

Guillaume Melquiond (Dec 05 2022 at 11:30):

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

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

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

Pierre-Marie Pédrot (Dec 05 2022 at 12:33):

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

Last updated: Feb 06 2023 at 19:03 UTC