aboutsummaryrefslogtreecommitdiff
path: root/pretyping/class.ml
AgeCommit message (Expand)Author
2000-11-20Mieux à sa place dans toplevelherbelin
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
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-10Ajout d'un LetIn primitif.herbelin
2000-08-08reparation bug des coercions (cas ou on importe une coercion faisantbarras
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-01-11Ajout de Recordherbelin