index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
uGraph.mli
Age
Commit message (
Expand
)
Author
2021-01-06
Further pushing up the printing and sorting of universes.
Pierre-Marie Pédrot
2020-09-28
Put type-in-type flag in ugraph.
Gaëtan Gilbert
2020-05-13
Make explicit that UGraph lower bounds are only of two kinds.
Pierre-Marie Pédrot
2020-04-16
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-08-26
Make kernel parametric on the lowest universe and fix #9294
Matthieu Sozeau
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-03-14
Add a non-cumulative impredicative universe SProp.
Gaëtan Gilbert
2018-12-17
Make ugraph implementation abstract wrt universe specifics
Gaëtan Gilbert
2018-11-27
Fix #8364: making univ algebraic when already equal to another.
Gaëtan Gilbert
2018-11-23
Local universes for opaque polymorphic constants.
Gaëtan Gilbert
2018-11-16
Use universe names when printing to dot.
Gaëtan Gilbert
2018-10-06
[api] Remove (most) 8.9 deprecated objects.
Emilio Jesus Gallego Arias
2018-07-25
kernel: missing check that all universes are declared.
Matthieu Sozeau
2018-06-22
Define and use UGraph.enforce_leq_alg for subtyping inference
Gaëtan Gilbert
2018-05-30
Fix restrict_universe_context
Gaëtan Gilbert
2018-04-13
universe normalisation: put equivalence class partition in UGraph
Gaëtan Gilbert
2018-03-05
Replace invalid tag @raises in ocamldoc comments with @raise
mrmr1993
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-09
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-11
Cleaning up the implementation of module subtyping in the kernel.
Pierre-Marie Pédrot
2017-05-23
Merge PR#518: Faster universe unification
Maxime Dénès
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-27
Fast path when checking equality of universe levels in UState.
Pierre-Marie Pédrot
2015-10-06
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
