From 8398ec48072b0bbe5e571a8d1f1f6c1ace9270f4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 5 Oct 2019 12:16:34 +0200
Subject: Remove "is_polymorphic_univ" checks in upper layers.

There were 2:

- when declaring a constraint to avoid monomorphic constraint
  referring to polymorphic univs, this check is redundant with the
  check in Section.ml

- when declaring a universe context to avoid redeclaring universes,
  this is not necessary after recent commits.
---
 library/lib.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 991e23eb3a..0d9efe2d5d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -425,9 +425,6 @@ let extract_worklist info =
 
 let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
 
-let is_polymorphic_univ u =
-  Section.is_polymorphic_univ u (sections ())
-
 let replacement_context () =
   Section.replacement_context (Global.env ()) (sections ())
 
-- 
cgit v1.2.3