aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/refine.ml
Commit message (Expand)AuthorAge
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* cosmétiqueGravatar herbelin2000-08-28
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* portage RefineGravatar filliatr2000-07-20