diff options
| author | Matthieu Sozeau | 2015-02-12 21:43:03 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-02-12 22:43:00 +0100 |
| commit | 43471abd4e61e7528fdaa2c576e7cb825a203c13 (patch) | |
| tree | 92e62950b9d3abb55376ce472ce21b820d76d038 /interp/modintern.ml | |
| parent | 7d06e602bea9e7a2c98e1c6badab3a667714b5c8 (diff) | |
Fix bug #2775: Correct handling of universes in leminv.
Diffstat (limited to 'interp/modintern.ml')
0 files changed, 0 insertions, 0 deletions