coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	checker: remove unused per-constant reduction flags.	Gaëtan Gilbert	2018-02-02
*	[checker] Avoid relying on canonical names.	Maxime Dénès	2018-01-25
*	[checker] Remove duplicated function	Maxime Dénès	2018-01-25
*	[checker] Better error message for bad recursive trees	Maxime Dénès	2018-01-25
*	fix space in coqchk error	Ralf Jung	2018-01-24
*	Fix #6618: coqchk fails with "ill-typed term".	Pierre-Marie Pédrot	2018-01-20
*	Actually use the strategy information in the checker.	Pierre-Marie Pédrot	2018-01-14
*	Store the conversion oracle in constant and inductive definitions.	Pierre-Marie Pédrot	2018-01-14
*	Add interfaces for checker and remove dead code.	Maxime Dénès	2018-01-10
*	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
*	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
*	Merge PR #6277: Qualified import in coqchk	Maxime Dénès	2017-12-07
\|\
* \	Merge PR #6303: Remove redundant Zcase from the checker.	Maxime Dénès	2017-12-07
\|\ \
* \ \	Merge PR #6266: Safe unmarshalling in the checker	Maxime Dénès	2017-12-05
\|\ \ \
\| \| * \|	Remove redundant Zcase from the checker.	Pierre-Marie Pédrot	2017-12-02
\| \|/ / \|/\| \|
\| \| *	Documenting the -Q flag of coqchk.	Pierre-Marie Pédrot	2017-12-01
\| \| *	Forbid implicitly relative names in the checker.	Pierre-Marie Pédrot	2017-11-29
\| \| *	Mark the -I option in coqchk as deprecated and merge it with -Q.	Pierre-Marie Pédrot	2017-11-29
\| \| *	Add a -Q option to coqchck.	Pierre-Marie Pédrot	2017-11-29
\| \|/ \|/\|
* \|	Allow to pass physical files to coqchk.	Pierre-Marie Pédrot	2017-11-29
* \|	Adding an interface file for checker/check.ml.	Pierre-Marie Pédrot	2017-11-28
\| *	Use safe demarshalling in the checker.	Pierre-Marie Pédrot	2017-11-28
\| *	Use large arrays in the checker demarshaller.	Pierre-Marie Pédrot	2017-11-28
\|/
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
* \|	Truncate strings in votour to 1024 characters.	Pierre-Marie Pédrot	2017-11-23
* \|	Bypass int and string representation in votour when it's incorrect.	Pierre-Marie Pédrot	2017-11-23
* \|	Tail-recursive list traversal in votour.	Pierre-Marie Pédrot	2017-11-23
* \|	Implement a tail-recursive traversal of the object in votour.	Pierre-Marie Pédrot	2017-11-22
\|/
*	Merge PR #6065: [api] Deprecate all legacy uses of Names in core.	Maxime Dénès	2017-11-13
\|\
\| *	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
* \|	[feedback] Helper to print feedback messages in the console.	Emilio Jesus Gallego Arias	2017-11-06
\|/
*	Merge PR #1075: Re-enable checker error messages	Maxime Dénès	2017-09-25
\|\
\| *	Fix -silent flag of coqchk after ff918e4.	Maxime Dénès	2017-09-21
\| *	Adapt checker to change in locations.	Maxime Dénès	2017-09-21
\| *	[checker] Add missing Feedback printer (BZ#5587)	Emilio Jesus Gallego Arias	2017-09-21
* \|	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias	2017-09-20
\|/
*	Merge PR #955: Do not hashcons universes beforehand	Maxime Dénès	2017-09-15
\|\
\| *	Do not hashcons universes beforehand.	Pierre-Marie Pédrot	2017-09-01
* \|	Statically enforcing that module types have no retroknowledge.	Pierre-Marie Pédrot	2017-08-29
* \|	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot	2017-08-29
\|/
*	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\
\| *	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
* \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\|/
*	Fixing the checker w.r.t. wrongly used abstract universe contexts.	Pierre-Marie Pédrot	2017-07-19
*	Properly handling polymorphic inductive subtyping in the checker.	Pierre-Marie Pédrot	2017-07-11
*	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
*	Less footguns in universe handling: remove subst_instance_context.	Pierre-Marie Pédrot	2017-07-11
*	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04