aboutsummaryrefslogtreecommitdiff
path: root/tactics/refine.mli
AgeCommit message (Expand)Author
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-07-16Nouvelle en-têteherbelin
2003-12-13Correction bug soumis par Yvesherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...herbelin
2000-07-20portage Refinefilliatr