Partial revert of r16711

 It seems that it's critical for the native compiler that
 a fresh (ref NotLinked) is created during substitution.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16719 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 16 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index da945b67b..518a40a6e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -55,22 +55,18 @@ let subst_const_def sub def = match def with
   | OpaqueDef lc ->
     OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
 
-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_native_name = ref NotLinked;
-        const_inline_code = cb.const_inline_code }
+(* 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_native_name = ref NotLinked;
+  const_inline_code = cb.const_inline_code }
 
 (** {7 Hash-consing of constants } *)