Stream: Dune devs & users

Topic: arbitrary terms as hints


view this post on Zulip Notification Bot (Jun 10 2020 at 10:34):

This topic was moved by Cyril Cohen to #Coq devs & plugin devs > declaring arbitrary terms as hints is deprecated


Last updated: Oct 16 2021 at 07:02 UTC