index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
univ.mli
Commit message (
Expand
)
Author
Age
*
Moving some universe substitution code out of the kernel.
Pierre-Marie Pédrot
2017-12-30
*
Returning instance instead of substitution in universe context abstraction.
Pierre-Marie Pédrot
2017-12-30
*
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-09
*
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
The only abstraction-breaking function in Univ is now AUContext.instance.
Pierre-Marie Pédrot
2017-07-13
*
Moving the last bits of abtraction-breaking code out of the kernel.
Pierre-Marie Pédrot
2017-07-11
*
Cleaning up the implementation of module subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
*
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
*
Asserting that monomorphic section variables have no abstracted context.
Pierre-Marie Pédrot
2017-07-11
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Simplify Univ.ml
Amin Timany
2017-06-16
*
Squashed commit of the following:
Amin Timany
2017-06-16
*
Check subtyping of inductive types in Kernel
Amin Timany
2017-06-16
*
New datastructure for universes of inductive types
Amin Timany
2017-06-16
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Univs: fix bug #3807
Matthieu Sozeau
2015-10-08
*
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
|
/
*
Univs: fix bug #4251, handling of template polymorphic constants.
Matthieu Sozeau
2015-10-02
*
Univs (kernel) adapt to new invariants
Matthieu Sozeau
2015-10-02
*
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Implement module subtyping for polymorphic constants (errors on
Matthieu Sozeau
2014-10-02
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Adding a primitive to merge ContextSets which is more efficient when one
Pierre-Marie Pédrot
2014-08-09
*
Cleaning up interface of ContextSet.
Pierre-Marie Pédrot
2014-08-09
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
Useless export of Instance.eqeq. We hashcons everything before calling this
Pierre-Marie Pédrot
2014-07-31
*
Universe level maps use HMaps.
Pierre-Marie Pédrot
2014-07-21
*
Cleanup substitution inside universe instances, only done through subst_fn now,
Matthieu Sozeau
2014-07-21
*
Cleanup code related to the constraint solving, which sits now outside the
Matthieu Sozeau
2014-07-03
*
Add toplevel commands to declare global universes and constraints.
Matthieu Sozeau
2014-07-01
*
Code factorization in LMap.
Pierre-Marie Pédrot
2014-06-18
*
Made explanations for universe inconsistencies optional. They are only used
Pierre-Marie Pédrot
2014-06-10
*
- Fix substitution of universes which needlessly hashconsed existing universes.
Matthieu Sozeau
2014-06-10
*
More cleanup/reorganizing of univ.ml to separate constraint/universe handling...
Matthieu Sozeau
2014-06-10
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
Remove unused function in univ
Matthieu Sozeau
2014-06-10
[next]