coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \
\| \| *	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\| \| \|\
* \| \| \	Merge PR#442: Allow interactive editing of Coq.Init.Logic	Maxime Dénès	2017-03-17
\|\ \ \ \
* \ \ \ \	Merge PR#451: Add η principles for sigma types	Maxime Dénès	2017-03-17
\|\ \ \ \ \
\| \| \| * \| \|	Farewell decl_mode	Enrico Tassi	2017-03-07
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	A couple of other useful properties about compare_cont.	Hugo Herbelin	2017-03-03
* \| \| \| \|	Compatibility of iff wrt not and imp.	Hugo Herbelin	2017-03-03
\| * \| \| \|	Add η principles for sigma types	Jason Gross	2017-03-01
\| * \| \| \|	Remove some trailing whitespace in Init/Specif.v	Jason Gross	2017-03-01
\|/ / / /
\| \| \| *	Fixing a little bug in printing ex2 (type was printed "_" by default).	Hugo Herbelin	2017-02-23
\| * \| \|	Allow interactive editing of Coq.Init.Logic	Jason Gross	2017-02-21
\|/ / /
* / /	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
\|/ /
* \|	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24