Drop opaque bodies of abstracted definitions.

This should save us a lot of useless hashconsing. This change should not be
observable because outside of the proof, the abstracted definition will be
either inlined or redefined with the body coming from the side-effect.

1 files changed, 8 insertions, 6 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b85072d6d..da77a2882e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -936,12 +936,14 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e
       | DefinitionEff ce ->
         Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce)
     in
-  let senv, dcb = match cb.const_body with
-  | Def _ as const_body -> senv, { cb with const_body }
-  | OpaqueDef c ->
-    let local = empty_private cb.const_universes in
-    let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in
-    senv, { cb with const_body = OpaqueDef o }
+  let dcb = match cb.const_body with
+  | Def _ as const_body -> { cb with const_body }
+  | OpaqueDef _ ->
+    (* We drop the body, to save the definition of an opaque and thus its
+       hashconsing. It does not matter since this only happens inside a proof,
+       and depending of the opaque status of the latter, this proof term will be
+       either inlined or reexported. *)
+    { cb with const_body = Undef None }
   | Undef _ | Primitive _ -> assert false
   in
   let senv = add_constant_aux senv (kn, dcb) in