coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix typo in documentation for identity	Tej Chajed	2017-07-05
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge PR#826: Put plugin exports in the right compatibility file	Maxime Dénès	2017-06-26
\|\
* \	Merge PR#794: Cleanup of ltac cmxs	Maxime Dénès	2017-06-23
\|\ \
\| \| *	Put plugin exports in the right compatibility file	Jason Gross	2017-06-22
\| \|/ \|/\|
\| *	plugins/ltac : avoid spurious .cmxs files	Pierre Letouzey	2017-06-15
* \|	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\ \ \| \|/ \|/\|
* \|	Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).	Maxime Dénès	2017-06-14
\|\ \
* \| \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| \| *	Remove deprecated options from the standard library.	Guillaume Melquiond	2017-06-14
\| \| *	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
\| \|/ \|/\|
* \|	Merge PR#498: Bignums as a separate opam package	Maxime Dénès	2017-06-14
\|\ \
* \ \	Merge PR#385: Equality of sigma types	Maxime Dénès	2017-06-13
\|\ \ \
\| \| * \|	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey	2017-06-13
\| \|/ / \|/\| \|
* \| \|	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\| \| *	Fix bug 5026 (the stdlib shouldn't define inconsistent notations).	Théo Zimmermann	2017-06-08
\| \|/ \|/\|
* \|	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
\|/
*	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