diff options
| author | Emilio Jesus Gallego Arias | 2020-05-20 00:47:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | d83e95cce852c5471593a27d0fdca39a262c885f (patch) | |
| tree | 9117298b6f6d0a69e6863578858de27ddb23e8ba /vernac/declareDef.ml | |
| parent | 7d183d8a12a03a608a3dc8a724142468b45886ac (diff) | |
[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.
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 9 |
1 files changed, 0 insertions, 9 deletions
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]"] |