coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6820: Tacticals assert_fails and assert_succeeds	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 #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \
* \| \| \| \|	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
\| * \| \| \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/ / / /
* \| \| \|	Merge PR #6599: Decimals in prelude	Maxime Dénès	2018-02-24
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
\| * \| \|	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
* \| \| \|	User-level support for Gonthier-Ssreflect's "if t then pat then u else v".	Hugo Herbelin	2018-02-20
\|/ / /
\| * /	Add notation {x & P} for sigT	Tej Chajed	2018-02-12
\|/ /
\| *	Fix core hint database issue #6521	Anton Trunov	2018-01-03
\|/
*	Add named timers to LtacProf	Jason Gross	2017-12-14
*	Moving bug numbers to BZ# format in the source code.	Théo Zimmermann	2017-10-19
*	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
*	Fix typo in documentation for identity	Tej Chajed	2017-07-05
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	plugins/ltac : avoid spurious .cmxs files	Pierre Letouzey	2017-06-15
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
*	Merge PR#385: Equality of sigma types	Maxime Dénès	2017-06-13
\|\
* \|	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik	2017-06-01
\| *	More uniform indentation of sigma lemmas	Jason Gross	2017-05-28
\| *	Give explicit proof terms to proj2_sig_eq etc.	Jason Gross	2017-05-28
\| *	Use the rew dependent notation in ex, ex2 proofs	Jason Gross	2017-05-28
\| *	Make theorems about ex equality Qed	Jason Gross	2017-05-28
\| *	Make new proofs of equality Qed	Jason Gross	2017-05-28
\| *	Add some more comments about sigma equalities	Jason Gross	2017-05-28
\| *	Remove motive argument from [rew dependent]	Jason Gross	2017-05-28
\| *	Use a local [rew dependent] notation	Jason Gross	2017-05-28
\| *	Add forward-chaining versions: [eq_sig*_uncurried]	Jason Gross	2017-05-28
\| *	Use notation for sigT	Jason Gross	2017-05-28
\| *	Remove reference to [IsIso]	Jason Gross	2017-05-28
\| *	Use notations for [sig], [sigT], [sig2], [sigT2]	Jason Gross	2017-05-28
\| *	Use extended notation for ex, ex2 types	Jason Gross	2017-05-28
\| *	Replace [ex'] with [ex]	Jason Gross	2017-05-28
\| *	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
\| *	Add equality lemmas for sig2 and sigT2	Jason Gross	2017-05-28
\| *	Add lemmas for ex2	Jason Gross	2017-05-28
\| *	Use [rew] notations rather than [eq_rect]	Jason Gross	2017-05-28
\| *	Add an [inversion_sigma] tactic	Jason Gross	2017-05-28
\| *	Add lemmas about equality of sigma types	Jason Gross	2017-05-28
\| *	Use [rew_] instead of [eq_rect_] prefix	Jason Gross	2017-05-28
\| *	Use [rew] notations rather than [eq_rect]	Jason Gross	2017-05-28
\| *	Add more groupoid-like theorems about [eq]	Jason Gross	2017-05-28
\|/
*	Merge PR#201: Transparent abstract	Maxime Dénès	2017-05-11
\|\
* \	Merge PR#605: Report a useful error for dependent induction	Maxime Dénès	2017-05-05
\|\ \