coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	- Allow parsing of @const@{instance} for specifying universe instances of pol...	Matthieu Sozeau	2014-06-04
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	More monomorphization.	ppedrot	2013-03-05
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Yet a new reduction tactic in Coq : cbn	pboutill	2012-12-21
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	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
*	Updating headers.	herbelin	2012-08-08
*	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey	2012-08-07
*	Bigint: avoid dependency over Pp	letouzey	2012-07-30
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Fixing some inconsistencies of constr printer wrt constr parser	herbelin	2012-06-19
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29