aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hiddentac.ml
Commit message (Expand)AuthorAge
...
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Un type "standardisé" pour new_hypGravatar herbelin2003-01-25
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesGravatar herbelin2002-10-21
* NewDestruct/NewInduction acceptent l'option "using"Gravatar herbelin2002-10-21
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* entetesGravatar filliatr2001-03-15
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 14:27:23 +0000