diff options
| author | Pierre-Marie Pédrot | 2019-05-15 23:50:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-19 13:14:19 +0200 |
| commit | 801aed67a90ec49c15a4469e1905aa2835fabe19 (patch) | |
| tree | 9da139e5e0e5ecd8ba74806d2baa1225cee2e720 /kernel/safe_typing.ml | |
| parent | 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d (diff) | |
Parameterize the constant_body type by opaque subproofs.
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; } |