diff options
| author | Gaëtan Gilbert | 2018-04-28 21:36:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-17 18:47:10 +0200 |
| commit | 748a33cee41900d285897b24b4d8e29dd9eb2a3d (patch) | |
| tree | 1cac3f0d220fecc75e5b445f8b65d8d224d76c77 /engine/engine.mllib | |
| parent | d41eaff0b2c6f2ff10ef851864abfa3366862d22 (diff) | |
Split off Universes functions for minimization.
This finishes the splitting of Universes.
Diffstat (limited to 'engine/engine.mllib')
| -rw-r--r-- | engine/engine.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index befd49dc96..37e83b6238 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ UnivNames UnivGen UnivSubst UnivProblem +UnivMinim Universes Univops UState |