| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-30 | [dune] [docgram] Remove bash hack thanks to new option -no-update. | Théo Zimmermann | |
| 2020-03-28 | New target check-gram to check if fullGrammar and orderedGrammar are up-to-date. | Théo Zimmermann | |
| Use `dune build @check-gram --auto-promote` to automatically update these two files. You will need to run it twice if the two files need to be updated (which is the case most often) as Dune will stop after the first diff failure. The rst files are also updated but left in the `_build/` directory as Dune wouldn't support targets outside the current directory. You can just `mv _build/default/doc/sphinx doc` to update them after running the @check-gram target. | |||
| 2020-03-12 | Dune build rules for doc_grammar and fullGrammar. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |