coq - The formal proof system

Age	Commit message (Expand)	Author
2016-02-23	Moving tauto.ml4 to a proper ML file.	Pierre-Marie Pédrot
2016-02-22	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot
2016-02-22	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-30	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot
2015-12-24	Removing the last quoted auto tactic in Tauto.	Pierre-Marie Pédrot
2015-12-21	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot
2015-12-05	Fixing compilation with old CAMLPX versions.	Pierre-Marie Pédrot
2015-12-05	Getting rid of some quoted tactics in Tauto.	Pierre-Marie Pédrot
2015-12-04	Removing the last use of valueIn in Tauto.	Pierre-Marie Pédrot
2015-12-03	Fixing Tauto compilation for older versions of OCaml.	Pierre-Marie Pédrot
2015-12-03	Removing the use of tacticIn in Tauto.	Pierre-Marie Pédrot
2015-10-20	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot
2015-05-05	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-04-23	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot
2015-01-23	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot
2015-01-21	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-09-08	Removing antiquotations in Tauto.	Pierre-Marie Pédrot
2014-09-06	Proper interpretation function for tauto.	Pierre-Marie Pédrot
2014-08-18	Reorganization of tactics:	Hugo Herbelin
2014-08-18	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot
2014-08-07	Instead of relying on a trick to make the constructor tactic parse, put	Pierre-Marie Pédrot
2014-06-17	Removing dead code.	Pierre-Marie Pédrot
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-06-27	Removing useless tactic arguments, and using generic arguments	ppedrot
2013-06-22	Now, idtac closures use maps instead of association list.	ppedrot
2013-06-10	Hiding tactic value representations.	ppedrot
2013-02-19	Dir_path --> DirPath	letouzey
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-11-25	Monomorphization (tactics)	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-08-08	Updating headers.	herbelin
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-15	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey
2012-04-15	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin
2012-04-12	"A -> B" is a notation for "forall _ : A, B".	pboutill
2012-03-02	Noise for nothing	pboutill
2012-01-31	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau
2012-01-28	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau
2011-11-24	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot
2011-10-25	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin