coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-10-22	Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.	Arnaud Spiwack
2014-09-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2014-08-18	Reorganization of tactics:	Hugo Herbelin
2014-08-05	Experimentally adding an option for automatically erasing an	Hugo Herbelin
2014-06-18	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau
2014-06-12	Passing some tactics to the new monad type.	Pierre-Marie Pédrot
2014-06-08	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot
2014-06-08	Enforce a correct exception handling in declaration_hooks	Enrico Tassi
2014-05-06	Fix funind w.r.t. universes	Matthieu Sozeau
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
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-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	Rtree : cleanup of the comparing code	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-30	Fix typo in error message	gareuselesinge
2013-08-08	get rid of closures in global/proof state	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge
2013-05-06	States: frozen states can hold closures	gareuselesinge
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
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-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-31	correcting a little bug in Function	jforest
2012-09-24	Fixing a bug introduced in Funind plugin when reorganizing the CList	ppedrot
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
2012-09-15	Some documentation and cleaning of CList and Util interfaces.	ppedrot
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	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-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-30	Getting rid of Pp.msg	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Glob_term now mli-only, operations now in Glob_ops	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-04-23	correct abort in Function when a proof of inversion fails	letouzey
2012-03-23	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey
2012-03-02	Noise for nothing	pboutill
2012-03-01	various corrections in invfun due to a modification in induction	jforest