aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareDef.ml
blob: 83bb1dae7157d29c593bc38335f0cea6c3889db8 (plain)
1
2
3
4
5
6
7
8
9
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]"]