aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Ground Update.Gravatar corbinea2003-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4187 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Symmetry in Hyp'Gravatar herbelin2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Symmetry in Hyp'Gravatar herbelin2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'Gravatar herbelin2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4184 85f007b7-540e-0410-9357-904b9bb8a0f7
* addGravatar filliatr2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4183 85f007b7-540e-0410-9357-904b9bb8a0f7
* bal: preuve termineeGravatar filliatr2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4182 85f007b7-540e-0410-9357-904b9bb8a0f7
* bal: premier cas hl > hr + 2Gravatar filliatr2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4181 85f007b7-540e-0410-9357-904b9bb8a0f7
* undo de "Time tactic"Gravatar filliatr2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4180 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar filliatr2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4179 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar monate2003-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4178 85f007b7-540e-0410-9357-904b9bb8a0f7
* AVL: suiteGravatar filliatr2003-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments superflus pour Zlength_nilGravatar herbelin2003-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option Local aux HintGravatar herbelin2003-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4175 85f007b7-540e-0410-9357-904b9bb8a0f7
* AVL: suiteGravatar filliatr2003-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4174 85f007b7-540e-0410-9357-904b9bb8a0f7
* AVL de caml: un debutGravatar filliatr2003-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4173 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4172 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground updateGravatar corbinea2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4171 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground depthGravatar filliatr2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4170 85f007b7-540e-0410-9357-904b9bb8a0f7
* ground updateGravatar corbinea2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4169 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation fsets suite a changement de GroundGravatar filliatr2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground major update ... mmm, sounds exciting !Gravatar corbinea2003-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4167 85f007b7-540e-0410-9357-904b9bb8a0f7
* ground updateGravatar corbinea2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4166 85f007b7-540e-0410-9357-904b9bb8a0f7
* dependcoq integre les fichiers de fsetsGravatar letouzey2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major Ground update, may break semanticsGravatar corbinea2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de le_minus de fast_integer vers MinusGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de le_minus de fast_integer vers MinusGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4161 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4160 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement de spécif du foldGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground updateGravatar corbinea2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4158 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: undo plus efficace sur les inductifsGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4157 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update, new files.Gravatar corbinea2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4156 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: indentationGravatar monate2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
* fcts tail-recursivesGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Require ExportGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4152 85f007b7-540e-0410-9357-904b9bb8a0f7
* install-fsetsGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4151 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSets, mais pas compile' par make worldGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite changements ZArith en vu de librairie FSetGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4149 85f007b7-540e-0410-9357-904b9bb8a0f7
* quelques adaptations de Zarith en vu de la nouvelle librarie FSetGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4148 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: about now displays versions/Fix for alt-enterGravatar monate2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4147 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement d'un lemme sur nat de ZArith vers ArithGravatar herbelin2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4146 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: undo immediat sur les commandes ne modifiant pas l'etatGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update.Gravatar corbinea2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4144 85f007b7-540e-0410-9357-904b9bb8a0f7
* enieme correction du nommage modulaireGravatar letouzey2003-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4143 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin de l'affichage des signatures de modules dans les *.mlGravatar letouzey2003-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4142 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-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 ↵Gravatar herbelin2003-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 ↵Gravatar herbelin2003-06-12
| | | | | | traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7