aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/entries.ml
Commit message (Expand)AuthorAge
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* Remove special declaration of primitive projections in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Let definitions do not create new universe constraints.Gravatar Pierre-Marie Pédrot2017-12-19
* Specific type for section definition entries.Gravatar Pierre-Marie Pédrot2017-12-19
* [api] Remove kernel dependency on intf (Decl_kind)Gravatar Emilio Jesus Gallego Arias2017-12-10
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
* [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Proof using ...Gravatar gareuselesinge2011-12-12
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 11:04:10 +0000