coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
\|\ \
\| \| *	[stdlib] move “Require” out of sections	Vincent Laporte	2018-02-27
\| \|/ \|/\|
* \|	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
\|\ \ \
* \ \ \	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 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
* \| \| \|	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\| \|/ / \|/\| \|
\| * \|	Make list functions returning sumbools transparent	Tej Chajed	2017-11-15
\|/ /
* \|	Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful	Maxime Dénès	2017-10-27
\|\ \
\| * \|	Chaining two tactics in a proof	Raphaël Monat	2017-10-27
\| * \|	Moving from `is_true` to `= true`	Raphaël Monat	2017-10-25
* \| \|	Moving bug numbers to BZ# format in the source code.	Théo Zimmermann	2017-10-19
\| * \|	Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans.	Raphaël Monat	2017-10-12
* \| \|	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\ \ \
\| \| * \|	Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.	Raphaël Monat	2017-10-08
\| \| * \|	Removed leb_not_le (already existing as Nat.leb_nle)	Raphaël Monat	2017-10-08
\| * \| \|	Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)	Pierre Letouzey	2017-10-07
* \| \| \|	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\|/ / /
\| * \|	Changed the statement of leb_not_le; shortened the proof	Raphaël Monat	2017-10-03
\| * \|	Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).	Raphaël Monat	2017-10-03
\| * \|	Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.	Raphaël Monat	2017-10-03
\| * \|	Add leb_not_le: (n <=? m) = false -> n > m.	Raphaël Monat	2017-10-03
\|/ /
* \|	Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...	Maxime Dénès	2017-09-15
\|\ \
\| \| *	weakens an hypothesis of Rle_Rpower	Yves Bertot	2017-09-06
\| \| *	changed statements of Rpower_lt and Rle_power and added	Yves Bertot	2017-09-06
* \| \|	Addressing BZ#5713 (classical_left/classical_right artificially restricted).	Hugo Herbelin	2017-09-03
\| \|/ \|/\|
* \|	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
\| *	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
\|/
*	Merge PR #882: Adding a V8.7 compatibility version number.	Maxime Dénès	2017-07-26
\|\
* \	Merge PR #885: Removing a dummy parameter in some FMapPositive statements.	Maxime Dénès	2017-07-26
\|\ \
* \ \	Merge PR #845: Add Z.mod_div lemma to standard library.	Maxime Dénès	2017-07-26
\|\ \ \