From a4839aa1ff076a8938ca182615a93d6afe748860 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Jun 2018 13:32:35 +0200
Subject: Remove the proj_eta field of the kernel.

This field was not used inside the kernel and not used in
performance-critical code where caching is essential, so we extrude
the code that computes it out of the kernel.
---
 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 02871153b0..abebec156c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,7 +54,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
-  proj_eta : constr * types; (* Eta-expanded term and type *)
   proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
-- 
cgit v1.2.3