Revert "Partial revert of r16711"

The sharing introduced by this commit is now correct, since a reference used by
the native compiler has been removed from constant_body.

This reverts commit 413f5fcd4bf581ff3ea4694c193d637589c7d54f.

1 files changed, 15 insertions, 11 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 2e691491a..e40441d74 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -55,17 +55,21 @@ let subst_const_def sub def = match def with
   | OpaqueDef lc ->
       OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
 
-(* TODO : the native compiler seems to rely on a fresh (ref NotLinked)
-   being created at each substitution. Quite ugly... For the moment,
-   do not try to be clever here with memory sharing :-( *)
-
-let subst_const_body sub cb = {
-  const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
-  const_body = subst_const_def sub cb.const_body;
-  const_type = subst_const_type sub cb.const_type;
-  const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
-  const_constraints = cb.const_constraints;
-  const_inline_code = cb.const_inline_code }
+let subst_const_body sub cb =
+  assert (List.is_empty cb.const_hyps); (* we're outside sections *)
+  if is_empty_subst sub then cb
+  else
+    let body' = subst_const_def sub cb.const_body in
+    let type' = subst_const_type sub cb.const_type in
+    if body' == cb.const_body && type' == cb.const_type then cb
+    else
+      { const_hyps = [];
+        const_body = body';
+        const_type = type';
+        const_body_code =
+          Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+        const_constraints = cb.const_constraints;
+        const_inline_code = cb.const_inline_code }
 
 (** {7 Hash-consing of constants } *)