coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Improving formatting of output of "Test table".	herbelin	2013-01-27
*	Reductionops: whd_state_gen can take and answers a cst_stack too	pboutill	2013-01-24
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	- Fix evarconv so that we have complete eta-conversion:	msozeau	2013-01-22
*	Evarconv: Check stack before term in Canonical Structure approuval	pboutill	2013-01-18
*	Awful heuristic to refold mutual fixpoint in reductionops	pboutill	2012-12-21
*	Fixup and comment reductionops	pboutill	2012-12-21
*	Reductionops reduction machine can refold constant	pboutill	2012-12-19
*	Evarconv.Pseudorigid erasure	pboutill	2012-12-19
*	Array.create is deprecated	pboutill	2012-12-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Taking into account the possibility of having a type of type which is	herbelin	2012-12-18
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18
*	Factorization of the elim unif flag with the default flag. Since	herbelin	2012-12-18
*	Do not display REVERTcast inserted by reduction tactics (unless printing all).	herbelin	2012-12-17
*	Fixed a bug in the algorithm trying to elaborate a "match" return predicate.	herbelin	2012-12-17
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Evarconv: Fix #2936 + comments	pboutill	2012-11-28
*	Reductionops uses Closure.reds	pboutill	2012-11-28
*	Removed some FIXME related to equality on universes.	ppedrot	2012-11-26
*	Small cleaning of interface in Univ	ppedrot	2012-11-26
*	More equality functions	ppedrot	2012-11-25
*	Fixed bug #2930: folded let-in's were hiding a violation to the occur	herbelin	2012-11-25
*	Added a constr_pattern_eq	ppedrot	2012-11-23
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Cleaning and small optimization in CList.	ppedrot	2012-11-20
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Removing another bunch of generic equalities	ppedrot	2012-11-08
*	Reversed roles of undefined/defined evars in Evd, thus saving precious	ppedrot	2012-11-03
*	Removed many calls to OCaml generic equality. This was done by	ppedrot	2012-10-29
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	univ inconsistency error message gives evidence of a cycle	barras	2012-10-17
*	Adapt pieces of code needing -rectypes	letouzey	2012-10-06
*	Improving error message when abtraction over goal (abstract_list_all	herbelin	2012-10-04
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	More cleaning in CArray...	ppedrot	2012-09-18
*	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey	2012-09-18
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14