aboutsummaryrefslogtreecommitdiff
path: root/proofs/tacexpr.ml
AgeCommit message (Expand)Author
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-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
2002-10-13Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Fichier des expressions de tactiquesherbelin