[api] Also deprecate constructors of Decl_kinds.

Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.

In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.

5 files changed, 6 insertions, 6 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 31ded9129a..11616da7b3 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -810,7 +810,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (_,projs,pbs)) when
-	mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
+        mib.Declarations.mind_finite == Declarations.BiFinite ->
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8e9b606a58..1f2ae0b6cc 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -710,7 +710,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
     best-effort fashion. *)
 let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
   let ntypes = Array.length inds in
-  let recursive = finite != Decl_kinds.BiFinite in
+  let recursive = finite != BiFinite in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
   let ra_env_ar = Array.rev_to_list rc in
   let nparamsctxt = Context.Rel.length paramsctxt in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2a629f00a9..28a09b81b0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -38,14 +38,14 @@ let find_inductive env c =
   let (t, l) = decompose_app (whd_all env c) in
   match kind t with
     | Ind ind
-        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_all env c) in
   match kind t with
     | Ind ind
-        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let inductive_params (mib,_) = mib.mind_nparams
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index de4dc21079..160a90dc2f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -515,7 +515,7 @@ let rec lambda_of_constr env sigma c =
 	    { asw_ind = ind;
           asw_ci = ci;
           asw_reloc = tbl; 
-          asw_finite = mib.mind_finite <> Decl_kinds.CoFinite;
+          asw_finite = mib.mind_finite <> CoFinite;
           asw_prefix = prefix}
       in
       (* translation of the argument *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2913c6dfad..d0d5cb1d56 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -193,7 +193,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (arities_of_specif (mind, inst) (mib2, p2))
   in
   let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
-  check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
+  check (fun mib -> mib.mind_finite<>CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
   check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x);
   assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps);
   assert (Array.length mib1.mind_packets >= 1