coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	- Suppression de Rstar/Newman peu utilisables comme biblio (encodage	herbelin	2008-07-17
\| \| \| \| \| \| \| \| \| \|	des inductifs à l'ordre supérieur par exemple) et qui sont de toutes façons accessible en contrib dans Rocq/CoC_History. - MAJ numéro de version dans Tutorial.tex git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau	2008-03-16
\| \| \| \| \| \| \| \| \| \| \| \|	implicits for left, inl or eq, hence some theories had to be changed again. It should make some user contribs compile again too. Also do not import functional extensionality when importing Program.Basics, add a Combinators file for proofs requiring it and a Syntax file for the implicit settings. Move Classes.Relations to Classes.RelationClasses to avoid name clash warnings as advised by Hugo and Pierre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	out. The semantics of the old setoid are faithfully simulated by the new tactic, hence no scripts involving rewrite are modified. However, parametric morphism declarations need to be changed, but there are only a few in the standard library, notably in FSets. The declaration and the introduction of variables in the script need to be tweaked a bit, otherwise the proofs remain unchanged. Some fragile scripts not introducting their variable names explicitely were broken. Requiring Setoid requires Program.Basics which sets stronger implicit arguments on some constants, a few scripts benefit from that. Ring/field have been ported but do not really use the new typeclass architecture as well as they could. Performance should be mostly unchanged, but will certainly improve in the near future. Size of the vo's seems not to have changed at all. It will certainly break some contribs using Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Autres passages de Set Ã Type dans Relations et Wellfounded	herbelin	2007-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur le passage de Set à Type pour l'ordre lexicographique	herbelin	2007-02-07
\| \| \| \| \| \| \| \|	pour garder Relation_Operators.Pow dans Set (puisque le polymorphisme d'univers pour les inductifs ne se propage pas aux définitions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9609 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9598 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
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵	notin	2006-04-28
\| \| \| \| \| \|	'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification des propriétés (svn:executable)	notin	2006-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement parametres inductifs dans les theories	mohring	2005-11-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7630 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Généralisation à Type de certaines propriétés des relations	herbelin	2004-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6331 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
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 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
*	Cacher les .v8	herbelin	2003-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de Induction/Destruct par NewInduction/NewDestruct	herbelin	2003-09-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de 'relation' à Type	herbelin	2003-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4288 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nommage explicite des hypotheses introduites quand le nom existe aussi comme ↵	herbelin	2003-04-07
\| \| \| \| \| \|	global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3861 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression d'axiomes dans Rstar, Newman et Integers	letouzey	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2187 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Library doc adjustments (until page 140)	coq	2001-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remplace Zarith par ZArith	mohring	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement PolyListSyntax est necessaire (la redondance venait d'une ↵	herbelin	2000-11-10
\| \| \| \| \| \|	confusion dans les methodes open/load) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@840 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring	2000-11-07
\| \| \| \| \| \| \| \| \| \|	de fonctions dans les .vo ajout de lemmes dans EqNat, Logic_Type suppression de PolyListSyntax qui redefinissait le Infix de append Recherche d'instances a reecrire dans les Cases et les FixPoint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retire les parentheses autour des tactiques	mohring	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@766 85f007b7-540e-0410-9357-904b9bb8a0f7
*	theories/Relations	filliatr	2000-06-21
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7