@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"?
It might be a CoqIDE issue - checking ...
No, AFAIK it's a limitation of the printing engine. You'd have the same issue with the vanilla
I think I remember there was an open issue about this.
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: Dec 06 2023 at 15:01 UTC