coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove declare_object for SsrHave NoTCResolution.	Maxime Dénès	2018-07-19
*	Remove fourier plugin	Maxime Dénès	2018-07-17
*	Tactic deprecation machinery	Maxime Dénès	2018-07-12
*	Merge PR #7920: Generic syntax for attributes	Maxime Dénès	2018-07-09
\|\
* \|	Mention the removal of Emacs modes in CHANGES.	Théo Zimmermann	2018-07-08
* \|	Merge PR #7921: Archive the `gallina` tool	Maxime Dénès	2018-07-07
\|\ \
\| \| *	Document attributes.	Vincent Laporte	2018-07-03
\| \|/ \|/\|
* \|	Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands	Pierre-Marie Pédrot	2018-07-03
\|\ \
\| * \|	hints: add Hint Variables/Constants Opaque/Transparent commands	Matthieu Sozeau	2018-07-02
* \| \|	Document option Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\|/ /
* \|	CHANGES for 8.8.1.	Théo Zimmermann	2018-06-28
* \|	Merge PR #7866: Implementation of mutual records in the higher strata	Maxime Dénès	2018-06-28
\|\ \
* \| \|	Fix #7723: vm_compute segfaults with universe polymorphism	Maxime Dénès	2018-06-27
\| \| *	Archive the `gallina` tool	Vincent Laporte	2018-06-25
\| \|/ \|/\|
\| *	Added mention of mutual records to CHANGES.	Pierre-Marie Pédrot	2018-06-24
\|/
*	[ssr] implement {}/v as a short hand for {v}/v when v is an id	Enrico Tassi	2018-06-22
*	[ssr] simplify delayed clears	Enrico Tassi	2018-06-22
*	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
*	Fix #7615: Functor inlining drops universe substitution.	Pierre-Marie Pédrot	2018-06-07
*	Make direct invocations of `simple apply` obey `Opaque` directive.	Maxime Dénès	2018-06-05
*	Merge PR #7229: Deprecate implicit tactic solving.	Hugo Herbelin	2018-06-04
\|\
* \	Merge PR #7486: Update old parts of CHANGES to use current bug numbers.	Hugo Herbelin	2018-06-04
\|\ \
\| \| *	Documenting the deprecation.	Pierre-Marie Pédrot	2018-06-04
\| \|/ \|/\|
* \|	Add CHANGES entry	Maxime Dénès	2018-05-28
* \|	[tactics] Remove anonymous fix/cofix form.	Emilio Jesus Gallego Arias	2018-05-24
* \|	[stm] Make toplevels standalone executables.	Emilio Jesus Gallego Arias	2018-05-21
* \|	Document nested proofs and associated option.	Théo Zimmermann	2018-05-17
\| *	Update old parts of CHANGES to use current bug numbers.	Théo Zimmermann	2018-05-11
* \|	Notations: advertize that distinct "only parsing"/"only printing" rules work.	Hugo Herbelin	2018-05-11
\|/
*	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02
*	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
*	Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"	Pierre-Marie Pédrot	2018-04-23
\|\
* \|	Fix typo in CHANGES.	Maxime Dénès	2018-04-16
* \|	Mention other deprecations and fixes in CHANGES	Maxime Dénès	2018-04-16
* \|	CHANGES: document COQFLAGS change	Ralf Jung	2018-04-16
* \|	Merge PR #7200: [ltac] Deprecate nameless fix/cofix.	Maxime Dénès	2018-04-16
\|\ \
* \| \|	Add missing CHANGES entry for #6169.	Théo Zimmermann	2018-04-14
\| \| *	Making tactic-in-term aware of "Set Ltac Debug".	Hugo Herbelin	2018-04-13
\| \|/ \|/\|
\| *	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
\|/
*	Merge PR #7103: Fix #7101: STM delegation policy broken	Enrico Tassi	2018-04-09
\|\
* \|	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
\|/ /
\| *	Fix #7101: STM delegation policy broken	Maxime Dénès	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