coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
*	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
*	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin	2016-06-16
*	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
*	Removing "rename" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Removing "exact" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Removing "double induction" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Revert "In the short term, stronger invariant on the syntax of TacAssert, what"	Hugo Herbelin	2016-04-27
*	In the short term, stronger invariant on the syntax of TacAssert, what	Hugo Herbelin	2016-04-27
*	Attempt to slightly improve abusive "Collision between bound	Hugo Herbelin	2016-04-27
*	Removing the ad-hoc tactic_expr type.	Pierre-Marie Pédrot	2016-04-11
*	Expliciting the fact that the atomic tactic type is self-contained.	Pierre-Marie Pédrot	2016-04-10
*	Moving type_uconstr to Pretyping.	Pierre-Marie Pédrot	2016-03-25
*	Moving Ltac traces to Tacexpr and Tacinterp.	Pierre-Marie Pédrot	2016-03-06
*	Removing the UConstr entry of the tactic_arg AST.	Pierre-Marie Pédrot	2016-03-04
*	Moving the "move" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Moving the "exists" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Moving the "symmetry" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Moving the "generalize dependent" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Moving the "clearbody" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Moving the "cofix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Moving the "fix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
*	Removing the MetaIdArg entry of tactic expressions.	Pierre-Marie Pédrot	2016-02-24
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
* \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
* \|	Getting rid of the dynamic node of the tactic AST.	Pierre-Marie Pédrot	2015-12-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
* \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	Code documentation of the TACTIC/VERNAC EXTEND macros.	Pierre-Marie Pédrot	2015-06-29
* \|	Remove other types not carried by interpretations in `Tacexpr`.	Arnaud Spiwack	2015-06-25
* \|	Remove useless `and_short_name` in interpreted level in `Tacexpr`.	Arnaud Spiwack	2015-06-25
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-10
\|\\|
\| *	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
* \|	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
*	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack	2014-12-23
*	Fix compilation error in some configurations.	Arnaud Spiwack	2014-12-23
*	Add a backtracking version of Ltac's [match].	Arnaud Spiwack	2014-12-19
*	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack	2014-12-12
*	Removing a unused boolean in the TacMove node of tacexpr AST.	Pierre-Marie Pédrot	2014-11-09
*	Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.	Arnaud Spiwack	2014-11-01