aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* nouvelle implantation de la reductionGravatar barras2001-03-01
* uniformisation avec constr des lieurs dans rawterm/patternGravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Prise en compte du let-in dans lookup_*_as_renamedGravatar herbelin2001-01-30
* Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...Gravatar herbelin2000-12-14
* Utilisation de global_reference dans rawconstr; blindage pour quand appelé d...Gravatar herbelin2000-11-20
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Bug affichage du nom des letinGravatar herbelin2000-10-11
* 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
* Nettoyage de GenericGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* N'importe quel rawconstr maintenant dans le contexte d'une référenceGravatar herbelin2000-04-26
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Traduction constr->rawconstr (avant dans TermastGravatar herbelin2000-01-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 10:58:12 +0000