From 15cb1aace0460e614e8af1269d874dfc296687b0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 1 Mar 2012 18:59:04 +0000
Subject: 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
---
 kernel/univ.ml  | 8 ++++++++
 kernel/univ.mli | 4 ++++
 2 files changed, 12 insertions(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3