diff options
| author | Gaëtan Gilbert | 2018-10-20 22:16:22 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-20 22:16:22 +0200 |
| commit | fd214f1ad31d88c76dd928b6c6b039eaefcb21db (patch) | |
| tree | 10327a156140bb6e671237ebac7cb6459247346e /kernel/names.ml | |
| parent | 16e0223e111cdf1c61c421617dfda08de6e96720 (diff) | |
| parent | c3bafe593f431bf5ae1313a591a9ee719098a9f1 (diff) | |
Merge PR #8769: [library] Remove redundant re-addition of universe constraints.
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions