aboutsummaryrefslogtreecommitdiff
path: root/tactics/eauto.ml
AgeCommit message (Expand)Author
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-06-28Modifs de presentation.delahaye
2000-06-21portage EAuto et Ringfilliatr