diff options
| author | Maxime Dénès | 2018-06-26 14:59:24 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-26 14:59:24 +0200 |
| commit | 0b8c1aa84dc7200b055d45cf528a83163dfd21f8 (patch) | |
| tree | 73222697d2a80aa2ac34d46eb83f1172504e4cc9 /kernel/type_errors.mli | |
| parent | f6fe2741610552ffc9eb8cbe1f9061dedf965f90 (diff) | |
| parent | 3553d5d035f925e6b2f23daad5a8fdd2637a584d (diff) | |
Merge PR #7775: Fix handling of universe context for expanded program obligations.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions