aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenvtac.mli
AgeCommit message (Expand)Author
2008-12-14Fix looping class resolution bug discovered by B. Aydemir and use themsozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-10simplification de clenvbarras
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03premiere reorganisation de l\'unificationbarras