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/evarconv.ml     | 2 +-
 pretyping/inductiveops.ml | 6 +++---
 pretyping/unification.ml  | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f7a3789a21..788e4d268a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1044,7 +1044,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
+    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 30674fee27..b41fb4e4dd 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -666,7 +666,7 @@ let is_eta_constructor_app env sigma ts f l1 term =
   | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite &&
+      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
 	(** Check that the other term is neutral *)
 	is_neutral env sigma ts term
-- 
cgit v1.2.3