Stream: Dune devs & users

Topic: arbitrary terms as hints

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: Jun 04 2023 at 23:30 UTC