Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | * | 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 | ||
|\ \ \ \ | ||||
| * | | | | gitlab: build sphinx doc in separate job | 2018-06-08 | ||
| | | | | | ||||
| | | | * | Existing Class noop when already a class + warning. | 2018-06-08 | ||
| |_|_|/ |/| | | | | | | | | | | | Fix #5012. | |||
| | | * | [doc] Disable smartquotes conversion | 2018-06-08 | ||
| |_|/ |/| | | | | | | | | Closes GH-7742. | |||
| | * | Improve links to SSR tactics, and some other improvements. | 2018-06-05 | ||
| | | | ||||
| | * | Workaround a weird error of .. coqtop:: | 2018-06-05 | ||
| | | | ||||
| | * | Remove many abusive .. coqtop in SSR chapter. | 2018-06-05 | ||
| | | | | | | | | | | | | Many still remain. | |||
| | * | A few additional small fixes. | 2018-06-05 | ||
| | | | ||||
| | * | [sphinx] Fix missing indices warnings. | 2018-06-05 | ||
| | | | ||||
| | * | [ssr] index entry for "without loss", "suffices" and "generally have" | 2018-06-05 | ||
| | | | ||||
| | * | [ssr] some fixes to the documentation markup | 2018-06-05 | ||
| | | | ||||
| | * | [sphinx] Start fixing SSR chapter. | 2018-06-05 | ||
| |/ |/| | ||||
* | | Merge PR #7229: Deprecate implicit tactic solving. | 2018-06-04 | ||
|\ \ | ||||
* \ \ | Merge PR #7481: document 7025 (coq_makefile flag variables) | 2018-06-04 | ||
|\ \ \ | ||||
* \ \ \ | Merge PR #7601: Fix notation for code snippet in documentation | 2018-06-04 | ||
|\ \ \ \ | |_|_|/ |/| | | | ||||
| | | * | Documenting the deprecation. | 2018-06-04 | ||
| |_|/ |/| | | ||||
* | | | Merge PR #7648: Indicate in the doc that clearbody can take several idents | 2018-06-04 | ||
|\ \ \ | ||||
* \ \ \ | Merge PR #7537: Improve the Gallina chapter of the reference manual. | 2018-06-01 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR #7606: Allow more than one signature and name per Sphinx object | 2018-06-01 | ||
|\ \ \ \ \ | ||||
| | | * | | | Merge two clearbody docs | 2018-06-01 | ||
| | | | | | | ||||
| | | * | | | Indicate in the doc that clearbody can take several idents | 2018-05-31 | ||
| |_|/ / / |/| | | | | ||||
* | | | | | Merge PR #7566: Remove a dead old-refman file. | 2018-05-29 | ||
|\ \ \ \ \ | ||||
| | | * | | | Improve the last section of the Gallina chapter. | 2018-05-28 | ||
| | | | | | | ||||
| | | * | | | Chapter 1 of the refman compiles without reporting any undocumented object. | 2018-05-28 | ||
| | | | | | | ||||
| | | * | | | Improve sections on (Co)Fixpoint of the Gallina chapter. | 2018-05-28 | ||
| | | | | | | ||||
| | | * | | | Improve subsection on co-inductive types of the Gallina chapter. | 2018-05-27 | ||
| | | | | | | ||||
| | | * | | | Improve subsection on mutual inductive types of the Gallina chapter. | 2018-05-27 | ||
| | | | | | | ||||
| | | * | | | Move 'new in Coq 8.1' subsection to an appropriate place. | 2018-05-27 | ||
| | | | | | | ||||
| | | * | | | Document Variant properly. | 2018-05-27 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Cf. Enrico's remark at https://github.com/coq/coq/pull/7536#issuecomment-389826121 This commit also marginally improves the Record doc (a lot more remains to do). |