coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-12-14	Modulification of identifier	ppedrot
2012-09-14	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
2012-03-02	Noise for nothing	pboutill
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
2010-12-25	Rename mkR* smart constructors (mostly in funind)	glondu
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-24	Rename files in funind to respect new conventions	glondu