Erik Martin-Dorel

@ejgallego IIUC you suggest that the main place from PG codebase where `coqtop` is called to run the REPL, we should replace for example (if I open a file from...

BTW I have the same question as @Matafou > Isn't it the `dune` file that we want to detect here? `dune-project` is not necessary is it? also we may want...

@HuStmpHrrr good catch! Rather than just removing this part, I guess it'd be nicer to somewhat "translate" it to, say, Coq (?)

Hi @hendriktews, what the status of this PR? * In particular, I've just seen https://github.com/coq/coq/pull/10489 had been merged. * But that PR 10489 is only integrated in Coq 8.11+, so...

* On the other hand, coq/coq#10489 mentions it addressed issue coq/coq#10399, which did not seem to impact Coq

Thanks a lot @hendriktews for your detailed reply. > I suggest to only support proof tree display for Coq >= 8.11 in the future. OK for me! > If there...

Hi @chdoc, thanks for suggesting this! sounds like a neat feature to have for ssreflect proofs indeed. would you already have further suggestions to refine that part of the feature...

Hi @chdoc > idea: add a macro for "new line beginning with all:rewrite" − I'm neutral about the locking for rewriting indeed, the "lock" seems unneeded, provided it is easy...

Hi @chdoc > > And we should also decide which keybinding would be OK for the three steps involved > > In my setup (PG + company-coq) `C-c r` is...

> > I think this feature goes beyong ssreflect. I have been thinking about something like this for the `;` tactical. Debuging `foo;bar;rab;oof` boils down to the same mechanics really....