Erik Martin-Dorel

Hi @gares, thanks for your comments. That's good if you think something is feasible (in a more "semantic" way) from the coq/ocaml side for the "expansion". But as I had...

FYI I just posted a related question on [zulip](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Ltac1.2Fssr.3A.20toplevel_selector.20to.20emulate.20the.20.22last.22.20tactical.3F).

Hi @Matafou, thanks for you comment! indeed, ``` { all: rewrite lem1. all: rewrite lem2. all: cycle -1. 1: apply lem3. } ``` is a working workaround (while `-1:` is...

Hi @ifigueroap! thanks for your detailed bugreport. At first sight I'd say that coqdep's output is correct. The colons that are part of Windows' drive letter must indeed be escaped...

Cc @hendriktews FYI Hendrik, we'll be very soon in the process of integrating PG/xml (ideally before end-of-February), which will require at some point to freeze master... so I suggest to...

Now that PG/xml has been integrated, we'll be able to look at this issue. @hendriktews would you have a little time to investigate/fix this? Otherwise I'll give a try next...

Hi, I'm in Toulouse (Paris time = UTC+1); next week I'll only be available on {Wednesday−Thursday−Friday 12 February} (morning or after 18:30)

@cpitclaudel https://terminplaner4.dfn.de/ODlvvqfN5CSxcqxE ← friendly ping :)

Hi @hendriktews, March 10 @ 21:00 is OK for me. Regarding the video system: I don't actually have the Zoom client installed on the workstation I usually develop for PG...

> I though it would be good to share our priorities wrt. to Proof General. Indeed. Also, we could discuss: * some ideas regarding the documentation / discoverability of (new)...