index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
refman
/
Universes.tex
Age
Commit message (
Expand
)
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
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
2014-07-25
More documentation of universes.
Matthieu Sozeau
2014-07-24
Start documenting universe polymorphism.
Matthieu Sozeau
