coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tweak printing boxes for unicode binders	Ralf Jung	2018-06-10
*	Merge PR #7690: Fixing typos in file Berardi.v	Pierre-Marie Pédrot	2018-06-05
\|\
* \|	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	2018-06-04
\| *	Fixing typos in file Berardi.v	Hugo Herbelin	2018-06-03
\|/
*	Protecting against a "deprecated cofix" warning.	Hugo Herbelin	2018-04-16
*	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
*	Merge PR #6820: Tacticals assert_fails and assert_succeeds	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6155: Get rid of ' notation for Zpos in QArith	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #6937: Add empty compat file for Coq 8.8	Maxime Dénès	2018-03-09
\|\ \ \
* \ \ \	Merge PR #6522: Fix core hint database issue #6521	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
\|\ \ \ \ \ \
* \| \| \| \| \| \|	[stdlib] Do not use “Require” inside sections	Vincent Laporte	2018-03-07
\| \| \| \| * \| \|	Add empty compat file for Coq 8.8	Jason Gross	2018-03-07
\| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6744: Add String.concat	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Remove all uses of Focus in standard library.	Théo Zimmermann	2018-03-04
* \| \| \| \| \| \| \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
* \| \| \| \| \| \| \|	Remove VOld compatibility flag.	Théo Zimmermann	2018-03-02
* \| \| \| \| \| \| \|	Turn warning for deprecated notations on.	Théo Zimmermann	2018-03-02
* \| \| \| \| \| \| \|	Remove the deprecation for some 8.2-8.5 compatibility aliases.	Théo Zimmermann	2018-03-02
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	Uniform spacing layout in Tactics.v.	Hugo Herbelin	2018-02-28
\| \| \| \| \| \| *	Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).	Hugo Herbelin	2018-02-28
* \| \| \| \| \| \|	Merge PR #6852: [stdlib] move “Require” out of sections	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	[stdlib] move “Require” out of sections	Vincent Laporte	2018-02-27
\| \|/ / / / / / \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	Add String.concat	Jason Gross	2018-02-24
\| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6599: Decimals in prelude	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \
\| \| * \| \| \| \|	Decimal goodies : conversion to/from Coq strings	Pierre Letouzey	2018-02-20
\| \| * \| \| \| \|	Decimal: proofs that conversions from/to nat,N,Z are bijections	Pierre Letouzey	2018-02-20
\| \| * \| \| \| \|	Decimal: simple representation of base-10 numbers	Pierre Letouzey	2018-02-20
* \| \| \| \| \| \|	Trying a hack to support {'pat\|P} without breaking compatibility.	Hugo Herbelin	2018-02-20
* \| \| \| \| \| \|	Adding notations of the form "{'pat\|P}", "exists2 'pat, P & Q", etc.	Hugo Herbelin	2018-02-20
* \| \| \| \| \| \|	More structured printing in unicode notations for binders.	Hugo Herbelin	2018-02-20
* \| \| \| \| \| \|	User-level support for Gonthier-Ssreflect's "if t then pat then u else v".	Hugo Herbelin	2018-02-20
\| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \
\| \| \| \| * \| \|	Add notation {x & P} for sigT	Tej Chajed	2018-02-12
\| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6139: Make list functions returning sumbools transparent	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Document between and exists_between types.	Ismail	2018-01-08
\| \| * \| \| \| \|	Remove dir-locals and ship suggested helper hooks instead.	Gaëtan Gilbert	2018-01-06
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| \| * \|	Fix core hint database issue #6521	Anton Trunov	2018-01-03
\| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Fix warning about shadowing a global name.	Gaëtan Gilbert	2017-12-19
* \| \| \| \|	Add named timers to LtacProf	Jason Gross	2017-12-14
* \| \| \| \|	Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts	Maxime Dénès	2017-12-12
\|\ \ \ \ \
* \| \| \| \| \|	Axiom-free proof of eta expansion.	Jasper Hugunin	2017-12-11
* \| \| \| \| \|	Remove most uses of function extensionality in Program.Combinators	Jasper Hugunin	2017-12-09
\| * \| \| \| \|	Additional rewrite lemmas on Ensembles, in Powerset_facts	Joachim Breitner	2017-12-06
\|/ / / / /
\| \| * \| \|	proposed fix for issue #3213: extra variable m in Lt.S_pred	fredokun	2017-12-01