aboutsummaryrefslogtreecommitdiff
path: root/tactics/hiddentac.ml
AgeCommit message (Expand)Author
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