aboutsummaryrefslogtreecommitdiff
path: root/tactics/hiddentac.ml
AgeCommit message (Expand)Author
2003-11-13factorisation et generalisation des clausesbarras
2003-11-06Added Instantiate ... incorbinea
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-12*** empty log message ***barras
2003-01-25Un type "standardisé" pour new_hypherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-03-15entetesfilliatr
2000-05-03Ajout du langage de tactiquesdelahaye
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:28:33 +0000