aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
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-25Ground and CCsolve updatescorbinea
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-21MAJherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-16Major Ground tactic update, sensible performance improvementcorbinea
2003-05-13Notations arithmetiquesherbelin
2003-05-08bugfixes in Ground.corbinea
2003-05-07Enhancement of the Ground tactic, addition of GTauto and GIntuition.corbinea
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-28bug concernant les projecteurs de Record avec args logiquesletouzey
2003-04-28adaptation a Acc_iterletouzey
2003-04-26bugfix in Ground tacticcorbinea
2003-04-25Added the Ground tactic.corbinea
2003-04-17Diversherbelin
2003-04-17Ajout "at next level" dans Notationherbelin
2003-04-17commentairesherbelin
2003-04-17Ooopsletouzey
2003-04-17temporaireletouzey
2003-04-16BIG MAJ Extraction:letouzey
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-04-11Explicitation arguments de eqherbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-09Alignement du comportement des implicites d'inductif en sortie de section sur...herbelin
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
2003-04-07Mauvaise resolution conflit dans commit precedentherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-03Légères simplifications code de Field; message d'erreur si pas égalitéherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 08:18:30 +0000