coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Readback for int31 values from native compiler.	Maxime Dénès	2014-04-09
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Native compiler: timing info for reification in debug mode.	mdenes	2013-03-25
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey	2013-03-12
*	More monomorphization.	ppedrot	2013-03-05
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22