Move body_of_constant_body to Global and specialize its uses.

This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.

The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.

1 files changed, 11 insertions, 0 deletions

diff --git a/library/global.ml b/library/global.ml
index 58e2380440..827b062725 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -132,6 +132,17 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
 let opaque_tables () = Environ.opaque_tables (env ())
 
+let body_of_constant_body env cb =
+  let open Declarations in
+  let otab = Environ.opaque_tables env in
+  match cb.const_body with
+  | Undef _ | Primitive _ ->
+     None
+  | Def c ->
+     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+  | OpaqueDef o ->
+     Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
+
 let body_of_constant_body ce = body_of_constant_body (env ()) ce
 
 let body_of_constant cst = body_of_constant_body (lookup_constant cst)