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: Dec 07 2023 at 09:01 UTC