diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -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 c6bb9faa0..6fc1973d0 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -999,7 +999,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_typ (Lazyconstr.force_opaque (Future.force c)) + mk_typ (Lazyconstr.force_opaque c) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with @@ -1008,7 +1008,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_def (Lazyconstr.force_opaque (Future.force c)) + mk_def (Lazyconstr.force_opaque c) else mk_ax ()) let extract_constant_spec env kn cb = |