coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "Revert "Improve the interpretation scope of arguments of an ltac matc...	Maxime Dénès	2016-07-04
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	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
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
*	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
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Removing useless generic arguments.	Pierre-Marie Pédrot	2016-05-04
*	Revert "In the short term, stronger invariant on the syntax of TacAssert, what"	Hugo Herbelin	2016-04-27
*	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin	2016-04-27
*	Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...	Hugo Herbelin	2016-04-27
*	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin	2016-04-27
*	Honor parsing and printing levels for tactic entry in TACTIC EXTEND and	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
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21