aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-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 b0c1f6661..b9a3f0c21 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"]