aboutsummaryrefslogtreecommitdiff
path: root/kernel/entries.mli
AgeCommit message (Expand)Author
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-08State Transaction Machinegareuselesinge
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of mod_bound_idppedrot
2012-12-14Modulification of identifierppedrot
2012-10-26Moved Entries module back to kernelppedrot
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
2012-08-08Updating headers.herbelin
2011-12-12Proof using ...gareuselesinge
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2008-03-14Ajout des alias de module dans le noyau.soubiran
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2007-02-21Removed some useless code in mod_typing that was redundant with safe_typing.soubiran
2006-03-18MAJ documentation en syntaxe v8herbelin
2005-11-02Types inductifs parametriquesmohring
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2002-08-19La notation 'with'. L'interpretation - version preliminairecoq
2002-08-02Modules dans COQ\!\!\!\!coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:03:36 +0000