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.
---
 kernel/section.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/section.mli b/kernel/section.mli
index fc3ac141e4..56b4d9ba8f 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -83,5 +83,3 @@ val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list
 (** Section segments of all declarations from this section. *)
 
 val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool
-
-val is_polymorphic_univ : Level.t -> 'a t -> bool
-- 
cgit v1.2.3