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 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: May 18 2024 at 08:40 UTC