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: Jun 10 2023 at 06:31 UTC