aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
Commit message (Expand)AuthorAge
* [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
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Code factorization in LMap.Gravatar Pierre-Marie Pédrot2014-06-18
* Made explanations for universe inconsistencies optional. They are only usedGravatar Pierre-Marie Pédrot2014-06-10
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
* More cleanup/reorganizing of univ.ml to separate constraint/universe handling...Gravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Remove unused function in univGravatar Matthieu Sozeau2014-06-10
* Function in Univ uselessly exported.Gravatar Pierre-Marie Pédrot2014-06-08
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:25:50 +0000