aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-06-24concat; debut splitfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4203 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23Ajout systématique de Proof dans la traductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4202 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23Formattage Apply withherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4201 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23Formattage pattern 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4200 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23joinfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4199 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23add_tree : sur type tree plutot que sur type tfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4198 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23merge_bis et debug joinfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4197 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-22Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4196 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-21Added a test for Functional Induction.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4195 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4194 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4193 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20Bug compilationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4192 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20removfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4191 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20mergefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4190 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20remove_min, remove_maxfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4189 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20Ground Update.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4187 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19Ajout 'Symmetry in Hyp'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4186 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19Ajout 'Symmetry in Hyp'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4184 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19addfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4183 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19bal: preuve termineefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4182 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19bal: premier cas hl > hr + 2filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4181 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19undo de "Time tactic"filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4180 85f007b7-540e-0410-9357-904b9bb8a0f7
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