From 91df402729f70144a4e4d198c4384dc515920e59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 11 Jul 2017 15:42:43 +0200
Subject: Moving the last bits of abtraction-breaking code out of the kernel.

---
 library/heads.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/heads.ml')

diff --git a/library/heads.ml b/library/heads.ml
index 0f420c0e6..a1cb81242 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -128,7 +128,7 @@ let compute_head = function
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
      if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
-     then Declareops.body_of_constant (Environ.opaque_tables env) cb else None 
+     then Global.body_of_constant cst else None
    in
      (match body with
      | None -> RigidHead (RigidParameter cst)
-- 
cgit v1.2.3