From c7bd285555153294ec077cfa05c36bb420716f3b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 12 Apr 2018 21:41:03 +0200 Subject: Reduce circular dependency constants <-> projections Instead of having the projection data in the constant data we have it independently in the environment. --- plugins/extraction/extraction.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'plugins/extraction') 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) -- cgit v1.2.3