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/prettyp.ml | 4 ++-- printing/printmod.ml | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 647111bbe..2b7886d11 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -235,8 +235,8 @@ let print_type_in_type ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" - | Decl_kinds.BiFinite -> str " with eta conversion" + | CoFinite | Finite -> str" without eta conversion" + | BiFinite -> str " with eta conversion" in [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] 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