aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
AgeCommit message (Expand)Author
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-08-08reparation bug des coercions (cas ou on importe une coercion faisantbarras
2000-01-07Déplacement non-affichage des coercions dans termastherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-05changement type add_anonymous_leaffilliatr
1999-12-02Modifs suite à intégration de class.mlherbelin
1999-12-02affichage classes et coercionsfilliatr
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
1999-11-29portage Astterm (partiellement)filliatr
1999-11-26module Classops; ajout de fonctions dans Declare en consequencefilliatr
1999-11-25Des progres dans l'integrationherbelin
1999-11-24Versions initialesherbelin