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. --- kernel/environ.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index fb89576dd..2d6c9117b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -490,7 +490,7 @@ let lookup_projection cst env = Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - (lookup_constant cst env).const_proj + Cmap_env.mem cst env.env_globals.env_projections (* Mutual Inductives *) let polymorphic_ind (mind,i) env = -- cgit v1.2.3