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/term.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/term.mli')
-rw-r--r-- | kernel/term.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 501aaf741..f8badb0dd 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -427,11 +427,11 @@ val eq_constr : constr -> constr -> bool (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) -val eq_constr_univs : constr Univ.check_function +val eq_constr_univs : constr UGraph.check_function (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) -val leq_constr_univs : constr Univ.check_function +val leq_constr_univs : constr UGraph.check_function (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) |