diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 19:09:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 20:09:06 +0200 |
| commit | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (patch) | |
| tree | baee8c0b023277d43366996685503c9d1f855413 /kernel/kernel.mllib | |
| parent | c4db6fc1086d984fd983ff9a6797ad108d220b98 (diff) | |
Splitting kernel universe code in two modules.
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
Diffstat (limited to 'kernel/kernel.mllib')
| -rw-r--r-- | kernel/kernel.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 29fe887d7..f7220c94a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,6 +1,7 @@ Names Uint31 Univ +UGraph Esubst Sorts Evar |