diff options
| author | Maxime Dénès | 2017-12-27 10:19:29 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:29 +0100 |
| commit | f6857ce53ecf64b0086854495b4a8451f476d5b4 (patch) | |
| tree | 7c36a59b64fcd20b3666eca8de54b4fd33606cc1 /API/API.mli | |
| parent | 4969f9425cb0d5cd5bd735110886a0cbd2641588 (diff) | |
| parent | 21750c40ee3f7ef3103121db68aef4339dceba40 (diff) | |
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/API/API.mli b/API/API.mli index e46bca85fc..def60ec267 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1443,9 +1443,9 @@ sig type record_body = (Id.t * Constant.t array * projection_body array) option type recursivity_kind = - | Finite - | CoFinite - | BiFinite + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) type mutual_inductive_body = { mind_packets : one_inductive_body array; @@ -2160,10 +2160,14 @@ module Decl_kinds : sig type polymorphic = bool type cumulative_inductive_flag = bool + type recursivity_kind = Declarations.recursivity_kind = - | Finite - | CoFinite - | BiFinite + | 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"] type discharge = |