coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
*	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
*	Moving Tacexpr to ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
*	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
*	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
*	Making Vernacexpr independent from Tacexpr.	Pierre-Marie Pédrot	2016-09-08
*	Support qualified identifiers in Show Match (bug #5050).	Guillaume Melquiond	2016-08-27
*	Add and document match, fix and cofix reduction flags.	Maxime Dénès	2016-07-01
*	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
*	COMMENTS: Vernacexpr.extend_name	Matej Kosik	2016-06-20
*	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
*	par: like all: but in parallel	Enrico Tassi	2016-06-17
*	Extend Hint Mode to handle the no-head-evar case	Matthieu Sozeau	2016-06-16
*	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
* \	Merge remote-tracking branch 'github/pr/194' into trunk	Maxime Dénès	2016-06-16
\|\ \
\| \| *	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
\| \| *	Add goal range selectors.	Cyprien Mangin	2016-06-14
\| * \|	Adding an only printing flag to notations.	Pierre-Marie Pédrot	2016-06-07
\| * \|	Removing the use to Egramcoq.recover_constr_grammar.	Pierre-Marie Pédrot	2016-06-07
\| \|/
* /	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/
*	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 pointless field NPatVar. It does not make sense to have Meta	Hugo Herbelin	2016-06-02
*	AlistNsep token now accepts an arbitrary separator.	Pierre-Marie Pédrot	2016-05-10
*	Simpler data structure for Arules token.	Pierre-Marie Pédrot	2016-05-10
*	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
*	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
*	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 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
*	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\
* \|	Getting rid of the "_mods" parsing entry.	Pierre-Marie Pédrot	2016-04-01
* \|	Moving type_uconstr to Pretyping.	Pierre-Marie Pédrot	2016-03-25
* \|	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Print Ltac to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Tactic Notation to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving VernacSolve to an EXTEND-based definition.	Pierre-Marie Pédrot	2016-03-19
* \|	Allowing generalized rules in typed symbols.	Pierre-Marie Pédrot	2016-03-19
* \|	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin	2016-03-13
* \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \|	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
* \|	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