[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, 9 insertions, 10 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 51dd5cd4f..ec6b62ee2 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -317,7 +317,7 @@ let build_beq_scheme mode kn =
       let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
 	if not (Sorts.List.mem InSet kelim) then
 	  raise (NonSingletonProp (kn,i));
-        if mib.mind_finite = Decl_kinds.CoFinite then
+        if mib.mind_finite = CoFinite then
 	  raise NoDecidabilityCoInductive;
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
         create_input fix),
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f3f50f41d..1c8677e9c 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -25,7 +25,6 @@ open Nametab
 open Impargs
 open Reductionops
 open Indtypes
-open Decl_kinds
 open Pretyping
 open Evarutil
 open Indschemes
@@ -411,7 +410,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
   (* spiwack: raises an error if the structure is supposed to be non-recursive,
         but isn't *)
   begin match mie.mind_entry_finite with
-  | BiFinite when is_recursive mie ->
+  | Declarations.BiFinite when is_recursive mie ->
       if Option.has_some mie.mind_entry_record then
         user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
       else
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e4ca98749..2f4c95aff 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -258,7 +258,7 @@ let declare_one_induction_scheme ind =
 
 let declare_induction_schemes kn =
   let mib = Global.lookup_mind kn in
-  if mib.mind_finite <> Decl_kinds.CoFinite then begin
+  if mib.mind_finite <> Declarations.CoFinite then begin
     for i = 0 to Array.length mib.mind_packets - 1 do
       declare_one_induction_scheme (kn,i);
     done;
@@ -268,7 +268,7 @@ let declare_induction_schemes kn =
 
 let declare_eq_decidability_gen internal names kn =
   let mib = Global.lookup_mind kn in
-  if mib.mind_finite <> Decl_kinds.CoFinite then
+  if mib.mind_finite <> Declarations.CoFinite then
     ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
 
 let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
@@ -512,7 +512,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
 let declare_default_schemes kn =
   let mib = Global.lookup_mind kn in
   let n = Array.length mib.mind_packets in
-  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+  if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag)
      && mib.mind_typing_flags.check_guarded then
     declare_induction_schemes kn;
   if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 27a680b9b..6ef310837 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -100,7 +100,7 @@ let find_mutually_recursive_statements sigma thms =
           match EConstr.kind sigma t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite ->
+                mind.mind_finite <> Declarations.CoFinite ->
               [ind,x,i]
           | _ ->
               []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in
@@ -110,7 +110,7 @@ let find_mutually_recursive_statements sigma thms =
         match EConstr.kind sigma whnf_ccl with
         | Ind ((kn,_ as ind),u) when
               let mind = Global.lookup_mind kn in
-              Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
+              Int.equal mind.mind_ntypes n && mind.mind_finite == Declarations.CoFinite ->
             [ind,x,0]
         | _ ->
             [] in
diff --git a/vernac/record.ml b/vernac/record.ml
index 114b55cb4..fb73f3a01 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -143,7 +143,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
   let assums = List.filter is_local_assum newps in
   let params = List.map (RelDecl.get_name %> Name.get_id) assums in
-  let ty = Inductive (params,(finite != BiFinite)) in
+  let ty = Inductive (params,(finite != Declarations.BiFinite)) in
   let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
   let env2,sigma,impls,newfs,data =
     interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
@@ -507,7 +507,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
          | Monomorphic_const_entry univs ->
            Monomorphic_ind_entry univs
        in
-       let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
+       let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in