coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \|	Merge remote-tracking branch 'origin/pr/166' into trunk	Enrico Tassi	2016-06-14
\|\ \
* \ \	Merge branch "LtacProf for trunk" (PR #165).	Pierre-Marie Pédrot	2016-06-14
\|\ \ \
* \| \| \|	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\|\ \ \ \
\| \| * \| \|	LtacProf for Coq trunk	Jason Gross	2016-06-05
\| \|/ / / \|/\| \| \|
\| * \| \|	Fix incorrect checking of library checksums.	Maxime Dénès	2016-06-05
* \| \| \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| \| * \|	coqc: support -o option to specify output file name	Enrico Tassi	2016-05-19
\| \|/ / \|/\| \|
* \| \|	Dyn: simplify API introducing an Easy submodule	Enrico Tassi	2016-05-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\\| \|
\| * \|	Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.	Pierre-Marie Pédrot	2016-05-08
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\| \|
\| * \|	Fix bug #4292: Unexpected functor objects.	Pierre-Marie Pédrot	2016-05-03
* \| \|	Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...	Matthieu Sozeau	2016-04-04
\|\ \ \
* \ \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Fix #4607: do not read native code files if native compiler was disabled.	Maxime Dénès	2016-03-04
* \| \| \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \ \ \
* \ \ \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \ \ \| \| \|/ / / \| \|/\| \| \|
\| \| * \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ / / \|/\| \| \|
\| * \| \|	Optimizing the universes_of_constr_function.	Pierre-Marie Pédrot	2016-02-03
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\| \| \|
\| * \| \|	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \| \|
\| * \| \|	Update copyright headers.	Maxime Dénès	2016-01-20
\| * \| \|	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \| \| \|	Changing "P is assumed" to "P is declared".	Hugo Herbelin	2016-01-14
* \| \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \ \
\| * \| \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \| \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\ \ \ \ \ \| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
* \| \| \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \| \| \|	Remove keys for evar and meta, since they cannot occur.	Guillaume Melquiond	2016-01-02
* \| \| \| \|	Remove some useless type declarations.	Guillaume Melquiond	2016-01-02
* \| \| \| \|	Remove Library.mem, which is pointless since 8.5.	Guillaume Melquiond	2015-12-31
* \| \| \| \|	Avoid a pointless conversion/copy.	Guillaume Melquiond	2015-12-22
* \| \| \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
* \| \| \| \|	Move the From logic to Loadpath.expand_path.	Guillaume Melquiond	2015-12-22
* \| \| \| \|	Do not query module files that have already been loaded.	Guillaume Melquiond	2015-12-22
\| \|/ / / \|/\| \| \|
* \| \| \|	COMMENTS: added to some variants of "Globalnames.global_reference" type.	Matej Kosik	2015-12-18
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\| \| \|
* \| \| \|	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot	2015-12-05
* \| \| \|	Specializing the Dyn module to each usecase.	Pierre-Marie Pédrot	2015-12-04
\| * \| \|	Univs: fix bug #4443.	Matthieu Sozeau	2015-12-03
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\| \| \|
\| * \| \|	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
\| * \| \|	Avoid recording spurious Set <= Top.i constraints which are always	Matthieu Sozeau	2015-11-27
* \| \| \|	More efficient implementation of equality-up-to-universes in Universes.	Pierre-Marie Pédrot	2015-11-26
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\| \| \|