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 ---
 library/lib.mli | 2 --
 2 files changed, 5 deletions(-)

(limited to 'library')

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 ())
 
diff --git a/library/lib.mli b/library/lib.mli
index d3315b0f2e..59d77480e9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,8 +183,6 @@ val is_in_section : GlobRef.t -> bool
 
 val replacement_context : unit -> Opaqueproof.work_list
 
-val is_polymorphic_univ : Univ.Level.t -> bool
-
 (** {6 Discharge: decrease the section level if in the current section } *)
 
 (* XXX Why can't we use the kernel functions ? *)
-- 
cgit v1.2.3