From 17810e2b920fefd69a407336ae1f090d2c878257 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 8 Jun 2014 00:20:38 +0200
Subject: Function in Univ uselessly exported.

---
 kernel/univ.ml  | 3 +++
 kernel/univ.mli | 1 -
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1c60f2c3a1..c1d01487ed 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -2272,6 +2272,9 @@ let constraints_of_universes g =
   in
   UMap.fold constraints_of g Constraint.empty
 
+let constraints_of_universes g =
+  constraints_of_universes (normalize_universes g)
+
 (* Pretty-printing *)
 
 let pr_arc = function
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 9398e23ba9..fee47235ae 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -423,7 +423,6 @@ exception UniverseInconsistency of univ_inconsistency
 
 val enforce_constraint : univ_constraint -> universes -> universes
 val merge_constraints : constraints -> universes -> universes
-val normalize_universes : universes -> universes
 val sort_universes : universes -> universes
 
 val constraints_of_universes : universes -> constraints
-- 
cgit v1.2.3