aboutsummaryrefslogtreecommitdiff
path: root/kernel/term_typing.ml
AgeCommit message (Expand)Author
2006-10-30Débranchement du polymorphisme de sorte sur les définitions dans Typeherbelin
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite nouvel avertissement Z de ocaml 3.09herbelin
2004-11-22compatibility with POWERPCgregoire
2004-11-17bug module M:=N avec vmbarras
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2002-12-10Déplacement du hash-consing vers declare.mlherbelin
2002-10-07Lazy manuelles dans le codecoq
2002-10-05Lazy experimentale temporaire...coq
2002-08-02Modules dans COQ\!\!\!\!coq