Stream: Coq devs & plugin devs

Topic: if: "Needed cmt file of module 'Hints'

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 15:24):

on Hints.add_hints in classes.ml I try merlin-locate and it says "Needed cmt file of module 'Hints' to locate 'Hints.add_hints' but it is not present"
what is going on?

Last updated: Dec 06 2023 at 13:01 UTC