Stream: Coq devs & plugin devs

Topic: flags to control TC search

view this post on Zulip Enrico Tassi (Nov 15 2021 at 12:38):

Some code takes both ~with_classes ~flagslike Hints.hint_res_pf or Clenv.res_pf. My problem is that flags.resolve_evars seem to already control TC resolution. I think we should only keep one.

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 12:43):

flags.resolve_evars raises an exn if it can't resolve everything (calls resolve_typeclasses ~fail:true), but res_pf ~with_evars:true ~with_classes:true doesn't

Last updated: Jul 24 2024 at 11:01 UTC