aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.ml
Commit message (Expand)AuthorAge
* changement comparaison etatsGravatar filliatr2001-03-08
* Modification de e_give_exact pour eviter d'echouer sur l'unificationGravatar mohring2001-03-06
* eta-expansionGravatar mohring2001-03-06
* EAutod (debug)Gravatar filliatr2001-03-06
* module Explore générique et réécriture EAuto avec ce module; occur check ...Gravatar filliatr2001-03-05
* modifGravatar mohring2001-02-28
* EAuto mixte (largeur puis profondeur)Gravatar mohring2001-02-27
* Eauto version en largeurGravatar mohring2001-02-26
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Prise en compte de l'env local dans make_apply_entryGravatar herbelin2000-10-11
* 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
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Modifs de presentation.Gravatar delahaye2000-06-28
* portage EAuto et RingGravatar filliatr2000-06-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 21:55:13 +0000