aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml12
1 files changed, 8 insertions, 4 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cdd698304..5aee70194 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1066,8 +1066,10 @@ let extract_constant env kn cb =
| Undef _ -> warn_info (); mk_typ_ax ()
| Def c ->
(match cb.const_proj with
- | None -> mk_typ (get_body c)
- | Some pb -> mk_typ (EConstr.of_constr pb.proj_body))
+ | false -> mk_typ (get_body c)
+ | true ->
+ let pb = lookup_projection (Projection.make kn false) env in
+ mk_typ (EConstr.of_constr pb.proj_body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_typ (get_opaque env c)
@@ -1077,8 +1079,10 @@ let extract_constant env kn cb =
| Undef _ -> warn_info (); mk_ax ()
| Def c ->
(match cb.const_proj with
- | None -> mk_def (get_body c)
- | Some pb -> mk_def (EConstr.of_constr pb.proj_body))
+ | false -> mk_def (get_body c)
+ | true ->
+ let pb = lookup_projection (Projection.make kn false) env in
+ mk_def (EConstr.of_constr pb.proj_body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_def (get_opaque env c)