coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	Indexing and documenting some options.	Pierre-Marie Pédrot	2015-12-12
\|
*	a few edits to the universe polymorphism section of the manual	Gregory Malecha	2015-12-09
\|
*	Univs: update refman, better printers for universe contexts.	Matthieu Sozeau	2015-11-04
\|
*	Fix some typos.	Guillaume Melquiond	2015-10-14
\|
*	Fix some typos.	Guillaume Melquiond	2015-10-13
\|
*	Fix documentation of universes.	Matthieu Sozeau	2015-07-08
\|
*	Separate index for vernacular options.	Maxime Dénès	2015-02-17
\|
*	Univs: Complete documentation in refman.	Matthieu Sozeau	2015-01-17
\|
*	Expand Credits for 8.5 and doc on universes	Matthieu Sozeau	2015-01-15
\|
*	Fix some documentation typos.	Guillaume Melquiond	2015-01-08
\|
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
\| \| \| \| \| \| \| \| \| \| \|	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).
*	More documentation of universes.	Matthieu Sozeau	2014-07-25
\|
*	Start documenting universe polymorphism.	Matthieu Sozeau	2014-07-24