| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-11 | [Sphinx] Move chapter 29 to new infrastructure | Maxime Dénès | |
| 2018-03-09 | Documentation for Cumulativity Weak Constraints. | Gaëtan Gilbert | |
| 2018-02-11 | Documentation for cumulative inductive variance. | Gaëtan Gilbert | |
| 2017-12-01 | [refman] Expand a little on global universes. | Matthieu Sozeau | |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-08-17 | Document anonymous universes (PR #544). | Gaëtan Gilbert | |
| 2017-08-02 | Typo in the documentation of cumulativity | Amin Timany | |
| 2017-07-31 | Update documentation of cumulativity | Amin Timany | |
| 2017-07-31 | Fix typo and Add Jason's example to the doc | Amin Timany | |
| 2017-07-31 | Improve documentation of cumulativity | Amin Timany | |
| 2017-06-16 | Document cumulativity for inductive types | Amin Timany | |
| 2016-06-13 | Univs: more robust Universe/Constraint decls #4816 | Matthieu Sozeau | |
| This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816 | |||
| 2015-12-12 | Indexing and documenting some options. | Pierre-Marie Pédrot | |
| 2015-12-09 | a few edits to the universe polymorphism section of the manual | Gregory Malecha | |
| 2015-11-04 | Univs: update refman, better printers for universe contexts. | Matthieu Sozeau | |
| 2015-10-14 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-07-08 | Fix documentation of universes. | Matthieu Sozeau | |
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès | |
| 2015-01-17 | Univs: Complete documentation in refman. | Matthieu Sozeau | |
| 2015-01-15 | Expand Credits for 8.5 and doc on universes | Matthieu Sozeau | |
| 2015-01-08 | Fix some documentation typos. | Guillaume Melquiond | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar). | |||
| 2014-07-25 | More documentation of universes. | Matthieu Sozeau | |
| 2014-07-24 | Start documenting universe polymorphism. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |