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