aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/entries.mli
Commit message (Expand)AuthorAge
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Removed some useless code in mod_typing that was redundant with safe_typing.Gravatar soubiran2007-02-21
* MAJ documentation en syntaxe v8Gravatar herbelin2006-03-18
* 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