coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
\| \| \| \| \| \| \| \| \|	This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option.
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
\|
*	Fix checker to handle projections with eta and universe polymorphism correctly.	Matthieu Sozeau	2014-09-06
\|
*	Fix test-suite file.	Matthieu Sozeau	2014-08-18
\|
*	Changed syntax of explicit universes.	Matthieu Sozeau	2014-06-23
\|
*	- Better parsing and printing of named universes: Type{ident} and ↵	Matthieu Sozeau	2014-06-04
	foo@{(ident\|Prop\|Set\|Type\|' ')*} (user given names are still write only). - Add test-suite file for named universes.