diff options
| author | Emilio Jesus Gallego Arias | 2018-10-18 22:47:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-18 23:25:58 +0200 |
| commit | c3bafe593f431bf5ae1313a591a9ee719098a9f1 (patch) | |
| tree | dd79a69f29599a7360e318d7e3e91538465112e5 /dev/include | |
| parent | c3823156da73a63967d9d472e21560af1585b271 (diff) | |
[library] Remove redundant re-addition of universe constraints.
After some analysis this should be taken care of by
`Safe_typing.add_constant`
It was added in
https://github.com/coq/coq/commit/f7338257584ba69e7e815c7ef9ac0d24f0dec36c
, so maybe @gares can provide more context as to how is this stuff
supposed to work.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions