diff options
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index af6992252..58465849c 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -719,7 +719,7 @@ let compile env c = let compile_constant_body env = function | Undef _ | OpaqueDef _ -> BCconstant | Def sb -> - let body = Lazyconstr.force sb in + let body = Mod_subst.force_constr sb in match kind_of_term body with | Const kn' -> (* we use the canonical name of the constant*) |