coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Made Tacsubst independent of Auto at linking time so that Tacenv does	Hugo Herbelin	2014-10-01
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	Removing the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	Removing [revert] tactic from the AST.	Pierre-Marie Pédrot	2014-09-02
*	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot	2014-09-01
*	Type-safe version of genarg list / pair / opt functions.	Pierre-Marie Pédrot	2014-08-29
*	Moving the TacAlias node out of atomic tactics.	Pierre-Marie Pédrot	2014-08-18
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	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
*	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
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	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 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
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Closing bug #3260	Julien Forest	2014-04-14
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	Removing RefArgType generic argument.	Pierre-Marie Pédrot	2013-12-01
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	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
*	Removing SortArgType.	ppedrot	2013-07-05
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05
*	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot	2013-07-02
*	Removed the ad-hod handling of wit_tacticn.	ppedrot	2013-07-02
*	Getting rid of IntroPatternArgType.	ppedrot	2013-06-27
*	Removing useless tactic arguments, and using generic arguments	ppedrot	2013-06-27
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21