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. --- interp/dumpglob.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'interp/dumpglob.ml') diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 0197cf9ae..d7962e29a 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -68,6 +68,7 @@ let pause () = previous_state := !glob_output; glob_output := NoGlob let continue () = glob_output := !previous_state open Decl_kinds +open Declarations let type_of_logical_kind = function | IsDefinition def -> @@ -111,14 +112,12 @@ let type_of_global_ref gr = | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record <> None then - let open Decl_kinds in begin match mib.Declarations.mind_finite with | Finite -> "indrec" | BiFinite -> "rec" | CoFinite -> "corec" end else - let open Decl_kinds in begin match mib.Declarations.mind_finite with | Finite -> "ind" | BiFinite -> "variant" -- cgit v1.2.3