Stream: Coq devs & plugin devs

Topic: set_term_pr

view this post on Zulip Gaëtan Gilbert (Jul 22 2020 at 11:36):

Does anyone use the Ppconstr.set_term_pr functionality? Otherwise we should remove it.

view this post on Zulip Gaëtan Gilbert (Jul 22 2020 at 11:37):

same for the Prettyp.set_object_pr

Last updated: Sep 09 2024 at 05:02 UTC