From d83e95cce852c5471593a27d0fdca39a262c885f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 20 May 2020 00:47:21 +0200
Subject: [declare] [api] Removal of deprecated functions

The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.

All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
---
 vernac/declareDef.ml | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 vernac/declareDef.ml

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
deleted file mode 100644
index 83bb1dae71..0000000000
--- a/vernac/declareDef.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-type locality = Declare.locality =
-  | Discharge [@ocaml.deprecated "Use [Declare.Discharge]"]
-  | Global of Declare.import_status [@ocaml.deprecated "Use [Declare.Global]"]
-[@@ocaml.deprecated "Use [Declare.locality]"]
-
-let declare_definition = Declare.declare_definition
-[@@ocaml.deprecated "Use [Declare.declare_definition]"]
-module Hook = Declare.Hook
-[@@ocaml.deprecated "Use [Declare.Hook]"]
-- 
cgit v1.2.3