aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-06-13suite changements ZArith en vu de librairie FSetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4149 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13quelques adaptations de Zarith en vu de la nouvelle librarie FSetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4148 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13coqide: about now displays versions/Fix for alt-entermonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4147 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Deplacement d'un lemme sur nat de ZArith vers Arithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4146 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13CoqIDE: undo immediat sur les commandes ne modifiant pas l'etatfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4145 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground update.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4144 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12enieme correction du nommage modulaireletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4143 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12fin de l'affichage des signatures de modules dans les *.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4142 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4141 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le ↵herbelin
traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4140 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du ↵herbelin
traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-11Pb quand une meme classe est definie dans 2 fichiersherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4138 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-11Token '.(' seulement pour v8, sinon conflit avec '.(*'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4137 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4136 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4135 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4134 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Module Bij inutiliseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4133 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Import nat_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4132 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Suppression d'une occurrence superflue d'argument de type dans Notation ↵herbelin
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
2003-06-10Deplacement delimiteur T dans Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4130 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Module Bij inutiliseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4129 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10freshid -> freshherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4127 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4126 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur ↵herbelin
de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4125 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Simplification case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Record; raffinement diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4123 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Raffinement diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4122 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Globalisation des tactiques avant traduction pour capture des noms; ↵herbelin
affinement divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4121 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Distinction mode v7 ou translate; conséquences du déplacement traducteur ↵herbelin
de nom dans Constrextern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4120 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement de code dans command; MAJ DebugOnherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4119 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Mise en place structure pour des 'arguments scope' dirigés par une classeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4118 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Amélioration afficheur de Cases pour les constr_patternherbelin
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
2003-06-10Passage des noms de tactiques à kernel_name pour compatibilité avec les ↵herbelin
foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4116 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4115 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4114 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Factorisation de detype_case pour utilisation par l'afficheur de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4113 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Traducteur + passage des noms de tactiques à kernel_name pour ↵herbelin
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
2003-06-10Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur ↵herbelin
de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4111 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Amélioration afficheur de Cases pour les constr_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4110 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Extension de Locate sur les symboles avec recherche de sous-chaînes; mise ↵herbelin
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
2003-06-10Globalisation de ce qui n'etait pas encore globaliseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4108 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4107 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout fonctions de recherche de sous-chaines (merci a Jacek)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4106 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4105 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-08interaction entre fun/case permut et assert falseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4104 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-08Tables logarithmiques pour les coercions + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-06coqide: compile sans activate reparemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4102 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-06bug CoqIDE avec Goalfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4101 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-06Added new syntax definitionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4100 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 10:57:26 +0000