From e43710b391c278ac7fcb808ec28d720b4317660c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Jun 2018 15:26:20 +0200 Subject: Remove the proj_body field from the kernel. This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute. --- plugins/extraction/extraction.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index b1ee21536..3a61c7747 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1069,7 +1069,11 @@ let extract_constant env kn cb = | 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)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1082,7 +1086,11 @@ let extract_constant env kn cb = | 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)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) -- cgit v1.2.3