From 8de0fcaa08c82ece8874606e8fa1954d860bd88e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Apr 2020 03:13:08 +0200
Subject: [declare] [compat] Add alias for deprecated function

---
 vernac/declare.ml  | 2 ++
 vernac/declare.mli | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 6a4511ead8..366dd2d026 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -884,3 +884,5 @@ let declare_definition_scheme ~internal ~univs ~role ~name c =
 
 let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
 let _ = Abstract.declare_abstract := declare_abstract
+
+let declare_universe_context = DeclareUctx.declare_universe_context
diff --git a/vernac/declare.mli b/vernac/declare.mli
index a551c621c4..e23e148ddc 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -279,3 +279,6 @@ val build_constant_by_tactic :
   EConstr.types ->
   unit Proofview.tactic ->
   Evd.side_effects proof_entry * bool * UState.t
+
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
+[@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
-- 
cgit v1.2.3