aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
Commit message (Expand)AuthorAge
* Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
* Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
* Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Adding a sanity check on inductive variance subtyping.Gravatar Pierre-Marie Pédrot2018-02-15
* Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\
| * Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-12
* | Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
* | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* | Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
|/
* Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* 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
* Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
* Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* Asserting that monomorphic section variables have no abstracted context.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Simplify Univ.mlGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
* New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* Univs (kernel) adapt to new invariantsGravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Adding a primitive to merge ContextSets which is more efficient when oneGravatar Pierre-Marie Pédrot2014-08-09
* Cleaning up interface of ContextSet.Gravatar Pierre-Marie Pédrot2014-08-09
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 02:27:54 +0000