From d782dabc61251834e35a77c43e070ea8b4e0b04a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 21:59:18 +0200
Subject: Centralize the hashconsing of constant declarations.

Safe_typing is now responsible for hashconsing of all accessible structures,
except for opaque terms which are handled by Opaqueproof.
---
 kernel/safe_typing.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 873cc2a172..eb03854af4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -555,6 +555,8 @@ let add_constant_aux ~in_section senv (kn, cb) =
     end
   | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
   in
+  (* This is the only place where we hashcons the contents of a constant body *)
+  let cb = if in_section then cb else Declareops.hcons_const_body cb in
   let cb, otab = match cb.const_body with
     | OpaqueDef lc when not in_section ->
       (* In coqc, opaque constants outside sections will be stored
@@ -771,8 +773,7 @@ let export_private_constants ~in_section ce senv =
 
 let add_recipe ~in_section l r senv =
   let kn = Constant.make2 senv.modpath l in
-  let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
-  let cb = if in_section then cb else Declareops.hcons_const_body cb in
+  let cb = Term_typing.translate_recipe senv.env kn r in
   let senv = add_constant_aux ~in_section senv (kn, cb) in
   kn, senv
 
-- 
cgit v1.2.3