coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #882: Adding a V8.7 compatibility version number.	Maxime Dénès	2017-07-26
\|\
* \	Merge PR #885: Removing a dummy parameter in some FMapPositive statements.	Maxime Dénès	2017-07-26
\|\ \
* \ \	Merge PR #845: Add Z.mod_div lemma to standard library.	Maxime Dénès	2017-07-26
\|\ \ \
\| \| \| *	Adding a V8.7 compatibility version number.	Hugo Herbelin	2017-07-21
\| \|_\|/ \|/\| \|
\| \| *	Removing a dummy parameter in some FMapPositive statements.	Hugo Herbelin	2017-07-16
* \| \|	Fix typo in documentation for identity	Tej Chajed	2017-07-05
\| \|/ \|/\|
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Fix Zmod_div.	Russell O'Connor	2017-06-29
\| *	Use forall for consistency	roconnor-blockstream	2017-06-29
\| *	Add Z.mod_div lemma to standard library.	Russell O'Connor	2017-06-29
\|/
*	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
\|\