From fda9bdb09a2f2f7b98351e047ae43f097b428902 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 30 Oct 2019 17:55:27 +0100
Subject: [vernac] Remove deprecated function.

---
 vernac/comAssumption.ml | 15 ---------------
 1 file changed, 15 deletions(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d97bf6724c..2e9f0283ca 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -277,18 +277,3 @@ let context ~poly l =
   if Global.sections_are_opened ()
   then context_insection sigma ~poly ctx
   else context_nosection sigma ~poly ctx
-
-(* Deprecated *)
-let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name =
-let open DeclareDef in
-match scope with
-| Discharge ->
-  let univs = match univs with
-    | Monomorphic_entry univs -> univs
-    | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
-  in
-  let () = Declare.declare_universe_context ~poly univs in
-  declare_variable is_coe ~kind typ imps impl name;
-  GlobRef.VarRef name.CAst.v, Univ.Instance.empty
-| Global local ->
-  declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name
-- 
cgit v1.2.3