aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/refine.ml
Commit message (Expand)AuthorAge
* nouvelle implantation de la reductionGravatar barras2001-03-01
* suppression warning et calcule type dans replace_by_meta dans tous les casGravatar filliatr2000-12-15
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* mise en pageGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 23:33:40 +0000