diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_subst.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 5f81ddb4da..75a167f6c5 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -527,10 +527,13 @@ let mp_in_key mp key = let subset_prefixed_by mp resolver = let prefixmp key hint resolv = - if mp_in_key mp key then - Deltamap.add key hint resolv - else - resolv + match hint with + | Inline _ -> resolv + | _ -> + if mp_in_key mp key then + Deltamap.add key hint resolv + else + resolv in Deltamap.fold prefixmp resolver empty_delta_resolver |