diff options
| author | Gaëtan Gilbert | 2020-12-02 14:09:06 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-12-02 14:09:06 +0100 |
| commit | ecb23dc8db0682ec327a110482b034677aecb6e9 (patch) | |
| tree | 5622375bf7bb895336101f9bb70b92fdd6570212 /kernel/cPrimitives.ml | |
| parent | ad8cf0108e628710128e5a6e266b72895eed98b9 (diff) | |
Stop calling Id.Map.domain on univ binders every individual universe
Diffstat (limited to 'kernel/cPrimitives.ml')
0 files changed, 0 insertions, 0 deletions