| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle | |
| 2021-01-18 | Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermost | coqbot-app[bot] | |
| Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: gares | |||
| 2021-01-06 | Improve description of rewrite_strat/innermost and outermost | Jim Fehrle | |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-11-24 | Convert auto chapter to prodn | Jim Fehrle | |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann | |
| The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version. | |||
| 2020-10-24 | Convert misc chapters to prodn | Jim Fehrle | |
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann | |
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann | |
| 2020-03-09 | Remove some productionlists | Jim Fehrle | |
| 2020-02-28 | Convert Gallina Vernac to use prodn | Jim Fehrle | |
| 2019-11-27 | weaker then -> weaker than | larsr | |
| 2019-11-20 | Update grammar in the Terms section of Gallina chapter | Jim Fehrle | |
| Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed. | |||
| 2019-11-14 | Merge PR #11100: small documentation fixes | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Ack-by: cpitclaudel | |||
| 2019-11-14 | doc fixes | Antonio Nikishaev | |
| 2019-11-03 | Elan → Stratego in documentation of `rewrite_strat`. | Robbert Krebbers | |
| @eelcovisser told me that the strategies in Luttik and Visser 97 were inspired by Elan, but they are not part of Elan. They are part of the Stratego language. | |||
| 2019-06-04 | [rewrite] Add Morphism syntax made different for module type parameters | Enrico Tassi | |
| 2019-05-23 | Define many undefined tokens, and other misc fixes. | Théo Zimmermann | |
| Progress towards #9411, extracted from #10118, rebased ontop of #10192. | |||
| 2019-05-21 | Fixing typos - Part 1 | JPR | |
| 2019-05-19 | [refman] Misc fixes (indentation, whitespace, notation syntax) | Clément Pit-Claudel | |
| 2019-05-16 | [refman] Introduce syntax for alternatives in notations | Clément Pit-Claudel | |
| Closes GH-8482. | |||
| 2019-02-18 | Using options abort and restart of coqtop directive in the manual. | Théo Zimmermann | |
| 2019-02-12 | Fix failing coqtops in generalized-rewriting.rst | Gaëtan Gilbert | |
| 2019-01-22 | Remove unneeded | in productionlists | Jim Fehrle | |
| 2018-11-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 2018-09-20 | [doc] Fix a few syntax highlighting issues | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-08-31 | Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵ | Zeimer | |
| directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues. | |||
| 2018-08-03 | Fix docs on arguments to setoid_replace. Fixes #8213 | Langston Barrett | |
| 2018-08-01 | Added a tactic index entry for nsatz, reformatted commands in chapter ↵ | Zeimer | |
| 'Generalized Rewriting' and renamed the chapter Nsatz from _nsatz to _nsatz_chapter. | |||
| 2018-08-01 | Improved grammar and spelling in the remaining chapters of the Reference Manual. | Zeimer | |
| 2018-06-13 | doc: fix typo. | whitequark | |
| 2018-05-09 | [sphinx] Fix new warnings related to tacn, cmd, opt... | Théo Zimmermann | |
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | More fixes in the Generalized Rewriting chapter. | Théo Zimmermann | |
| 2018-04-16 | [Sphinx] Clean-up indices | Maxime Dénès | |
| 2018-04-14 | [Sphinx] Fix all remaining warnings. | Maxime Dénès | |
| 2018-04-14 | [sphinx] Fix many warnings. | Théo Zimmermann | |
| Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | |||
| 2018-03-30 | [Sphinx] Add chapter 27 | Maxime Dénès | |
| Thanks to Calvin Beck for porting this chapter. | |||
| 2018-03-30 | [Sphinx] Move chapter 27 to new infrastructure | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |