aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2003-09-18Interface Eautoherbelin
2003-09-12Indépendance vis à vis de Declareherbelin
2003-09-11Nettoyageherbelin
2003-09-09Protection traducteur contre meta de Grammar tacticherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-07-03switching back to old tautocorbinea
2003-07-02added hints into Groundcorbinea
2003-07-02suppression de newtautocorbinea
2003-06-27*** empty log message ***courant
2003-06-25Une completion de l'interpretation des TacAlias pour la partie interpretableherbelin
2003-06-20Ground Update.corbinea
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du traduct...herbelin
2003-06-10Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...herbelin
2003-05-25Ground and CCsolve updatescorbinea
2003-05-24Amélioration affichage locations; prise en compte variables dans lettac; ajo...herbelin
2003-05-22Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...herbelin
2003-05-22Preservation affichage des ?n en V7herbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-19Restructuration des procédures de filtrageherbelin
2003-05-13Separation entre les propositions de syntaxe - suiteherbelin
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-25Added the Ground tactic.corbinea
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
2003-04-14Bug: lookup inapproprie dans subst_tacticherbelin
2003-04-10Relachement globalisation Unfold en usage interactifherbelin
2003-04-10Trop de restriction pour les TacDefherbelin
2003-04-08Prise en compte des variables de grammaires de tactiques et dédollarisation ...herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07code mortherbelin
2003-04-03Backtrack du commit de Christine, qui posait probleme avec FTCletouzey
2003-04-01Extension de Replace aux égalités entre preuvesherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Ajout d'un message à FailTac; localisation des appels à des tactiques défi...herbelin
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-28Fixed Relative names not,iff in Camlp4 quotation.corbinea
2003-03-18Introducing Christine's Intuition1 and adding some invertible hyps.corbinea
2003-03-12*** empty log message ***barras
2003-02-26Changed Tauto so it displays less 'Unfold not iff'corbinea
2003-02-13Correction d'un bug introduit dans le backtracking d'occurrencedelahaye
2003-02-13Chargement dynamique de .cmadelahaye
2003-02-13Debugger plus informatifdelahaye
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 02:50:19 +0000