aboutsummaryrefslogtreecommitdiff
path: root/intf/decl_kinds.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-27 10:19:29 +0100
committerMaxime Dénès2017-12-27 10:19:29 +0100
commitf6857ce53ecf64b0086854495b4a8451f476d5b4 (patch)
tree7c36a59b64fcd20b3666eca8de54b4fd33606cc1 /intf/decl_kinds.ml
parent4969f9425cb0d5cd5bd735110886a0cbd2641588 (diff)
parent21750c40ee3f7ef3103121db68aef4339dceba40 (diff)
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
Diffstat (limited to 'intf/decl_kinds.ml')
-rw-r--r--intf/decl_kinds.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index b0c1f66613..b9a3f0c212 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -77,6 +77,9 @@ type logical_kind =
type recursivity_kind = Declarations.recursivity_kind =
| Finite (** = inductive *)
+ [@ocaml.deprecated "Please use [Declarations.Finite"]
| CoFinite (** = coinductive *)
+ [@ocaml.deprecated "Please use [Declarations.CoFinite"]
| BiFinite (** = non-recursive, like in "Record" definitions *)
+ [@ocaml.deprecated "Please use [Declarations.BiFinite"]
[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]