From 249a1910a2474216b7f98491afafc6019a04c894 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Wed, 24 May 2017 23:46:23 +0200
Subject: Remove Warnings: unused value ...

---
 vernac/vernacentries.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'vernac/vernacentries.ml')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 957911e1e..21f053fb9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2091,12 +2091,6 @@ let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
   | Some b -> Flags.make_polymorphic_flag b; b
 
-let check_vernac_supports_cumulativity c p =
-  match p, c with
-  | None, _ -> ()
-  | Some _, (VernacInductive _ ) -> ()
-  | Some _, _ -> CErrors.error "This command does not support Cumulativity"
-
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
-- 
cgit v1.2.3