diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_subst.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f32198f800..668f2d412e 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -295,7 +295,9 @@ let subst_con0 sub con = let dup con = con, mkConst con in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with - | Some t -> con', t + | Some t -> + (* In case of inlining, discard the canonical part (cf #2608) *) + constant_of_kn (user_con con'), t | None -> let con'' = match side with | User -> constant_of_delta resolve con' |