@ejgallego Ah, I didn't think to click on filenames. I hadn't heard anyone mention code coverage, so I thought was new. Is it getting much use? No coverage of printing? The number of untested paths per file would be an interesting statistic, though.
Emilio Jesús Gallego Arias
@jfehrle oh, I'll add printing indeed. It is fairly easy to get and process the coverage data by yourself, there are still some issues with the build system but I hope to push a full CI coverage job this summer. The tool that generates the reports has many options and I'm sure they would warmly welcome contributions, there are easier on PRs than us :) see the coverage issue in the coq repos for more details
I don't quite get this. The highlighting seems to indicate 2 paths on each line where I don't see any conditionality.
@mattam82 What does "TCB" mean? Abbreviation for ??
From /dev/doc/change.md "The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are deprecated. Use TYPED AS instead." According to the coqpp parser they are more than deprecated, can't find an entry for them.
one question that came up over lunch: best documentation resources for doing real analysis using Coq?
Yves pointed out that Boldo & Melquiond's book covers this to some extent, but are there others?