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
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
