aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
2003-04-01remplace == par = dans la tactique field pour que le debugger marche a nouvea...narboux
2003-04-01Fail 1 pour traverser le matchherbelin
2003-03-31Noms absolusherbelin
2003-03-31Plus de eqT; message Failherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
2003-03-31minus a changé d'emplacement -> omega pas contentletouzey
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-25Extract Constant marche avec les axiomes schémas de typesletouzey
2003-03-24Bugfix pour Linear.corbinea
2003-03-21Fin de la résurrection de Linear.corbinea
2003-03-12*** empty log message ***barras
2003-03-12* Ajout du traducteur nouvelle syntaxe *barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 17:55:26 +0000