coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\ \
\| \| *	Add command 'Set foo Append "bar"' for appending to an option (bug #5109).	Guillaume Melquiond	2016-10-01
\| \|/
\| *	Merge remote-tracking branch 'github/pr/299' into v8.6	Maxime Dénès	2016-09-30
\| \|\
\| * \|	Fix bug #4798: compat notations should not modify the parser.	Pierre-Marie Pédrot	2016-09-29
\| * \|	Arguments: cleanup + detect discrepancy rename/implicit (#3753)	Enrico Tassi	2016-09-29
\| \| *	Fix bug #4869, allow Prop, Set, and level names in constraints.	Matthieu Sozeau	2016-09-29
\| \|/
* \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \|	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