Jason Gross

Is LaTeX installed on the CI that runs Coq's test-suite?

Perhaps the configure script should be updated

However, I have installed tipa, and that is not enough, the test still fails with ``` 2] kpathsea: Running mktextfm ecti1200 /usr/share/texlive/texmf-dist/web2c/mktexnam: Could not map source abbreviation for ecti1200. /usr/share/texlive/texmf-dist/web2c/mktexnam:...

I will note that I'm using texlive-latex-extra rather than texlive-science; is this an important difference? Also, my dependency list is: ``` Build-Depends: rsync, tipa, python, python3, debhelper (>= 9), dh-ocaml...

https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=759928 suggests that maybe I also need texlive-fonts-recommended

As I understand it, the issue here is that Coq checks the typing of each branch before checking that the patterns of subsequent branches are valid. I believe @cpitclaudel is...

> Why does not Coq use the annotation that's on the definition? It seems to do that when the annotation is simpler (just nat instead of a match, like in...

> I would say that `Transparent` and `Opaque` refers to the current status of a `Defined` constant for the non-kernel parts The kernel's heuristics care about `Transparent` and `Opaque` though....

> The current idea with `is:` is really that it refers to the word used in the source code. But, indeed, that may be more intuitive to decide that `is:Definition`...

Also, "Error: Syntax error: operator expected." is a horrible error message for "`type` is a reserved keyword" (or something like that) (and it shows up on characters 75-79 of the...