Erik Martin-Dorel

@Zimmi48 > @erikmd I should ideally set up the mirror before you open the PR so please let me know when you're close to doing that. Sure! good point, so...

Hi @JasonGross, sorry for the delay :-/ But good news: it happens the coqorg/coq:8.5 image was stalled because of a non-portable Makefile command, and this issue is now solved: *...

Thanks! I don't know the github nickname of Hugo, but it seems the intended question is mentioned here: https://github.com/ocaml-sf/learn-ocaml-corpus/blob/master/exercises/hferee/1.2_declarations/solution.ml So @armandsalek, feel free to open a PR if you can/want...

> Can you elaborate on the situation? Sure! Let me know if you can reproduce the following issue: (I'm using the latest centaur-tabs from MELPA using GNU Emacs 27.1) Actual...

Hi @jcs090218 ! Was my explanation clear enough? or do you need more details Kind regards.

OK thanks @jcs090218 ! Indeed, I now realize that this feature is not "on" by default... so to give full context:

@gares thanks for your comment! > I'm wondering if we could instead hide the evar as in: (...) Yes I was also thinking about this idea, but I didn't try...

> That would also work but needs to be implemented, and can be used outside of the under tactic. Just to correct: a prototype has already been implemented: https://github.com/coq/coq/pull/11200 but...

> (but I'm not sure anything can be done until the serapi release is available) Sure: I can prepare the PR in docker-coq, and the build involving serapi etc. only...

(cross-post of https://coq.discourse.group/t/coq-8-20-rc1/2360/2) FYI: * the [docker-coq](https://hub.docker.com/r/coqorg/coq#supported-tags) image `coqorg/coq:8.20-alpha` has just been replaced with `coqorg/coq:8.20-rc1` (= `coqorg/coq:8.20` as short identifier) * the main change is the addition of the recently-released...