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. --- printing/printmod.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'printing/printmod.ml') diff --git a/printing/printmod.ml b/printing/printmod.ml index 05292b06b..fb9d45a79 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -125,7 +125,7 @@ let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> "Inductive" | BiFinite -> "Variant" @@ -184,7 +184,7 @@ let print_record env mind mib udecl = (Array.to_list (Univ.Instance.to_array u)) udecl in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | BiFinite -> "Record" | Finite -> "Inductive" @@ -346,7 +346,7 @@ let print_body is_impl env mp (l,body) = pr_mutual_inductive_body env (MutInd.make2 mp l) mib None with e when CErrors.noncritical e -> let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> def "Inductive" | BiFinite -> def "Variant" -- cgit v1.2.3