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.

---
 library/universes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

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