aboutsummaryrefslogtreecommitdiff
path: root/kernel/entries.ml
AgeCommit message (Expand)Author
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-08Template polymorphism is now a property of the inductive block.Pierre-Marie Pédrot
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-10-16Split the function used to declare side-effects from the standard one.Pierre-Marie Pédrot
2019-10-16Cleaning up the previous code by ensuring statically invariants on opaque pro...Pierre-Marie Pédrot
2019-10-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
2019-07-08Similar purity invariants in the kernel.Pierre-Marie Pédrot
2019-06-27Kernel transparent definition entries have no body universes.Gaëtan Gilbert
2019-06-26Perform the opaque section variable inference outside of the kernel.Pierre-Marie Pédrot
2019-06-24Code simplification for definition_entry type.Pierre-Marie Pédrot
2019-06-24Remove the unused opaque_entry_inline_code field from opaque entries.Pierre-Marie Pédrot
2019-06-24Enforce that opaque entries carry their type.Pierre-Marie Pédrot
2019-06-24Dedicated type for opaque entries in the kernel.Pierre-Marie Pédrot
2019-06-24Enforce that transparent entries are forced beforehand.Pierre-Marie Pédrot
2019-06-24Take advantage of the change of entry representation to split opacity status.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-26Remove a few circumvolutions around parameters of inductive entriesMaxime Dénès
2018-09-03Merge PR #7912: Simplify effects APIMaxime Dénès
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-17Remove special declaration of primitive projections in the kernel.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-19Let definitions do not create new universe constraints.Pierre-Marie Pédrot
2017-12-19Specific type for section definition entries.Pierre-Marie Pédrot
2017-12-10[api] Remove kernel dependency on intf (Decl_kind)Emilio Jesus Gallego Arias
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-25[api] Put modules in order in API.{mli,ml}Emilio Jesus Gallego Arias
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:56:40 +0000