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. --- vernac/lemmas.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/lemmas.ml') 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 -- cgit v1.2.3