Merge PR #11481: Do not rely on Libobject for the current environment in extraction.

Reviewed-by: maximedenes

3 files changed, 5 insertions, 36 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f6f2058c13..e8adde2605 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -321,6 +321,8 @@ let universes_of_private eff =
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
+let structure_body_of_safe_env env = env.revstruct
+
 let sections_of_safe_env senv = senv.sections
 
 let get_section = function
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 92bbd264fa..e6f2fc4a5d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env
 
 val sections_of_safe_env : safe_environment -> section_data Section.t option
 
+val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2dc3e8a934..853be82eb8 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -26,43 +26,8 @@ open Common
 (*S Part I: computing Coq environment. *)
 (***************************************)
 
-(* FIXME: this is a Libobject hack that should be removed. *)
-module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end)
-
-let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
-| f -> f o
-| exception Not_found -> None
-
 let toplevel_env () =
-  let get_reference = function
-  | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
-    let mp,l = KerName.repr kn in
-    let handler =
-      DynHandle.add Declare.Internal.objConstant begin fun _ ->
-        let constant = Global.lookup_constant (Constant.make1 kn) in
-        Some (l, SFBconst constant)
-      end @@
-      DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
-        let inductive = Global.lookup_mind (MutInd.make1 kn) in
-        Some (l, SFBmind inductive)
-      end @@
-      DynHandle.empty
-    in
-    handle handler o
-    | (_,kn), Lib.Leaf Libobject.ModuleObject _ ->
-      let mp,l = KerName.repr kn in
-      let modl = Global.lookup_module (MPdot (mp, l)) in
-      Some (l, SFBmodule modl)
-    | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ ->
-      let mp,l = KerName.repr kn in
-      let modtype = Global.lookup_modtype (MPdot (mp, l)) in
-      Some (l, SFBmodtype modtype)
-    | (_,kn), Lib.Leaf Libobject.IncludeObject _ ->
-      user_err Pp.(str "No extraction of toplevel Include yet.")
-    | _ -> None
-  in
-  List.rev (List.map_filter get_reference (Lib.contents ()))
-
+  List.rev (Safe_typing.structure_body_of_safe_env (Global.safe_env ()))
 
 let environment_until dir_opt =
   let rec parse = function