diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 051d1f8e0f..8c505eb202 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -115,7 +115,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr) let get_opaque env c = EConstr.of_constr - (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c) + (fst (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c)) let applistc c args = EConstr.mkApp (c, Array.of_list args) |