aboutsummaryrefslogtreecommitdiff
path: root/kernel/declarations.ml
AgeCommit message (Expand)Author
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-06-05Use projection indices in native compilation rather than constant names.Pierre-Marie Pédrot
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.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-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16A short cleanupAmin Timany
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-06-07Put all plugins behind an "API".Matej Kosik
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 nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-10-10Hash-consing of mutual_inductive_body (and Univ.constraints)letouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-02-24Mod_subst: improving sharing of subst_mpsletouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-20Mrec was not substituted correctlybarras
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:04:51 +0000