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 -
 library/universes.ml | 2 +-
 3 files changed, 4 insertions(+), 2 deletions(-)

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
diff --git a/library/universes.ml b/library/universes.ml
index f6922e4958..765d34f98f 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -627,7 +627,7 @@ let normalize_context_set ctx us algs =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
     let g = Univ.merge_constraints csts Univ.empty_universes in
-      Univ.constraints_of_universes (Univ.normalize_universes g)
+      Univ.constraints_of_universes g
   in
   let noneqs =
     Constraint.fold (fun (l,d,r) noneqs ->
-- 
cgit v1.2.3