diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 11 |
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) |