coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	- Fix abstract forgetting about new constraints.	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-05	closing bug 3037	Julien Forest
2014-03-05	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-02-14	fast correction of bug #3234	Julien Forest
2013-12-24	Qed: feedback when type checking is done	Enrico Tassi
2013-12-04	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack
2013-11-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-21	Add Acc_intro_generator on top of all wf function proof (much much faster exe...	Julien Forest
2013-11-08	Porting Tactics.assumption to the new engine.	ppedrot
2013-11-02	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-08-30	recdef: restore old semantics (pre STM)	gareuselesinge
2013-08-22	Nicer code concerning dirpaths and modpath around Lib	letouzey
2013-08-22	Less "Coq" strings everywhere	letouzey
2013-08-08	calling interp by hand is forbidden	gareuselesinge
2013-08-08	get rid of closures in global/proof state	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 11)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-18	Minor code cleanups, especially take advantage of Dir_path.is_empty	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-18	Modulification of name	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	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-08-08	Updating headers.	herbelin
2012-07-13	Fixes r15610 (A new status Unsafe in Interface).	aspiwack
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-01	More cleaning	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot