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: Oct 21 2021 at 21:03 UTC