coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixes bug #2678	aspiwack	2012-07-06
*	Cleaning opening of the standard List module.	ppedrot	2012-06-28
*	Added a .mli to pretyping/program.ml	ppedrot	2012-06-25
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:	msozeau	2012-06-21
*	Fixing use of an error instead of a boolean result in the unification	herbelin	2012-06-20
*	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin	2012-06-20
*	Reductionops abstract machine uses Zcase & Zfix stack node.	pboutill	2012-06-15
*	Reductionops : Better abstract machine stack utilities	pboutill	2012-06-15
*	Replacing some str with strbrk	ppedrot	2012-06-04
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	More cleaning	ppedrot	2012-06-01
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01