coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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 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
\|\ \
* \ \	Merge PR#593: Functional choice <-> [inhabited] and [forall] commute	Maxime Dénès	2017-05-05
\|\ \ \
\| \| * \|	Report a useful error for dependent induction	Tej Chajed	2017-05-03
\| * \| \|	Functional choice <-> [inhabited] and [forall] commute	Gaetan Gilbert	2017-04-30
\| \|/ /
* / /	Add .dir-locals.el and _CoqProject files for emacs stdlib editing	Jason Gross	2017-04-28
\|/ /
* \|	Merge PR#584: Give andb_prop a simpler proof	Maxime Dénès	2017-04-27
\|\ \
* \| \|	Small typo in comment	Vadim Zaliva	2017-04-26
\| \| *	Add transparent_abstract tactic	Jason Gross	2017-04-25
\| \|/ \|/\|
\| *	Give andb_prop a simpler proof	Jason Gross	2017-04-25
\|/
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
* \	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\ \