aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
AgeCommit message (Expand)Author
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans l...herbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
2000-04-26N'importe quel rawconstr maintenant dans le contexte d'une référenceherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration d...herbelin
2000-01-07Traduction constr->rawconstr (avant dans Termastherbelin