aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declarations.ml
Commit message (Expand)AuthorAge
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
* Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* Use projection indices in native compilation rather than constant names.Gravatar Pierre-Marie Pédrot2018-06-05
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
* Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
* [api] Remove kernel dependency on intf (Decl_kind)Gravatar Emilio Jesus Gallego Arias2017-12-10
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
* Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A short cleanupGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Mod_subst: improving sharing of subst_mpsGravatar letouzey2011-02-24
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Mrec was not substituted correctlyGravatar barras2010-05-20
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 03:50:03 +0000