| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-06 | Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann. | Hugo Herbelin | |
| 2020-05-06 | Documenting plugin/tactic/stdlib keywords in corresponding chapters. | Hugo Herbelin | |
| Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch || | |||
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann | |
| 2020-05-01 | Create basics out of sections from Gallina and Vernac chapters. | Théo Zimmermann | |
| 2020-05-01 | Create section on basics with just flags, options and tables. | Théo Zimmermann | |
| 2020-05-01 | Create section on basics with just lexical conventions and attributes. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |