aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-06-19typofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4179 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-18*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4178 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-18AVL: suitefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4177 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-18Arguments superflus pour Zlength_nilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4176 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-17Ajout option Local aux Hintherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4175 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-17AVL: suitefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4174 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-17AVL de caml: un debutfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4173 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4172 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4171 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16Ground depthfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4170 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4169 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16reparation fsets suite a changement de Groundfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4168 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-15Ground major update ... mmm, sounds exciting !corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4167 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4166 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14dependcoq integre les fichiers de fsetsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4165 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Major Ground update, may break semanticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4164 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Deplacement de le_minus de fast_integer vers Minusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4162 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Deplacement de le_minus de fast_integer vers Minusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4160 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13changement de spécif du foldletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4159 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4158 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13CoqIDE: undo plus efficace sur les inductifsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4157 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground update, new files.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4156 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13coqide: indentationmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4155 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13fcts tail-recursivesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4153 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Require Exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4152 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13install-fsetsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4151 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13FSets, mais pas compile' par make worldfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
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