coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	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
\|/
*	Stop using auto with * in two proofs.	Théo Zimmermann	2017-05-16
*	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
\|\ \ \
* \ \ \	Merge PR#588: Allow interactive editing of {C,}Morphisms in PG	Maxime Dénès	2017-05-03
\|\ \ \ \
* \ \ \ \	Merge PR#386: Better editing of the standard library in coqtop/PG	Maxime Dénès	2017-05-03
\|\ \ \ \ \
\| \| \| \| * \|	Report a useful error for dependent induction	Tej Chajed	2017-05-03
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| * \|	Reorganize comment documentation of ChoiceFacts.v	Gaetan Gilbert	2017-05-03
\| \| \| * \|	Functional choice <-> [inhabited] and [forall] commute	Gaetan Gilbert	2017-04-30
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Suppress warning message in stdlib.	Guillaume Melquiond	2017-04-29
\| \| * \|	Allow interactive editing of {C,}Morphisms in PG	Jason Gross	2017-04-28
\| \|/ / \|/\| \|
\| * \|	Add .dir-locals.el and _CoqProject files for emacs stdlib editing	Jason Gross	2017-04-28
\|/ /
* \|	Merge PR#414: Some more theory on powerRZ.	Maxime Dénès	2017-04-27
\|\ \
* \ \	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 PR#545: Add some hints to the "real" database to automatically discharg...	Maxime Dénès	2017-04-19
\|\ \
* \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\ \ \
\| \| * \|	Add some hints to the "real" database to automatically discharge literal comp...	Guillaume Melquiond	2017-04-07
\| \|/ / \|/\| \|
* \| \|	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
\| \| \|\ \
* \| \| \| \|	Fix documentation typo (bug #5433).	Guillaume Melquiond	2017-04-02
* \| \| \| \|	Simplify some proofs.	Guillaume Melquiond	2017-04-02
* \| \| \| \|	Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.	Guillaume Melquiond	2017-03-30
* \| \| \| \|	Merge PR#469: Added take to VectorDef	Maxime Dénès	2017-03-30
\|\ \ \ \ \
\| * \| \| \| \|	Added take to VectorDef.	George Stelle	2017-03-30
* \| \| \| \| \|	Fixing missing PropFacts.v in Logic/vo.itarget.	Hugo Herbelin	2017-03-28
* \| \| \| \| \|	Merge PR#392: strengthened the statement of JMeq_eq_dep	Maxime Dénès	2017-03-24
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\ \ \ \ \ \ \ \| \| \|_\|_\|/ / / \| \|/\| \| \| \| \|
* \| \| \| \| \| \|	Make IZR a morphism for field.	Guillaume Melquiond	2017-03-22
* \| \| \| \| \| \|	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
* \| \| \| \| \| \|	Make IZR use a compact representation of integers.	Guillaume Melquiond	2017-03-22