diff options
| author | Gaëtan Gilbert | 2018-12-04 16:22:18 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-17 14:49:13 +0100 |
| commit | a2ec08199d023b102df7806db8ed1e71c3ed27ce (patch) | |
| tree | 24d6607635a844f888c104309ee4f8d4c423a2e5 /kernel/type_errors.ml | |
| parent | 854d3e1b404fb3ee9087ffb07cbba7cc9196c1f9 (diff) | |
Make ugraph implementation abstract wrt universe specifics
This should give better visibility of universe specific operations vs
generic graph operations.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions