coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Modulification of name	ppedrot	2012-12-18
*	Fixing parsing of specific primitive tokens used as notations for patterns	herbelin	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot	2012-12-14
*	More equality functions	ppedrot	2012-11-25
*	More monomorphizations	ppedrot	2012-11-13
*	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
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29