Jerome Simeon

I've just noticed the following Coq warning: ``` File "./coq/Translation/SQLPPtoNRAEnv.v", line 40, characters 0-6785: Warning: Not a fully mutually defined fixpoint (sqlpp_to_nraenv depends on sqlpp_select_statement_to_nraenv but not conversely). Well-foundedness check...

Question about this: why do we prepend at all? Shouldn't the clean-up logic prevent the need to prepend?

There is a now a small README in `qcert/doc` that documents how to re-generate the documentation and how to re-deploy it consistently to the external Web site. See a6ea8a57a2e915de60ff9b2ea635a770b3183eb4.

The 'main page' for the code documentation produced by coq2html is `doc/doc.html`. It is also available on querycert.github.io (the external Web site).

The main Web site is now produced *from* the `qcert/doc` directory, which is the single source for all the documentation. This ensures for consistency between the documentation and demo produced...

The compilation pipeline figure in Tikz is in `doc/figure` and should be kept up to date there. Previous compilation pipeline figures in keynote have been removed from the source.

The Web demo and documentation are now both contained in the same directory, which facilitates consistent code browsing from the demo and should avoids inconsistent links from the demo to...

Modules in `Basic` have now been split into two directories: - `Utils` containing general purpose libraries, which have been added to the documentation - `Common` containing common components such as...

I've written a sort of "documentation template" for one of our languages (`cNNRC`). This includes a denotational semantics that closely aligns with the published papers, and I believe might be...

Great! Not a big deal, just wondered why we had Python code, and that had to do with the coqoon setup.