aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-05-29Ne pas mettre d'associatif a droite au niveau 3 en V7herbelin
2003-05-29:= dans un record engendre un LetIn qui n'etait pas géréletouzey
2003-05-28gestion plus fine des beta-redex lineaires (cf nb_occur_match)letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 15:32:30 +0000