coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	MAJ	herbelin	2003-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4141 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
*	Ajout option translate_syntax pour caractériser l'interprétation du ↵	herbelin	2003-06-12
\| \| \| \| \| \|	traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pb quand une meme classe est definie dans 2 fichiers	herbelin	2003-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4138 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Token '.(' seulement pour v8, sinon conflit avec '.(*'	herbelin	2003-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4137 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4136 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4135 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4134 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Module Bij inutilise	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Import nat_scope	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4132 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression d'une occurrence superflue d'argument de type dans Notation ↵	herbelin	2003-06-10
\| \| \| \| \| \|	sachant que les 2 occurrences ne sont pas forcement dans le meme scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4131 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement delimiteur T dans Notations	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4130 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Module Bij inutilise	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
*	freshid -> fresh	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4127 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur ↵	herbelin	2003-06-10
\| \| \| \| \| \|	de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4125 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification case_info	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout notation c.(f) en v8 pour les projections de Record; raffinement divers	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4123 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Raffinement divers	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4122 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des tactiques avant traduction pour capture des noms; ↵	herbelin	2003-06-10
\| \| \| \| \| \|	affinement divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4121 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Distinction mode v7 ou translate; conséquences du déplacement traducteur ↵	herbelin	2003-06-10
\| \| \| \| \| \|	de nom dans Constrextern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4120 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de code dans command; MAJ DebugOn	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4119 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place structure pour des 'arguments scope' dirigés par une classe	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4118 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration afficheur de Cases pour les constr_pattern	herbelin	2003-06-10
\| \| \| \| \| \| \| \| \|	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs Extension du traducteur de nom Ajout notation c.(f) en v8 pour les projections de Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4117 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage des noms de tactiques à kernel_name pour compatibilité avec les ↵	herbelin	2003-06-10
\| \| \| \| \| \|	foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4116 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4115 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Factorisation de detype_case pour utilisation par l'afficheur de pattern	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traducteur + passage des noms de tactiques à kernel_name pour ↵	herbelin	2003-06-10
\| \| \| \| \| \|	compatibilité avec les foncteurs + réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur ↵	herbelin	2003-06-10
\| \| \| \| \| \|	de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4111 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration afficheur de Cases pour les constr_pattern	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4110 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Locate sur les symboles avec recherche de sous-chaînes; mise ↵	herbelin	2003-06-10
\| \| \| \| \| \|	en place structure pour des 'arguments scope' dirigés par une classe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation de ce qui n'etait pas encore globalise	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4108 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4107 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout fonctions de recherche de sous-chaines (merci a Jacek)	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-06-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4105 85f007b7-540e-0410-9357-904b9bb8a0f7
*	interaction entre fun/case permut et assert false	letouzey	2003-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4104 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tables logarithmiques pour les coercions + nettoyage	herbelin	2003-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: compile sans activate repare	monate	2003-06-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4102 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug CoqIDE avec Goal	filliatr	2003-06-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4101 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added new syntax definition	barras	2003-06-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4100 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugfix for Ground ( merci JC )	corbinea	2003-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4097 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ground update + some bugfix	corbinea	2003-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4096 85f007b7-540e-0410-9357-904b9bb8a0f7
*	au lieu de make	monate	2003-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4095 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oups	letouzey	2003-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4094 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug niveau	herbelin	2003-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4092 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
*	Ground daily update	corbinea	2003-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4090 85f007b7-540e-0410-9357-904b9bb8a0f7