coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik	2017-06-01
*	Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.	Hugo Herbelin	2017-03-03
*	Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.	Hugo Herbelin	2017-03-03
*	Completing "few lemmas about Zneg" with lemmas also about Zpos.	Hugo Herbelin	2017-03-03
*	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\
\| *	Int.v: simplify Jason's commit 5b4e3ace	Pierre Letouzey	2016-05-04
\| *	Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...	Pierre Letouzey	2016-05-04
\| \|\
* \| \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\|/ /
* \|	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Move compatibility notations to their proper files	Jason Gross	2015-12-29
\|/
*	Fix some typos.	Guillaume Melquiond	2015-12-07
*	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
*	ZArith/Int.v: some modernizations	Pierre Letouzey	2015-04-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...	Hugo Herbelin	2014-10-17
*	Essai où assert_style n'est utilisé que si pas visuellement une équation;	Hugo Herbelin	2014-10-17
*	eta contractions	Pierre Boutillier	2014-10-01
*	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier	2014-10-01
*	Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to	Hugo Herbelin	2014-08-18
*	Testing a replacement of "cut" by "enough" on a couple of test files.	Hugo Herbelin	2014-08-05
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Pos.iter arguments in a better order for cbn.	Pierre Boutillier	2014-05-02
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-02
*	Restore Zsqrt compat now that refine works fine with match.	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	More dynamic argument scopes	letouzey	2013-07-17
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill	2012-12-21
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Updating headers.	herbelin	2012-08-08
*	BinPos/BinInt/BinNat : fix some argument scopes	letouzey	2012-07-06
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	BinInt: a forgotten scope for a notation	letouzey	2012-06-19
*	Functions *_beq aren't generated anymore, remove comments about them	letouzey	2012-05-30
*	Fixing typo in previous commit r15180.	herbelin	2012-04-15
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	Deleted the only use of BeginSubProof from the standard library.	ppedrot	2012-01-23
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin	2011-10-01
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11