coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix #6404 - Print tactics called by ML tactics	Jason Gross	2018-04-02
*	Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)	Pierre-Marie Pédrot	2018-04-01
\|\
* \|	Add CHANGES for removing Implicit Arguments and Arguments Scope	Jasper Hugunin	2018-03-30
\| *	Supporting fix/cofix in Ltac pattern-matching (wish #7092).	Hugo Herbelin	2018-03-28
\|/
*	Merge PR #7018: Fix typo in CHANGES.	Maxime Dénès	2018-03-23
\|\
* \|	update CHANGES	Enrico Tassi	2018-03-23
\| *	Fix typo in CHANGES.	Théo Zimmermann	2018-03-19
\|/
*	Add some missing entries in CHANGES	Maxime Dénès	2018-03-15
*	[doc] Document removal of deprecated options.	Emilio Jesus Gallego Arias	2018-03-09
*	Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\ \
\| \| *	Revert "Merge PR #873: New strategy based on open scopes for deciding which n...	Maxime Dénès	2018-03-09
* \| \|	Merge PR #6923: Export options	Maxime Dénès	2018-03-09
\|\ \ \ \| \|_\|/ \|/\| \|
\| \| *	Documentation for Cumulativity Weak Constraints.	Gaëtan Gilbert	2018-03-09
* \| \|	Merge PR #6480: Allow Prop as source for coercions	Maxime Dénès	2018-03-09
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6820: Tacticals assert_fails and assert_succeeds	Maxime Dénès	2018-03-09
\|\ \ \
\| \| \| *	Documenting the Export modifier for options in CHANGES.	Pierre-Marie Pédrot	2018-03-09
\| \|_\|/ \|/\| \|
\| \| *	doc and changes for coercion from prop/type	charguer	2018-03-09
\| \|/ \|/\|
* \|	Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry...	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...	Maxime Dénès	2018-03-08
\|\ \ \
* \ \ \	Merge PR #6743: Add notation {x & P} for sigT	Maxime Dénès	2018-03-08
\|\ \ \ \
* \ \ \ \	Merge PR #6909: Deprecate Focus and Unfocus	Maxime Dénès	2018-03-08
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \
* \| \| \| \| \| \|	[vernac] Warn when using “Require” in a section	Vincent Laporte	2018-03-07
* \| \| \| \| \| \|	Merge PR #6744: Add String.concat	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \
\| \| \| \| \| \| * \|	Add CHANGES and man entry for coqdep learning _CoqProject.	Gaëtan Gilbert	2018-03-06
\| \| \| \| \| * \| \|	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
\| \| \| \| \| \|/ /
* \| \| \| \| \| \|	CHANGES and tests for with Definition @{univs}	Gaëtan Gilbert	2018-03-05
\| \| \| * \| \| \|	Deprecate Focus and Unfocus.	Théo Zimmermann	2018-03-05
\| \| \| \| \|/ / \| \| \| \|/\| \|
* \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \
\| * \| \| \| \| \|	CHANGES entry for #6791.	Théo Zimmermann	2018-03-02
\| \| \|_\|/ / / \| \|/\| \| \| \|
* / \| \| \| \|	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
\|/ / / / /
\| \| \| \| *	Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).	Hugo Herbelin	2018-02-28
\| * \| \| \|	Add String.concat	Jason Gross	2018-02-24
\|/ / / /
* \| \| \|	Merge PR #6599: Decimals in prelude	Maxime Dénès	2018-02-24
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`	Maxime Dénès	2018-02-21
\|\ \ \ \
\| \| * \| \|	Add CHANGES entry for decimals in prelude	Jason Gross	2018-02-20
* \| \| \| \|	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin	2018-02-20
* \| \| \| \|	More flexibility in locating or referring to a notation.	Hugo Herbelin	2018-02-20
* \| \| \| \|	A first step at refreshing and documenting the new feature.	Hugo Herbelin	2018-02-20
* \| \| \| \|	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20
\| \|/ / / \|/\| \| \|
\| \| * \|	Implement name mangling option	Jasper Hugunin	2018-02-17
\| \|/ / \|/\| \|
\| * \|	Extend `zify_N` with knowledge about `N.pred`	Joachim Breitner	2018-02-14
* \| \|	CHANGES for 8.7.2.	Théo Zimmermann	2018-02-14
\|/ /
* \|	Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)	Maxime Dénès	2018-02-14
\|\ \
\| * \|	Add CHANGES entry for #1047	Tej Chajed	2018-02-13
\| \| *	Add notation {x & P} for sigT	Tej Chajed	2018-02-12
\| \|/
* /	CHANGES for universe variance	Gaëtan Gilbert	2018-02-12
\|/
*	Merge PR #6629: Archive COMPATIBILITY	Maxime Dénès	2018-01-23
\|\
\| *	Move the mention of the removal of Qed exporting at the right place.	Théo Zimmermann	2018-01-22