diff options
| -rw-r--r-- | kernel/declareops.ml | 28 |
1 files changed, 12 insertions, 16 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index da945b67b7..518a40a6e7 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 } *) |