From 74d700e9f7fcb14e7136e87b5efab25d5adb194b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Jun 2018 16:23:29 +0200 Subject: Getting rid of the const_proj field in the kernel. This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless. --- plugins/extraction/extraction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5aee70194..b1ee21536 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1065,7 +1065,7 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_typ (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in @@ -1078,7 +1078,7 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_def (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in -- cgit v1.2.3