From 427e8cac2c267a7302b71979c0f1019598176e31 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Aug 2020 17:37:24 +0200
Subject: 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.
---
 kernel/safe_typing.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3