Pierre Courtieu

I decided to add the fix of hardwired command strings (removing trailing spaces) in a separate commit of this same PR.

The failed CI is not related (reached VM limit). I merge now.

Thanks for the report! If the bug remains after coqtop is restarted then it can come only from the coqtop invokation itself. Can you give the containt of `awesome1.v` please?...

The option `-noinit` in `coq-prog-args` is passed to `coqtop`. It causes coqtop to be launched without the standard prelude. Since the notation for `+` is defined in Coq's standard prelude...

The most probable explanation is that the first file needs `-noinit` and you set it via a `_CoqProject`, and the second file has no project file so options are left...

I am not sure what is happening exactly, because `-noinit` should make the first file fail at first. @walck we need a bit more investigation :-).

But we should definitely restart coqtop: this is more robust than retracting as pointed out by Gaetan [here](https://coq.zulipchat.com/#narrow/stream/304019-Proof-General-users/topic/Restarting.20ProofGeneral/near/442904710). At least to be correct we need to check if the options...

I don't think so. The variable safe-local-variable-values only says that it safe to execute this piece of code. This piece of code is probably in a file .dir-locals.el or in...

I mean: this customization alone does not say that the option is set. It only says that it is allowed to do be set automatically by a file variable. It...

Hi. thanks for the PR. Sorry for the delay... Do we really want this? If one uses `unicode-tokens.el` then isn't it mandatory to have `token-symbol-map` defined? If yes then failing...