[vernac] Remove deprecated function.

2 files changed, 0 insertions, 31 deletions

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
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index ae9edefcac..f5192fc696 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -50,19 +50,3 @@ val context
   :  poly:bool
   -> local_binder_expr list
   -> unit
-
-(** Deprecated *)
-val declare_assumption
-  : coercion_flag
-  -> poly:bool
-  -> scope:DeclareDef.locality
-  -> kind:Decls.assumption_object_kind
-  -> Constr.types
-  -> Entries.universes_entry
-  -> UnivNames.universe_binders
-  -> Impargs.manual_implicits
-  -> Glob_term.binding_kind
-  -> Declaremods.inline
-  -> variable CAst.t
-  -> GlobRef.t * Univ.Instance.t
-[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."]