aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-09-06Pour accomoder autant le printer v8 que v7herbelin
2003-09-06Protection contre les types sans corps associéherbelin
2003-09-05bug dans calcul nb d'occurrencesletouzey
2003-08-28correction d'un stack overflow possible (PR#320)letouzey
2003-08-14Traducteur de correctnessherbelin
2003-08-14code mortherbelin
2003-08-14Traduction mlnamesherbelin
2003-08-14Notation access au dessous du niveau applicatif (2eme)herbelin
2003-08-13Notation access au dessous du niveau applicatifherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-07-11Ground bugfixcorbinea
2003-07-10bug typage du cases/identity: optim off si inductif avec varsletouzey
2003-07-10renommage des modules 1er niveau en monolithiqueletouzey
2003-07-08Ground updatecorbinea
2003-07-08 bug match matchletouzey
2003-07-04Ground bugfixcorbinea
2003-07-03switching back to old tautocorbinea
2003-07-03modification groundcorbinea
2003-07-03addition of Auto hints in Groundcorbinea
2003-07-02added hints into Groundcorbinea
2003-06-22Ground updatecorbinea
2003-06-20Ground updatecorbinea
2003-06-20Ground Update.corbinea
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-16Ground updatecorbinea
2003-06-16ground updatecorbinea
2003-06-15Ground major update ... mmm, sounds exciting !corbinea
2003-06-14ground updatecorbinea
2003-06-14Major Ground update, may break semanticscorbinea
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
2003-06-13Ground updatecorbinea
2003-06-13Ground update, new files.corbinea
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-06-13Ground update.corbinea
2003-06-12enieme correction du nommage modulaireletouzey
2003-06-12fin de l'affichage des signatures de modules dans les *.mlletouzey
2003-06-10Typoherbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-06-10Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...herbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-06-10Globalisation de ce qui n'etait pas encore globaliseherbelin
2003-06-08interaction entre fun/case permut et assert falseletouzey
2003-06-04bugfix for Ground ( merci JC )corbinea
2003-06-04Ground update + some bugfixcorbinea
2003-05-30oupsletouzey
2003-05-29Ground daily updatecorbinea
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