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/environ.mli | |
| 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/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 9f6ea522a..714c26066 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -41,7 +41,7 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env -val universes : env -> Univ.universes +val universes : env -> UGraph.t val rel_context : env -> rel_context val named_context : env -> named_context val named_context_val : env -> named_context_val |