coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	power associe a droite	marche	2003-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ratage standardisation Rge_monotony en Rmult_ge_compat_r	herbelin	2003-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5047 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
*	Notation locale pour Rpower	herbelin	2003-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5025 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout lemmes, simplification preuve de SeqProp	herbelin	2003-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5024 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation du total_order non constructif	herbelin	2003-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre les renommages; redondances	herbelin	2003-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5016 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration compatibilite 7.4 pour le Hint Unfold Rgt	herbelin	2003-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4951 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Meilleure solution pour la compatibilite	herbelin	2003-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ INZ	herbelin	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4886 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration preference Rge a Rle pour compatibilite...	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration preference Rge a Rle pour compatibilite...; petit nettoyage	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵	herbelin	2003-10-30
\| \| \| \| \| \|	associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 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
*	R passe dans Set !	herbelin	2003-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	20 est uniquement associatif a gauche	herbelin	2003-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4672 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lettac -> set	barras	2003-10-16
\| \| \| \| \| \| \|	suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour eviter des regles redondantes en v7	herbelin	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4647 85f007b7-540e-0410-9357-904b9bb8a0f7
*	FTC_P2 maintenant dans RIneq	herbelin	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de quelques lemmes cles	herbelin	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4645 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage = au lieu de == en v7	herbelin	2003-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notations pour l'exponentiation	herbelin	2003-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notation '^'	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4586 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
*	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵	herbelin	2003-09-23
\| \| \| \| \| \|	TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵	herbelin	2003-09-21
\| \| \| \| \| \|	aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4427 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le ↵	herbelin	2003-09-19
\| \| \| \| \| \|	traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4420 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵	herbelin	2003-09-19
\| \| \| \| \| \|	meme si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4417 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
*	Bind et Delimit pour R	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4373 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bind et Delimit pour R	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4367 85f007b7-540e-0410-9357-904b9bb8a0f7
*	INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le ↵	herbelin	2003-06-12
\| \| \| \| \| \|	traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4140 85f007b7-540e-0410-9357-904b9bb8a0f7
*	niveau 49 devient next	herbelin	2003-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals	herbelin	2003-05-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4074 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug	herbelin	2003-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4046 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration presentation	herbelin	2003-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration affichage	herbelin	2003-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de 'R' dans la notation == entre	herbelin	2003-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4016 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de 'R' dans la notation == entre	herbelin	2003-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4015 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement lemmes sur fact de Reals vers Arith	herbelin	2003-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ↵	herbelin	2003-04-29
\| \| \| \| \| \|	Rlt_sym, Rle_sym; utilisation de la terminologie 'commutative' plutôt que 'symétrie' pour les opérateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Divers	herbelin	2003-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3943 85f007b7-540e-0410-9357-904b9bb8a0f7
*	<> maintenant standard	herbelin	2003-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3942 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom different	letouzey	2003-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sumboolT, sumorT, sigTT, SigT redondants	herbelin	2003-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3927 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Local 'o'	herbelin	2003-04-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3918 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@3881 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