diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 19:09:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-23 19:50:55 +0100 |
| commit | 21750c40ee3f7ef3103121db68aef4339dceba40 (patch) | |
| tree | 0d431861ae07801be81224e6123f151a24c84d41 /vernac/lemmas.ml | |
| parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) | |
[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.
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |