Michael Soegtrop (Mar 21 2021 at 17:43): Michael Soegtrop (Mar 21 2021 at 17:43):@Pierre-Marie Pédrot : from a certain depth on, I get ellipses in the output of "Message.of_constr". I tried to change "Set Printing Depth", but this doesn't seem to have an effect. Is there a way to get a complete constr output from "Message.of_constr"?
Michael Soegtrop (Mar 21 2021 at 18:26):It might be a CoqIDE issue - checking ...
Pierre-Marie Pédrot (Mar 21 2021 at 19:46):No, AFAIK it's a limitation of the printing engine. You'd have the same issue with the vanilla Print command.
Pierre-Marie Pédrot (Mar 21 2021 at 19:47):I think I remember there was an open issue about this.
Michael Soegtrop (Mar 21 2021 at 19:59):With coqc (instead of CoqIDE) I can control the output with "Set Printing Depth". See also (https://github.com/coq/coq/pull/13972). But of cause it could be that with Ltac2 there are additional issues. It is hard to imagine that the output of Message.of_constr can somehow be manipulated by the IDE as Emilio described in the PR. But then I learned not to underestimate what is possible since I work with Coq ;-)
Last updated: Apr 19 2024 at 10:02 UTC