diff options
| author | Pierre-Marie Pédrot | 2020-08-11 20:38:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-11 20:38:37 +0200 |
| commit | e0e07f58da0d45ab54558c61a4a1c3074dfb6380 (patch) | |
| tree | 730de876e52f8ab346369d3537b086f5702a0e08 /dev/README.md | |
| parent | 1d6c794956b962294db765e624b58e531e2f970a (diff) | |
| parent | 1121a2da999db0a810cfb401e3c3db620fb6481d (diff) | |
Merge PR #12717: More documentation on grammars and parsing
Reviewed-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
Diffstat (limited to 'dev/README.md')
| -rw-r--r-- | dev/README.md | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/dev/README.md b/dev/README.md index 0c6b8020f1..0a6b196ec0 100644 --- a/dev/README.md +++ b/dev/README.md @@ -22,14 +22,12 @@ | [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source | | [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files | | [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling | -| [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | -| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | -| [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | +| [`dev/doc/universes.md`](doc/universes.md) | Help for debugging universes | | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | +| [`dev/doc/parsing.md`](doc/parsing.md) | Grammar and parsing overview | | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | | [`dev/doc/xml-protocol.md`](doc/xml-protocol.md) | XML protocol that coqtop and IDEs use to communicate | -| [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | |