coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suppress warning message in stdlib.	Guillaume Melquiond	2017-04-29
*	Merge PR#414: Some more theory on powerRZ.	Maxime Dénès	2017-04-27
\|\
* \|	Add some hints to the "real" database to automatically discharge literal comp...	Guillaume Melquiond	2017-04-07
* \|	Fix documentation typo (bug #5433).	Guillaume Melquiond	2017-04-02
* \|	Simplify some proofs.	Guillaume Melquiond	2017-04-02
* \|	Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.	Guillaume Melquiond	2017-03-30
* \|	Make IZR a morphism for field.	Guillaume Melquiond	2017-03-22
* \|	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
* \|	Make IZR use a compact representation of integers.	Guillaume Melquiond	2017-03-22
* \|	Simplify some proofs using ring and field.	Guillaume Melquiond	2017-03-22
\| *	Added some theory on powerRZ.	Thomas Sibut-Pinote	2017-02-15
\|/
*	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
*	Fix an occurrence of deprecated eqn syntax in stdlib.	Maxime Dénès	2016-08-18
*	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin	2016-04-27
*	Temporary hack to compensate missing comma while re-printing tactic	Hugo Herbelin	2016-04-27
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
*	Accomodating #4166 (providing "Require Import OmegaTactic" as a	Hugo Herbelin	2015-04-01
*	Add some missing Proof keywords.	Guillaume Melquiond	2015-03-06
*	Update headers.	Maxime Dénès	2015-01-12
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	adds general facts in the Reals library, whose need was detected in	Yves Bertot	2014-09-23
*	Change some Defined into Qed.	Guillaume Melquiond	2014-09-17
*	Add some missing Proof statements.	Guillaume Melquiond	2014-09-17
*	Change an axiom into a definition.	Guillaume Melquiond	2014-09-17
*	More proofs independent of the names generated by induction/elim over	Hugo Herbelin	2014-08-05
*	Deactivate the "Standard Propositions Naming" flag, source of a lot of	Hugo Herbelin	2014-06-26
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Remove spurious Show in script.	Matthieu Sozeau	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
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Import proof of decidability of negated formulas from Coquelicot.	Guillaume Melquiond	2014-04-23
*	Remove some uses of excluded middle.	Guillaume Melquiond	2014-04-22
*	Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...	Guillaume Melquiond	2014-04-22
*	Fixing missing headers.	Hugo Herbelin	2014-04-16
*	No more Coersion in Init.	Pierre Boutillier	2014-04-10
*	Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.	Guillaume Melquiond	2014-03-10
*	Add lemma derivable_pt_lim_atan.	Guillaume Melquiond	2013-12-04
*	Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.	Guillaume Melquiond	2013-12-03
*	Remove a useless hypothesis from Rle_Rinv.	Guillaume Melquiond	2013-12-03
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Removing redundant definition of case_eq (see #2919).	herbelin	2012-10-16
*	Updating headers.	herbelin	2012-08-08
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05