Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7921: Archive the `gallina` tool | 2018-07-07 | |
|\ | |||
* | | doc: Fix markup in Calculus of Inductive Constructions | 2018-07-04 | |
| | | |||
* | | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | 2018-07-03 | |
|\ \ | |||
* \ \ | Merge PR #7703: Add an option to force parameters to be uniform | 2018-07-02 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions | 2018-07-02 | |
|\ \ \ \ | |||
| | | * | | hints: add Hint Variables/Constants Opaque/Transparent commands | 2018-07-02 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables | ||
| | * | | | Document option Uniform Inductive Parameters | 2018-07-01 | |
| | |/ / | |||
| * / / | doc: typesetting and hyperlinks in Syntax Extensions | 2018-06-30 | |
| |/ / | |||
* / / | doc: Fix typesetting in Gallina extensions | 2018-06-29 | |
|/ / | |||
* | | Self-credit for the work done. | 2018-06-28 | |
| | | | | | | | | | | | | I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well. | ||
* | | wrong sphinx syntax | 2018-06-28 | |
| | | |||
* | | Update gallina-extensions.rst | 2018-06-28 | |
| | | | | | | I knew this feature existed but I did not remember the syntax and I could not find it in the manual | ||
* | | Merge PR #7866: Implementation of mutual records in the higher strata | 2018-06-28 | |
|\ \ | |||
* \ \ | Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things. | 2018-06-26 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7851: Modernize the introduction of the reference manual. | 2018-06-26 | |
|\ \ \ \ | |||
| | | | * | Archive the `gallina` tool | 2018-06-25 | |
| |_|_|/ |/| | | | |||
* | | | | Merge PR #7559: Existing Class noop when already a class + warning. | 2018-06-25 | |
|\ \ \ \ | |||
| | | | * | Documenting the syntax of mutual keywords. | 2018-06-24 | |
| |_|_|/ |/| | | | |||
* | | | | Merge PR #7784: Remove Tutorials from a few other places following #7466. | 2018-06-24 | |
|\ \ \ \ | |||
* | | | | | [ssr] document {}/view | 2018-06-22 | |
| | | | | | |||
* | | | | | [ssr] document rewrite {}foo | 2018-06-22 | |
| | | | | | | | | | | | | | | | | | | | | It was used in some examples, but never fully documented | ||
| | | | * | Clarify further doc/README.md following Jim's comments. | 2018-06-22 | |
| | | | | | | | | | | | | | | | | | | | | Relative links. Cf. #7800. | ||
| | | | * | Fix copyright dates in doc/LICENSE. | 2018-06-22 | |
| | | | | | | | | | | | | | | | | | | | | [ci skip] | ||
| | | | * | Improve doc/README.md. | 2018-06-22 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Fix the Markdown. - Add link to latest build of the refman for the master branch. - Clarify what are the dependencies of the HTML doc. [ci skip] | ||
| | | | * | Move INSTALL.doc into doc/README.md. | 2018-06-22 | |
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | This will avoid in particular this ambiguous file extension. [ci skip] | ||
* | | | | Merge PR #7770: Move indices on top on the TOC. Closes #7764. | 2018-06-21 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵ | 2018-06-21 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | understands. | ||
* \ \ \ \ \ | Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter. | 2018-06-21 | |
|\ \ \ \ \ \ | |||
| | | | | | * | Mention Company-Coq as well. | 2018-06-20 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We put it in a footnote otherwise the sentence was starting to be really long. Footnotes need to be in index.rst to really appear at the bottom of the index page. | ||
| | | | | | * | Add a good reference for Proof-General as suggested by Clément. | 2018-06-20 | |
| | | | | | | | |||
| | | | | | * | Modernize the introduction of the reference manual. | 2018-06-20 | |
| |_|_|_|_|/ |/| | | | | | |||
| | * | | | | On cygwin, pass the filename in a format that coqdoc understands. | 2018-06-20 | |
| | | | | | | |||
* | | | | | | Merge PR #7491: Fix #7421: constr_eq ignores universe constraints. | 2018-06-19 | |
|\ \ \ \ \ \ | |||
| | * | | | | | [doc] Rewrite and document the prodn directive | 2018-06-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. | ||
| | * | | | | | [doc] Fix a typo in the ssreflect chapter | 2018-06-19 | |
| | | | | | | | |||
| | * | | | | | [doc] Fix uncaught duplicate-label errors in the SSReflect chapter | 2018-06-19 | |
| | | | | | | | |||
| | * | | | | | [doc] Use productionlist instead of prodn in ring.rst | 2018-06-19 | |
| |/ / / / / |/| | | | | | |||
| * | | | | | Fix #7421: constr_eq ignores universe constraints. | 2018-06-18 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong. | ||
* | | | | | | Fix #7829: Spurious documentation failures. | 2018-06-18 | |
|/ / / / / | | | | | | | | | | | | | | | | We split a Require Import in two to avoid reaching the timeout. | ||
* | | | | | Merge PR #7848: Fix a typo in documentation | 2018-06-17 | |
|\ \ \ \ \ | |||
| | | | * | | Remove Tutorial from Additional documentation in refman intro. | 2018-06-17 | |
| | | | | | | |||
| | | | * | | Remove Tutorials from doc/LICENSE following #7466. | 2018-06-17 | |
| |_|_|/ / |/| | | | | |||
| | | * | | Add introduction and credits to the TOC. | 2018-06-17 | |
| | | | | | | | | | | | | | | | | | | | | Move credits to its own chapter (closes #6573). | ||
| | | * | | Move indexes on top on the TOC. Closes #7764. | 2018-06-17 | |
| |_|/ / |/| | | | |||
* | | | | Merge PR #7749: [doc] Disable smartquotes conversion | 2018-06-17 | |
|\ \ \ \ | |||
* | | | | | [sphinx] Finish clean-up of the Canonical Structure subsection. | 2018-06-16 | |
| | | | | | |||
* | | | | | doc: Add "Print Canonical Projections" command to Command index | 2018-06-16 | |
| |_|/ / |/| | | | |||
| | * | | doc: fix typo. | 2018-06-13 | |
| |/ / |/| | | |||
* | | | Merge PR #7284: [sphinx] Start fixing SSR chapter. | 2018-06-11 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7515: gitlab: build sphinx doc in separate job | 2018-06-09 | |
|\ \ \ \ |