aboutsummaryrefslogtreecommitdiff
path: root/tactics/auto.mli
AgeCommit message (Expand)Author
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
2001-03-15entetesfilliatr
2001-02-26Eauto version en largeurmohring
2001-02-16Prise en compte noms longs dans SuperAutoherbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-10-18Renommage canonique :herbelin
2000-10-11Prise en compte de l'env local dans make_apply_entryherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-12-05premier debugagefilliatr
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr