| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-15 | [Sphinx] Add chapter 14 | Maxime Dénès | |
| Thanks to Paul Steckler for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 14 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6993: Sphinx doc chapter 13 | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 13 | Maxime Dénès | |
| Thanks to Paul Steckler for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 13 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6991: Sphinx doc chapter 12 | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 12 | Maxime Dénès | |
| Thanks to Clément Pit-Claudel for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 12 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6990: Sphinx doc chapter 10 | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 10 | Maxime Dénès | |
| Thanks to Calvin Beck for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 10 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6987: Sphinx doc chapter 8 | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 8 | Maxime Dénès | |
| Thanks to Heiko Becker and Nikita Zyuzin for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 8 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6985: Sphinx doc chapter 5 | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 5 | Maxime Dénès | |
| Thanks to Richard Ford for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 5 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6983: Sphinx doc chapter 4 | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 4 | Maxime Dénès | |
| Thanks to Richard Ford for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 4 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6982: Sphinx doc chapter 2 | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 2 | Maxime Dénès | |
| Thanks to Paul Steckler for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 2 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | Merge PR #6979: Sphinx doc credits | Maxime Dénès | |
| 2018-03-15 | Merge PR #6912: [doc] Document removal of deprecated options. | Maxime Dénès | |
| 2018-03-15 | Merge PR #6967: [META] Update Coq version number. | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add credits | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move credits to new infrastructure | Maxime Dénès | |
| 2018-03-14 | Merge PR #6975: Fix whitespace issue in TacticNotationsVisitor.py | Maxime Dénès | |
| 2018-03-14 | Merge PR #6973: [Sphinx] migrate introduction | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Add introduction | Maxime Dénès | |
| I backported changes done to the LaTeX manual. | |||
| 2018-03-13 | [Sphinx] Move introduction to new infrastructure | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Add "edit on github" | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Mention license | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Remove ad-hoc color for links interfering with TOC | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Update some metadata | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Read version number from configure | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Comment out metadata for unused backends | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Remove information for .chm backend | Maxime Dénès | |
| 2018-03-13 | [Sphinx] add bibliography | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Add indexes | Maxime Dénès | |
| 2018-03-12 | [Sphinx] Add table of contents | Maxime Dénès | |
| 2018-03-12 | Fix whitespace issue in TacticNotationsVisitor.py | Maxime Dénès | |
| 2018-03-12 | [Sphinx] Add doc preamble | Maxime Dénès | |
| 2018-03-12 | [Sphinx] Add a few grammar constructions | Maxime Dénès | |
| Code from Paul Steckler (MIT). | |||
| 2018-03-11 | [META] Update Coq version number. | Emilio Jesus Gallego Arias | |
| 2018-03-10 | Merge PR #6869: [ssreflect] Fix module scoping problems due to packing and ↵ | Maxime Dénès | |
| mli files. | |||
| 2018-03-10 | [ssreflect] Fix module scoping problems due to packing and mli files. | Emilio Jesus Gallego Arias | |
| Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512. | |||
| 2018-03-10 | Merge PR #6837: [located] Push inner locations in reference to a CAst.t node. | Maxime Dénès | |
| 2018-03-10 | Merge PR #6831: [located] More work towards using CAst.t | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |