diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 8 | ||||
| -rw-r--r-- | kernel/univ.mli | 4 |
2 files changed, 12 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 1aad0fce1..0193542a3 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -801,6 +801,14 @@ let no_upper_constraints u cst = | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst | Max _ -> anomaly "no_upper_constraints" +(* Is u mentionned in v (or equals to v) ? *) + +let univ_depends u v = + match u, v with + | Atom u, Atom v -> u = v + | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl + | _ -> anomaly "univ_depends given a non-atomic 1st arg" + (* Pretty-printing *) let pr_arc = function diff --git a/kernel/univ.mli b/kernel/univ.mli index 8b3f62910..e4e66915d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -91,6 +91,10 @@ val subst_large_constraints : val no_upper_constraints : universe -> constraints -> bool +(** Is u mentionned in v (or equals to v) ? *) + +val univ_depends : universe -> universe -> bool + (** {6 Pretty-printing of universes. } *) val pr_uni_level : universe_level -> Pp.std_ppcmds |