aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite nouvel avertissement Z de ocaml 3.09Gravatar herbelin2005-11-08
* compatibility with POWERPCGravatar gregoire2004-11-22
* bug module M:=N avec vmGravatar barras2004-11-17
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Déplacement du hash-consing vers declare.mlGravatar herbelin2002-12-10
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 17:49:11 +0000