aboutsummaryrefslogtreecommitdiff
path: root/kernel/entries.mli
AgeCommit message (Expand)Author
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-16Renaming variants of Entries.local_entryMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 1).Arnaud Spiwack
2015-01-12Update headers.Maxime Dénès
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-29Add test-suite file. Compute the name for the record binder in theMatthieu Sozeau
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-07-25- Do module substitution inside mind_record.Matthieu Sozeau
2014-06-17Safer entry point of primitive projections in the kernel, now it does recognizeMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:18:20 +0000