From 44a5a0acb020be92ffe39209caf414b57c759139 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 15 May 2014 10:50:42 +0200
Subject: heads: avoid forcing opaque proofs

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

(limited to 'library/heads.ml')

diff --git a/library/heads.ml b/library/heads.ml
index 0faad827e..fa0393019 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -122,8 +122,9 @@ let compute_head = function
 | EvalConstRef cst ->
    let env = Global.env() in
    let cb = Environ.lookup_constant cst env in
+   let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
-     if cb.Declarations.const_proj = None 
+     if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
      then Declareops.body_of_constant cb else None 
    in
      (match body with
-- 
cgit v1.2.3