diff options
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index a7e8b0b26..e7859962e 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -723,7 +723,10 @@ let compile_constant_body env body opaque boxed = BCdefined(true, to_patch) else match kind_of_term body with - | Const kn' -> BCallias (get_allias env kn') + | Const kn' -> + (* we use the canonical name of the constant*) + let con= constant_of_kn (canonical_con kn') in + BCallias (get_allias env con) | _ -> let res = compile env body in let to_patch = to_memory res in |