aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/entries.mli
Commit message (Expand)AuthorAge
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Entries module back to kernelGravatar ppedrot2012-10-26
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
* 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
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-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