coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-16	Merge PR #13384: Warn on hints without an explicit locality	coqbot-app[bot]
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-11-15	Default disable automatic generalization of Instance type	Gaëtan Gilbert
2020-08-25	Modify Classes/Morphisms.v to compile with -mangle-names	Jasper Hugunin
2020-03-19	[stdlib] Remove a few `auto with *`	Vincent Laporte
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-01-23	Pass some files to strict focusing mode.	Gaëtan Gilbert
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-04-28	Allow interactive editing of {C,}Morphisms in PG	Jason Gross
2016-06-28	Typeclasses: use once in by clause for typeclass eauto	Matthieu Sozeau
2016-06-16	setoid_rewrite: fix the Params resolution tactic	Matthieu Sozeau
2016-03-04	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-06-29	Move Params definition in generalize rewriting out of a section so that	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2012-08-08	Updating headers.	herbelin
2012-07-05	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey
2012-03-19	Fix bugs related to Program integration.	msozeau
2012-03-14	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau
2012-01-31	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau
2012-01-28	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-11-17	Merge subinstances branch by me and Tom Prince.	msozeau
2011-10-10	Proper fix for complement/flip instances.	msozeau
2011-10-07	Fix bug #2557 and an issue with Propers for complement	msozeau
2011-09-06	Avoid registering λ and Π as keywords just for some private Local Notation	letouzey
2011-05-05	Merge branch 'subclasses' into coq-trunk	msozeau
2011-02-28	- Allow rewriting under abitrary products, not just those in Prop.	msozeau
2011-01-04	f_equiv : a clone of f_equal that handles setoid equivalences	letouzey
2011-01-03	Numbers: some improvements in proofs	letouzey
2010-07-31	Fixed commit r13359 which was incomplete for its "trunk" part. Thanks	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-08	Made option "Automatic Introduction" active by default before too many	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-01-30	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau
2010-01-26	Support for generalized rewriting under dependent binders, using the	msozeau
2010-01-11	Support "Local Obligation Tactic" (now the default in sections).	msozeau
2009-12-03	Rename proper to proper_prf to avoid clash with CoRN,	msozeau
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-15	Document Generalizable Variables, and change syntax to	msozeau
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-22	Fix new instances that could easily make class resolution loop on	msozeau
2009-10-13	MSets: a new generation of FSets	letouzey
2009-10-08	Implicit argument of Logic.eq become maximally inserted	letouzey
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu