coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing simple induction / destruct from the AST.	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-08-07
*	Removing the "constructor" tactic from the AST.	Pierre-Marie Pédrot	2014-08-07
*	Removing "intros untils" from the AST.	Pierre-Marie Pédrot	2014-08-06
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Adding a syntax "enough" for the variant of "assert" with the order of	Hugo Herbelin	2014-08-05
*	New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.	Arnaud Spiwack	2014-08-01
*	Add [numgoal] to Ltac.	Arnaud Spiwack	2014-08-01
*	Untyped terms in tactic: function [type_term c] to give a typed version of [c].	Arnaud Spiwack	2014-07-29
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot	2014-07-25
*	Distinguish tactics t1;t2 and t1;[t2..].	Arnaud Spiwack	2014-07-24
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	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-06-08
*	Moving the [split] tactic out of the AST.	Pierre-Marie Pédrot	2014-06-06
*	Moving the "specialize" tactic out of the AST. Also removed an obsolete	Pierre-Marie Pédrot	2014-05-22
*	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot	2014-05-22
*	Removing decompose record / sum from the tactic AST.	Pierre-Marie Pédrot	2014-05-21
*	Moving left & right tactics out of the AST.	Pierre-Marie Pédrot	2014-05-21
*	Moving (e)transitivity out of the AST.	Pierre-Marie Pédrot	2014-05-20
*	Tentative to add constr-using primitive tactics without grammar rules.	Pierre-Marie Pédrot	2014-05-20
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	Adds an experimental exactly_once tactical.	aspiwack	2013-11-02
*	Adds a tactical once.	aspiwack	2013-11-02
*	Added the tactical "tac1 + tac2".	aspiwack	2013-11-02
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	Getting rid of IntroPatternArgType.	ppedrot	2013-06-27
*	Removing useless tactic arguments, and using generic arguments	ppedrot	2013-06-27
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	More comments in Genarg.	ppedrot	2013-06-06
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	remove useless hidden_flag in TacMutual(Co)Fix	letouzey	2012-10-06
*	Tacexpr: revised version that doesn't need -rectypes	letouzey	2012-10-06
*	Added a new tactical infoH tac, that displays the names of hypothesis created...	courtieu	2012-10-01
*	Updating headers.	herbelin	2012-08-08
*	The tactic remember now accepts a final eqn:H option (grant wish #2489)	letouzey	2012-07-09
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09