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: Oct 21 2021 at 21:03 UTC