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: Oct 13 2024 at 01:02 UTC