Romain Tetley comments

Results 175 comments of


                                            Romain Tetley

Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

@gares what is the status on this ?

[notation-overridden,parsing,default] on `all_ssreflect` import

Pinging @gares

Ltac printing - where is it displayed?

Hi, Thanks for reporting ! There seems to be a regression... I'll investigate !

Output of "Search" inconvenient.

I believe the messages section in the goal panel of VsCoq 2 somewhat solves this issue. I'll close it here and if something else comes up we can continue the...

Shortcut for CoqIde `Compile` => `Compile Buffer`

I am closing this for now as it feels like the proposed solution works well enough.

Missing the "Fully check the document" command of CoqIDE

@MSoegtropIMC That's fair, I'll reopen it so long. Can we maybe make a separate issue for the colouring ? Also I'm not certain the violet colouring still happens with VsCoq...

The messages bar is missing?

This does not seem to be working in VsCoq 2, I will keep it open to investigate. I would expect the message to appear in the messages section of the...

Issues with Ltac2 (seen the same before in CoqIDE and PG).

Closing this issue as it seems fixed in VsCoq 2

Coq Platform packaging

Is this a duplicate of #472 ?

Print Notices/Error messages etc. in same buffer

Adding this to the VsCoq 2 road map as it doesn't seem to work.