aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
* 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