coq - The formal proof system

Age	Commit message (Expand)	Author
2016-07-03	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-07-01	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès
2016-06-09	newring: fix for hack using evars as integers.	Matthieu Sozeau
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
2016-03-18	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-03-10	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau
2016-02-15	CLEANUP: Simplifying the changes done in "kernel/*"	Matej Kosik
2016-02-09	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-08	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-12-07	Fix some typos.	Guillaume Melquiond
2015-09-14	Remove dead code in lazy reduction machine.	Maxime Dénès
2015-03-03	Fix bug #4103: forgot to allow unfolding projections of cofixpoints like	Matthieu Sozeau
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2015-01-06	improve efficiency of the reduction interpreter of coqtop	Bruno Barras
2014-10-11	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau
2014-09-27	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau
2014-09-13	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin
2014-09-05	Rename eta_expand_ind_stacks, fix the one from the checker and adapt	Matthieu Sozeau
2014-09-04	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack
2014-08-28	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau
2014-08-14	Restrict eta-conversion to inductive records, fixing bug #3310.	Matthieu Sozeau
2014-07-29	Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.	Matthieu Sozeau
2014-07-10	Overlooked to remove a change in kernel/closure that made reducing under	Matthieu Sozeau
2014-07-03	Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...	Matthieu Sozeau
2014-05-06	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-04	Fixing coqchk. It was my fault, I misused canonical and user equalities	Pierre-Marie Pédrot
2014-02-09	Small optimizations in Closure:	Pierre-Marie Pédrot
2013-12-15	Do not overallocate closures' named environments in infos. Modifying the access	Pierre-Marie Pédrot
2013-11-24	Slightly more efficient zip function in Closure.	Pierre-Marie Pédrot
2013-11-23	Small allocation improvement in Closure.	Pierre-Marie Pédrot
2013-11-04	Using allocation-free version of Array higher-order function in critical	ppedrot
2013-11-02	Closure: fix an issue with r16959 spotted by Matthieu	letouzey
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-31	Avoiding useless allocations in Closure.	ppedrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Specializing hash functions for widely used types.	ppedrot
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-10-23	cList.index is now cList.index_f, same for index0	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-08	Small optimization in Closure: replaced an index list with an array.	ppedrot