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/comInductive.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/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 |