diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f2e7cff8ec..36f1515a8c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -247,7 +247,7 @@ let get_opaque_body env cbo = type side_effect = { from_env : Declarations.structure_body CEphemeron.key; seff_constant : Constant.t; - seff_body : Declarations.constant_body; + seff_body : Opaqueproof.opaque Declarations.constant_body; seff_env : seff_env; seff_role : Entries.side_effect_role; } |