Enrico Tassi
Enrico Tassi
I switched to 1.4 and I get errors suggesting to do `alectryon/pygments/tacn:` -> `alectryon/pygments/coq/tacn:`. I followed the advice, but now my html starts with a bold `alectryon/pygments/tacn: elpi` (as if...
As per https://github.com/ocsigen/lwt/commit/fc633f8f02bf0f1a7b9e20607db0d44589142d9e `fork` is supposed to "cancel" the pending jobs. Unfortunately the doc does not say it does so in a delayed fashion. A comment hints that it is...
*do not merge* this is a POC to be discussed at a seminar on the 18th TODO (hopefully for the 18th): - [x] support `Terms.Meta` in the HOAS encoding using...
The bug was filed on the Debian package, https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=789534 The Debian package is still the old version 31, but looking at the changelog I could not see this particular issue...
This PR clean up some code path in the kernel, ensuring side effects are either there or not there (which was previously checked dynamically). Fix #13324 - https://github.com/maximedenes/vscoq/pull/10
The proof mode for the current proof was handled by the STM. We move this piece of state in Pvernac and include it into Vernacstate.Parser.t so that "the parsing state"...
- https://github.com/math-comp/math-comp/pull/911 Embeds #16366 #16367
apparently the rules for the prelude are not generated: ``` File "dev/shim/dune", line 14, characters 0-384: 14 | (rule 15 | (targets coqc-prelude) 16 | (deps 17 | %{bin:coqc} 18...
The changelog constains "DOC TODO" a few times. Check if it is really the case that the documentation is missing.
The idea is to warn when KEYWORD and IDENT are parsed and there is no space between them and KEYWORD ends with an ident-character. Eg `*m` infix KEYWORD and input...