aboutsummaryrefslogtreecommitdiff
path: root/kernel/term_typing.ml
AgeCommit message (Expand)Author
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-04-30Réutilisation de l'infrastructure pour le polymorphisme d'univers desherbelin
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 23:46:26 +0000