aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/entries.ml
Commit message (Expand)AuthorAge
* Types inductifs parametriquesGravatar mohring2005-11-02
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-tĂȘteGravatar herbelin2004-07-16
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02