diff options
| author | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
| commit | 61aeca9ca2a7c46b143b90583dfb84b037eccc5b (patch) | |
| tree | 936cab27bacc3bb779aff810be7b79425544f10d /vernac/declareDef.ml | |
| parent | 6e5fee168d874b7b6fe7d5c8f4384661bf328d79 (diff) | |
| parent | c62aa0e9d0c33a70822e66a422d4c5926a8c8df7 (diff) | |
Merge PR #12372: [declare] Refactor constant information into a record.
Reviewed-by: SkySkimmer
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]"] |