From 9316e4227311720e33e0b002b57626312d7d1245 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Jan 2020 09:36:08 +0100
Subject: Do not rely on Libobject for the current environment in extraction.

Instead, we export in Safe_typing the current module declaration.
---
 kernel/safe_typing.ml  | 2 ++
 kernel/safe_typing.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3