coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a new evar source to remember the name of evars which were	Hugo Herbelin	2017-01-22
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\
\| *	Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"	Maxime Dénès	2016-11-18
\| *	[stm] Remove STM-related vernaculars	Emilio Jesus Gallego Arias	2016-11-17
\| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
* \|	COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ...	Matej Kosik	2016-10-27
\| *	Complete overhaul of the Arguments vernacular.	Maxime Dénès	2016-10-27
* \|	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