coq - the Coq proof assistant

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