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.

1 files changed, 1 insertions, 1 deletions

diff --git a/library/heads.ml b/library/heads.ml
index 3d5f6a6ff..d9d650ac0 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -129,7 +129,7 @@ let compute_head = function
    let cb = Environ.lookup_constant cst env in
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
-     if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body
+     if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body
      then Global.body_of_constant cst else None
    in
      (match body with