Pierre Courtieu

Results 266 comments of Pierre Courtieu

Syntax of `-arg` in `_CoqProject`

@herbelin @cpitclaudel is there some news about this? I don't have strong opinion either. But it is very important that coqide, pg and coq_makefile behave all the same (and any...

*response* window is too small when proof-shrink-windows-tofit is t

I also happens to me sometimes but I could not yet understand in which conditions this happens. It may be due to the use of symbols, which may make lines...

PG highlights beginning of conclusion like a hypothesis name

Indeed the regexp is a simplistic for efficiency reasons. I will make some experiments.

PG highlights beginning of conclusion like a hypothesis name

Interesting. How big are your goals please? I think you can turn off syntax highlighting in goals if it is to annoying.

`.}` not detected by PG as syntax error

Indeed pg is far from perfect at splitting a file into commands. This case is known #357. Along with at least those: #612, #592, #58. We definitely need to make...

Every command to Coq also sends "Show." and gets error "This command requires an open proof."

I can't reproduce this behaviour. Can you give a coq file that make you have it please?

Every command to Coq also sends "Show." and gets error "This command requires an open proof."

Can you also give the version of PG you have?

Every command to Coq also sends "Show." and gets error "This command requires an open proof."

@jeapostrophe do you still have this issue? I can't reproduce it.

Every command to Coq also sends "Show." and gets error "This command requires an open proof."

Homebrew stable package? It dates back to 2016. If this is the case you should hopfor the HEAD homebrew package or the MELPA package.

Indentation issue: "forall"

> But maybe the second case isn't relevant anymore? (Is `;` associative now?) They always can, parenthesis are just prenthesis. Like in `repeat (intro)`. But a term inside a tactic...