Pierre Courtieu
Pierre Courtieu
Opening a discusison: I am not sure this is in the scope of stdlib2 or if this is already thought of, but it would be nice to move all default...
The idea is that this splash screen annoys everyone, even in its new manga-style form. I would even consider removing it completely but at least let us not have it...
### Description of the problem It seems that `%` is not considered when computing the width of an output. In the script below the output has width 78 characters instead...
Following a [remark](https://coq.zulipchat.com/#narrow/stream/304019-Proof-General-users/topic/Restarting.20ProofGeneral/near/442904710) by @SkySkimmer. Currently when the user asks for scripting a different file than the current one PG does the following things: 1. ask for retracting the current...
This bug appeared because of PR #774. Backtracking it is not satisfying because #773 shows a good reason for it. Example: ```coq Require Import Utf8. Definition trois := 3. (*test-definition*)...
We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymore (#774). Solution: use the character position information with the...
The lexer now glues a "\" to an immediately following word if it is itself preceded by a space. Note that for really good indentation you should try to add...
Coq stopped printing around debug infos some versions ago. This has been preventing response and goals buffers to dispatch debug info. This patch seems to fix this.
#### Description of the problem Don't know if this is a real bug or a feature. In the latter case I would like to ask for a workaround. `specialize` does...