aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_tactic.ml4
AgeCommit message (Expand)Author
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-03-19Ajout de l'entrée ne_constrarg_listdelahaye
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
2001-12-13compat ocaml 3.03filliatr
2001-11-05GROS COMMIT:barras
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...herbelin
2001-09-20Transparentbarras
2001-09-14Ajout syntaxe "Assert H:T."herbelin
2001-08-28Remplace numarg -> pure_numarg dans Double Inductionmohring
2001-08-10Parsingherbelin
2001-08-08Renommage TrueCut -> Assertherbelin
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...herbelin
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-06-19Extension des parametres de Clear + Instdelahaye
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-06-11Fix de quelques bugs syntaxiques de Ltacdelahaye
2001-04-24Les clauses de Rec doivent prendre des tactic_atom'sdelahaye
2001-04-20Petit menagedelahaye
2001-04-19*** empty log message ***mayero
2001-04-19Essais dans Ltacdelahaye
2001-04-14Non parenthesage des applications de tactiquesdelahaye
2001-04-12Ajout de _ dans les patterns d'intromohring
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...filliatr
2001-03-15entetesfilliatr
2001-02-16Prise en compte noms longs dans SuperAutoherbelin
2001-02-07Modif pour les patterns de sous-termesdelahaye
2001-02-01*** empty log message ***mohring
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des const...filliatr
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-20ajout ident_or_constrarg pour NewInductionherbelin
2000-12-19Correction associativite de Repeat/Orelsedelahaye
2000-12-11numarg -> pure_numarg a poursuivremohring
2000-12-06Extension de la syntaxe de LetTacherbelin
2000-12-06Correction pour les qualidconstargdelahaye
2000-12-05Plus de quote devant les ident et les ?delahaye
2000-11-28Elimination du 'delahaye
2000-11-26Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...herbelin
2000-11-23Bug qualidconstarg (intervient pour Transparent)herbelin
2000-11-20Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT pou...herbelin
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-10-30Priorite du Try/Orelse + Debug switch + correction bug dans Patterndelahaye
2000-10-03Ajout castedopenconstrarg; Renommage tactique Let en LetTacherbelin
2000-08-17Pattern matching de sous-termes + exceptions dans le lexerdelahaye
2000-07-21Modifs d'interpretation de patterns + exceptions dans le lexerdelahaye
2000-05-03Ajout du langage de tactiquesdelahaye
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 15:23:46 +0000