coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
\| \| \| \| \| \|	The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps.
*	Univs: fix checker generating undeclared universes.	Matthieu Sozeau	2015-10-02
\|
*	Univs: update checker	Matthieu Sozeau	2015-10-02
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Fix checker's treatment of template polymorphic	Matthieu Sozeau	2015-01-06
\| \| \| \| \|	inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ.
*	checker: Change in library on disk values, now using context_sets instead of	Matthieu Sozeau	2014-12-17
\| \| \| \|	constraints only.
*	Remove unused substitution functions in checker.	Matthieu Sozeau	2014-09-05
\|
*	Fix checker treatment of inductives using subst_instances instead of ↵	Matthieu Sozeau	2014-09-05
\| \| \| \|	subst_univs_levels.
*	Removing dead code in checker/univ.ml.	Pierre-Marie Pédrot	2014-06-10
\|
*	Removing explanations of universe inconsistencies from the checker. They	Pierre-Marie Pédrot	2014-06-10
\| \| \| \|	were never used and were responsible for code duplication.
*	Providing the checker with its own version of the Univ file.	Pierre-Marie Pédrot	2014-06-10
	I also took the opportunity to remove a lot of code not used by the checker.