coq - The formal proof system

Age	Commit message (Expand)	Author
2021-04-02	add Cantor pairing to_nat and its inverse of_nat	Andrej Dudenhefner
2020-11-16	Explicitly annotate all hint declarations of the standard library.	Pierre-Marie Pédrot
2020-10-11	Modify Arith/Euclid.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Arith/Div2.v to compile with -mangle-names	Jasper Hugunin
2020-10-11	Modify Arith/Even.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Wf_nat.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/EqNat.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Factorial.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Compare_dec.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Peano_dec.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Between.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Mult.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Plus.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/Le.v to compile with -mangle-names	Jasper Hugunin
2020-09-16	Modify Arith/PeanoNat.v to compile with -mangle-names	Jasper Hugunin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-06	Fix #11738 : Funind using deprecated Coqlib API.	Pierre Courtieu
2019-12-24	Add statements with output in Type	Olivier Laurent
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-25	Modifying theories to preferably use the "[= ]" syntax, and,	Hugo Herbelin
2019-04-08	Fix spelling in comment.	nlewycky
2019-04-02	Remove -compat 8.7	Jason Gross
2018-10-10	[coqlib] Rebindable Coqlib namespace.	Emilio Jesus Gallego Arias
2018-10-02	Update compat notations to be compat 8.7	Jason Gross
2018-04-13	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias
2018-03-05	Merge PR #6855: Update headers following #6543.	Maxime Dénès
2018-03-02	Remove the deprecation for some 8.2-8.5 compatibility aliases.	Théo Zimmermann
2018-02-27	Update headers following #6543.	Théo Zimmermann
2018-02-24	Merge PR #6599: Decimals in prelude	Maxime Dénès
2018-02-21	Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred	Maxime Dénès
2018-02-20	Decimal: proofs that conversions from/to nat,N,Z are bijections	Pierre Letouzey
2018-01-08	Document between and exists_between types.	Ismail
2017-12-01	proposed fix for issue #3213: extra variable m in Lt.S_pred	fredokun
2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-01	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik
2017-01-30	Proof clean-up.	Théo Zimmermann
2016-10-24	Remove v62 from stdlib.	Théo Zimmermann
2016-06-18	Giving a more natural semantics to injection by default.	Hugo Herbelin
2016-01-20	Update copyright headers.	Maxime Dénès
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-10-01	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier
2014-07-22	Fixed proof of irrelevance of le on nat, inspired by the	Maxime Dénès
2014-07-09	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey
2014-06-01	Making those proofs which depend on names generated for the arguments	Hugo Herbelin
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-12-21	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill
2012-10-04	Revert "En cours pour 'generalize in clause' et 'induction in clause'"	herbelin