coq - The formal proof system

Age	Commit message (Expand)	Author
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-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	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-01	Fixing pervasive comparisons	Pierre-Marie Pédrot
2014-01-20	bug correction in proving principles of function	jforest
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-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-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-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-08-08	get rid of closures in global/proof state	gareuselesinge
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 11)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey
2013-03-12	Recdef: an anomaly isn't so anomalous, occurs in 1618.v	letouzey
2013-02-26	kernel/declarations becomes a pure mli	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-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-10-06	remove useless hidden_flag in TacMutual(Co)Fix	letouzey
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
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-06-01	More cleaning	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	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-03-30	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey
2012-03-02	Noise for nothing	pboutill
2012-03-01	New version of recdef :	jforest
2011-06-18	Relaxed the constraint introduced in r14190 that froze the existing	herbelin
2011-06-10	Call process_vernac_interp_error before calling Errors.print in	herbelin
2011-05-13	A new mechanism to handle errors.	aspiwack
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu