coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Finalement, préservation de la compatibilité pour Z_lt_induction et ajout ↵	herbelin	2005-05-02
\| \| \| \| \| \|	plutôt de nouveaux énoncés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6984 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Lemme de passage de l'autre côté d'une égalité	herbelin	2005-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6983 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed hypotheses of Z_lt_induction (see #957)	herbelin	2005-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Missing translating a 'O' into a '0' (again - cf bug #947); removed useless ↵	herbelin	2005-03-29
\| \| \| \| \| \|	hypothesis of Zlt/Zgt_square_simpl (cg #948) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6898 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Missing translating a 'O' into a '0'	herbelin	2005-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6884 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement dans les boxed values .	gregoire	2004-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵	herbelin	2004-10-11
\| \| \| \| \| \|	evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zbool déjà dans ZArith_base	herbelin	2004-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6013 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
*	backtrack implicit dans Bvector	marche	2004-02-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	patch Bvector: args implicites	marche	2004-02-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5309 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
\| \| \| \| \| \| \| \|	documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 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
*	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace ↵	herbelin	2003-12-04
\| \| \| \| \| \|	par un niveau ajoute dynamiquement; plus de limite vers le haut: divide au niveau 260 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5069 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
*	ground->firstorder, cc-> congruence, CC final commit	corbinea	2003-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report de lemmes de Znumtheory dans Zabs ou BinInt	herbelin	2003-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5018 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renoncement de la compatibilite des noms qualifies au profit de la ↵	herbelin	2003-11-24
\| \| \| \| \| \|	compatibilite des arguments implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4979 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compatibilite	herbelin	2003-11-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification; ajout Zcompare_antisym	herbelin	2003-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4965 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout Pnat (suite)	herbelin	2003-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4964 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de Znumtheory.v dans ZArith	letouzey	2003-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un nouveau lemme redondant ...	herbelin	2003-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement ZERO_le_inj dans Zorder	herbelin	2003-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base	herbelin	2003-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4914 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cosmetique	herbelin	2003-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4912 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques oublis pour que les notations marchent bien	herbelin	2003-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4907 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug implicit arguments	herbelin	2003-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4905 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli report Nul/Pos	herbelin	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4895 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Require	herbelin	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	qq petit ajouts à Zdiv	letouzey	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration ZArith	herbelin	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout lemmes; independance vis a vis noms variables liees; restructuration	herbelin	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4873 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout partie sur bool anciennement dans Zmisc	herbelin	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4872 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout lemmes; independance vis a vis noms variables liees	herbelin	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout quelques lemmes; noms des variables liees	herbelin	2003-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4845 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli BinNat	herbelin	2003-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli d'un Set Implicit Arguments	herbelin	2003-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Des oublis	herbelin	2003-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report des definitions sorties de fast_integer pour compatibilite	herbelin	2003-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4818 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, ↵	herbelin	2003-11-05
\| \| \| \| \| \|	de la partie Omega dans contrib/omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Exporting ^; utilisation arg scope implicite	herbelin	2003-11-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵	herbelin	2003-11-01
\| \| \| \| \| \|	entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour en arriere sur d'autres renommages de variables	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4721 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour a un nommage non standard des variables pour compatibilite; report ↵	herbelin	2003-10-27
\| \| \| \| \| \|	'relation' pour compatibilite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4720 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation/Structuration	herbelin	2003-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4702 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
\| \| \| \| \| \| \|	Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Redondance de dec_eq_nat	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Type relation dans Datatypes	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4691 85f007b7-540e-0410-9357-904b9bb8a0f7