diff options
| author | letouzey | 2012-03-01 18:59:04 +0000 |
|---|---|---|
| committer | letouzey | 2012-03-01 18:59:04 +0000 |
| commit | 15cb1aace0460e614e8af1269d874dfc296687b0 (patch) | |
| tree | 87f3c4237d3ef3dd9b34af8a4c8f2772f470243d /kernel | |
| parent | 70d8c1e7a24b542c8e3f1788fd18226e2469801b (diff) | |
Univ: a univ_depends function to avoid a hack in Inductiveops
univ_depends checks whether a universe variable appears or
is equal to a universe. In comparison with the previous hack
in inductiveops based on try...catching UniverseInconsistency,
this should be semantically equivalent, simplier, and more
robust in case we allow someday an unsafe mode where
merge_constraints would be a no-op.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
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 1aad0fce14..0193542a36 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 8b3f62910a..e4e66915d1 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 |