From 74d700e9f7fcb14e7136e87b5efab25d5adb194b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/declarations.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd70c050..02871153b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,7 +87,6 @@ type constant_body = {
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
-    const_proj : bool;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
-- 
cgit v1.2.3