coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing parsing of constr argument of ltac functions at level 8 in the	Hugo Herbelin	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
\| *	Ident selectors cannot be used inside an Ltac expression.	Cyprien Mangin	2016-06-14
\| *	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
\| *	Remove the need for brackets in goal selectors.	Cyprien Mangin	2016-06-14
\| *	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
\| *	Fix the pretty-printing of goal range selectors.	Cyprien Mangin	2016-06-14
\| *	Add goal range selectors.	Cyprien Mangin	2016-06-14
* \|	STM: proof block detection for par:	Enrico Tassi	2016-06-06
* \|	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/
*	Adding the Print Ltac Signature command.	Pierre-Marie Pédrot	2016-06-05
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"	Hugo Herbelin	2016-04-27
*	Revert "Typo in comment."	Hugo Herbelin	2016-04-27
*	Typo in comment.	Hugo Herbelin	2016-04-27
*	Fixing parsing of constr argument of ltac functions at level 8 in the	Hugo Herbelin	2016-04-27
*	Higher-level API for tactic notations.	Pierre-Marie Pédrot	2016-04-24
*	Moving and enhancing the grammar_tactic_prod_item_expr type.	Pierre-Marie Pédrot	2016-04-14
*	Removing extra spaces in printing arguments of VERNAC EXTEND.	Hugo Herbelin	2016-04-09
*	Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...	Hugo Herbelin	2016-04-09
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21