coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	correct some ends of .mllib files (avoid a broken tolink.ml)	letouzey	2012-08-24
*	Unification in Evar_conv uses an abstract machine state	pboutill	2012-08-09
*	Updating headers.	herbelin	2012-08-08
*	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey	2012-08-07
*	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin	2012-07-29
*	Fix eta contraction in Reductionops	pboutill	2012-07-25
*	Reductionops refactoring	pboutill	2012-07-20
*	Fixing test-suite	pboutill	2012-07-20
*	flex_maybeflex factoring	pboutill	2012-07-12
*	miller_pfenning unification code factoring	pboutill	2012-07-12
*	flex_kind_of_term does not have a copy of term	pboutill	2012-07-12
*	evar reduction is already made by whd_*	pboutill	2012-07-12
*	tacred uses stack_reduction_function instead of state_reduction_function	pboutill	2012-07-12
*	Fix regression introduced in r15418 that broke MathClasses. In program mode, ...	msozeau	2012-07-11
*	Another correction to the dependent existential variable printing	aspiwack	2012-07-10
*	Continuing r15459: it helps testing occur-check early in some	herbelin	2012-07-06
*	Practical fix for bug #1206 (anomaly raised in pretyping instead of	herbelin	2012-07-06