From 6291e5b13e74ef3cd0b2354266352470f88cc70e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 16:55:13 +0200
Subject: [declare] [compat] Remove exception alias.

---
 vernac/declare.ml  |  3 ---
 vernac/declare.mli | 25 +++++++++++--------------
 2 files changed, 11 insertions(+), 17 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index e72f5a0397..fc52c05793 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1184,9 +1184,6 @@ let prepare_parameter ~poly ~udecl ~types sigma =
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, (None(*proof using*), (typ, univs), None(*inline*))
 
-(* Compat: will remove *)
-exception AlreadyDeclared = DeclareUniv.AlreadyDeclared
-
 module Obls = struct
 
 open Constr
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 4f6b2f70da..e0af3a7344 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -406,17 +406,6 @@ val fixpoint_message : int array option -> Id.t list -> unit
 
 val check_exists : Id.t -> unit
 
-(** {6 For internal support, do not use}  *)
-
-module Internal : sig
-
-  type constant_obj
-
-  val objConstant : constant_obj Libobject.Dyn.tag
-  val objVariable : unit Libobject.Dyn.tag
-
-end
-
 (** Semantics of this function is a bit dubious, use with care *)
 val build_by_tactic
   :  ?side_eff:bool
@@ -437,9 +426,6 @@ val prepare_obligation
   -> Evd.evar_map
   -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
 
-(* Compat: will remove *)
-exception AlreadyDeclared of (string option * Names.Id.t)
-
 module Obls : sig
 
 type 'a obligation_body = DefinedObl of 'a | TermObl of constr
@@ -545,3 +531,14 @@ val obl_substitution :
 val dependencies : Obligation.t array -> int -> Int.Set.t
 
 end
+
+(** {6 For internal support, do not use}  *)
+
+module Internal : sig
+
+  type constant_obj
+
+  val objConstant : constant_obj Libobject.Dyn.tag
+  val objVariable : unit Libobject.Dyn.tag
+
+end
-- 
cgit v1.2.3