4 files changed, 19 insertions, 18 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 -> ()
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 05f342a82a..c47bde0864 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -483,16 +483,6 @@ let constant_value_and_type env (kn, u) =
   in
   b', subst_instance_constr u cb.const_type, cst
 
-let body_of_constant_body env cb =
-  let otab = 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)
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f6cd41861e..2abcea148a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses ->
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
 
-(** Returns the body of the constant if it has any, and the polymorphic context
-    it lives in. For monomorphic constant, the latter is empty, and for
-    polymorphic constants, the term contains De Bruijn universe variables that
-    need to be instantiated. *)
-val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
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)