aboutsummaryrefslogtreecommitdiff
path: root/kernel/entries.mli
AgeCommit message (Expand)Author
2017-07-25[api] Put modules in order in API.{mli,ml}Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-16Extend definition of inductives to include subtyping infoAmin Timany
2017-03-24Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Making the side_effects type opaque.Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
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-08-25CLEANUP: Type alias "Context.section_context" was removedMatej Kosik
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:18:45 +0000