coq - The formal proof system

Age	Commit message (Expand)	Author
2020-12-15	Modify QArith/QArith_base.v to compile with -mangle-names	Jasper Hugunin
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-11-05	Rename Dec and HexDec to Decimal and Hexadecimal	Pierre Roux
2020-11-05	[numeral notation] Q	Pierre Roux
2020-10-30	Renaming Numeral.v into Number.v	Pierre Roux
2020-09-11	Rename Numeral Notation command to Number Notation	Pierre Roux
2020-05-09	Add hexadecimal numerals	Pierre Roux
2020-04-01	[micromega] use Coqlib.lib_ref to get Coq constants.	Frédéric Besson
2020-03-25	Nicer printing for decimal constants in Q	Pierre Roux
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-10-31	QArith: only depend on ZArith_base	Vincent Laporte
2019-10-22	QArith_base: do not use “omega”	Vincent Laporte
2019-08-09	Switch constructive Rlt to sort Type, to make it compute later	Vincent Semeria
2019-08-08	Add interface of constructive real numbers, with an opaque implementation by ...	Vincent Semeria
2019-08-06	Prove the completeness of real numbers from logical axiom sig_not_dec	Vincent Semeria
2019-07-16	Define constructive real numbers as Cauchy sequences of rational numbers. Red...	Vincent Semeria
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-04-02	Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)	Pierre Roux
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
2018-03-09	Merge PR #6155: Get rid of ' notation for Zpos in QArith	Maxime Dénès
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-11-14	Get rid of ' notation for Zpos in QArith.	Robbert Krebbers
2017-10-27	Chaining two tactics in a proof	Raphaël Monat
2017-10-25	Moving from `is_true` to `= true`	Raphaël Monat
2017-10-12	Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans.	Raphaël Monat
2017-10-08	Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.	Raphaël Monat
2017-10-03	Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.	Raphaël Monat
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-05-02	Eta contractions to please cbn	Pierre Boutillier
2012-08-08	Updating headers.	herbelin
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-03-17	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey
2010-11-02	Add small utility lemmas about nat/P/Z/Q arithmetic.	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-29	QArith: typo in name of hint db (fix #2346)	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-11-03	Better visibility of the inductive CompSpec used to specify comparison functions	letouzey
2009-11-03	OrderedType implementation for various numerical datatypes + min/max structures	letouzey
2009-10-08	Implicit argument of Logic.eq become maximally inserted	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-05	changed deprecated setoid into relation	amahboub
2008-07-27	Oups (on refait le 11268 en mieux)	herbelin
2008-07-26	- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec	herbelin
2008-07-15	Autour du parsing:	herbelin
2008-07-04	Fix bug #1899: no more strange notations for Qge and Qgt	letouzey
2008-04-08	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau
2008-03-16	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau