coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove fourier plugin	Maxime Dénès	2018-07-17
\| \| \| \|	As stated in the manual, the fourier tactic is subsumed by lra.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Simplify some proofs using ring and field.	Guillaume Melquiond	2017-03-22
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
\| \| \| \| \| \| \|	Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	finish the rearrangement for removing the sin_PI2 axiom. This new version	bertot	2012-06-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- provides the atan function - shows that this function is equal between -1 and 1 to a function defined with power series - establishes the equality with the PI value as given by the alternated series constructed with PI_tg - provides a smarter theorem to compute approximations of PI, based on a formula in the same family as the one used by John Machin in 1706 Dependencies between files have been rearranged so that the new theorems are loaded with the library Reals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15429 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix scripts relying on unification not doing any beta reduction.	msozeau	2011-04-13
\| \| \| \| \| \|	They are actually simpler, sometimes using the [rewrite at] variant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13992 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en forme des theories	notin	2006-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵	herbelin	2003-11-29
\| \| \| \| \| \|	par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout et MAJ commandes de scopes	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4375 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Open Scope en Local	herbelin	2003-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3917 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement Import par Open Scope en v8	herbelin	2003-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques améliorations	desmettr	2003-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3556 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de INR2 / Conséquence logique de la nouvelle représentation ↵	desmettr	2003-01-21
\| \| \| \| \| \|	des constantes entières git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3555 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cgt définition de plat	desmettr	2003-01-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage de RealsB en Rbase	desmettr	2003-01-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle interprétation des nombres réels	desmettr	2003-01-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation de la librairie des réels	desmettr	2002-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2884 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	desmettr	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2883 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proprietes (calculatoires) des fonctions trigonometriques	desmettr	2002-07-16
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2875 85f007b7-540e-0410-9357-904b9bb8a0f7