diff options
| author | Matthieu Sozeau | 2015-09-23 16:11:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:10 +0200 |
| commit | 26628315688e07c43b9881872a737454e93fe4c9 (patch) | |
| tree | 36dfc2e0a04a5901c840990bc0bd989e1d7feff7 /kernel/type_errors.mli | |
| parent | e841deb4750d43ab19f91907476d75fc73860c5a (diff) | |
Univs: minimization, adapt to graph invariants.
We are forced to declare universes that are global and appear in the
local constraints as we start from an empty universe graph.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions