diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5c67c33b6a..68f832997c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -993,7 +993,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_typ (Lazyconstr.force_opaque c) + mk_typ (Lazyconstr.force_opaque (Future.force c)) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with @@ -1002,7 +1002,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_def (Lazyconstr.force_opaque c) + mk_def (Lazyconstr.force_opaque (Future.force c)) else mk_ax ()) let extract_constant_spec env kn cb = |