aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Bug de contextesGravatar herbelin2000-12-26
* DĂ©placement du type stack de Reduction vers Closure et utilisation pour accĂ...Gravatar herbelin2000-12-26
* Utilisation de Let In pour les constantes locales, prise en compte des Let In...Gravatar herbelin2000-11-27
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Petit nettoyage de Evarutil et EvarconvGravatar herbelin2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01
* 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
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Achèvement abstraction du mécanisme (optionnel) de castGravatar herbelin2000-06-29
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Reparation bug isevars dans pretypingGravatar herbelin2000-03-10
* Poursuite intégration du CasesGravatar herbelin1999-12-13
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* portage modules Evarconv et EvarutilGravatar filliatr1999-11-29
* Versions initialesGravatar herbelin1999-11-24