diff options
| author | Gaëtan Gilbert | 2020-03-31 15:10:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-25 14:17:21 +0200 |
| commit | ae1acfefe52937ea7e3a098137df032363051361 (patch) | |
| tree | e9286129872296964cce1b59ab6171c4afb6647d /kernel/nativecode.ml | |
| parent | 50361dc784c8967e7c4b254102e2cb21cb7e9f9e (diff) | |
Generate names for anonymous polymorphic universes
This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions