From bd27f8b3c9894a73f3f93662f6ff11dfb8fb65c4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 24 Oct 2019 21:08:15 +0200
Subject: [vernac] [inductive] Remove unused internal export.

---
 vernac/comInductive.mli | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 3e1e9ceaf1..067fb3d2ca 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -67,7 +67,3 @@ val template_polymorphism_candidate :
    can be made parametric in its conclusion sort, if one is given.
    If the [Template Check] flag is false we just check that the conclusion sort
    is not small. *)
-
-val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t
-(** [sign_level env sigma ctx] computes the universe level of the context [ctx]
-    as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *)
-- 
cgit v1.2.3