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, 8 insertions, 2 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1dd16f1630..a3f151ef86 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -29,10 +29,16 @@ let check_constant_declaration env kn cb =
   in
   let ty = cb.const_type in
   let _ = infer_type env' ty in
+  let otab = Environ.opaque_tables env in
+  let body = match cb.const_body with
+  | Undef _ | Primitive _ -> None
+  | Def c -> Some (Mod_subst.force_constr c)
+  | OpaqueDef o -> Some (Opaqueproof.force_proof otab o)
+  in
   let () =
-    match Environ.body_of_constant_body env cb with
+    match body with
     | Some bd ->
-      let j = infer env' (fst bd) in
+      let j = infer env' bd in
       (try conv_leq env' j.uj_type ty
        with NotConvertible -> Type_errors.error_actual_type env j ty)
     | None -> ()