aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-05-27'only parsing' pour le passage de trucT a trucherbelin
2003-05-27majfilliatr
2003-05-26coqide: blaster interruptiblemonate
2003-05-26Bugherbelin
2003-05-26GIntuition now matches Intuition up to hyps renaming.corbinea
2003-05-26Added breakpoint in Ground tactic.corbinea
2003-05-26moved engine.ml4 to ground.ml4, added option 'Ground Depth'corbinea
2003-05-26*** empty log message ***monate
2003-05-26configure pour CoqIde reparemonate
2003-05-25Ground and CCsolve updatescorbinea
2003-05-24"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Realsherbelin
2003-05-24Amélioration affichage locations; prise en compte variables dans lettac; ajo...herbelin
2003-05-24Ajout FreshIdherbelin
2003-05-23coqide: blaster 2monate
2003-05-23fabrication de ide/utf8.voletouzey
2003-05-23Bug en mode translateherbelin
2003-05-23majfilliatr
2003-05-23coqide: blaster 2monate
2003-05-23majfilliatr
2003-05-22V8Notationherbelin
2003-05-22Ajout V8Notationherbelin
2003-05-22Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...herbelin
2003-05-22Test backtrackingherbelin
2003-05-22Ajout V8Notationherbelin
2003-05-22Preservation affichage des ?n en V7herbelin
2003-05-22coqide: blaster V1monate
2003-05-22Ocaml 3.00 a existe'herbelin
2003-05-22compat windowsfilliatr
2003-05-22majfilliatr
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...herbelin
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2003-05-21Nouveaux testsherbelin
2003-05-21MAJherbelin
2003-05-21Notationsherbelin
2003-05-21Bugherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-21MAJherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ...herbelin
2003-05-21majfilliatr
2003-05-20CoqIde: externalsmonate
2003-05-20Prise en compte notation dans Inductif pour traducteurherbelin
2003-05-20command_windows fixmonate
2003-05-20Extension renommageherbelin
2003-05-20majfilliatr
2003-05-19Affichage METAherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 00:30:49 +0000