From 21750c40ee3f7ef3103121db68aef4339dceba40 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 15 Dec 2017 19:09:15 +0100
Subject: [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.
---
 pretyping/inductiveops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 34df7d3d72..78e6bc6f14 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -275,7 +275,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 
 let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+  | Some (Some _) -> mib.mind_finite == BiFinite
   | _ -> true
 
 (* Annotation for cases *)
@@ -486,7 +486,7 @@ let find_inductive env sigma c =
   let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
-        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite ->
         let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
@@ -496,7 +496,7 @@ let find_coinductive env sigma c =
   let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
-        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite ->
         let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
-- 
cgit v1.2.3