From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 library/heads.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'library/heads.ml')

diff --git a/library/heads.ml b/library/heads.ml
index 8124d347..02465f22 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -15,6 +15,7 @@ open Environ
 open Globnames
 open Libobject
 open Lib
+open Context.Named.Declaration
 
 (** Characterization of the head of a term *)
 
@@ -63,13 +64,13 @@ let kind_of_head env t =
       (try on_subterm k l b (variable_head id)
        with Not_found ->
         (* a goal variable *)
-        match pi2 (lookup_named id env) with
-        | Some c -> aux k l c b
-        | None -> NotImmediatelyComputableHead)
+        match lookup_named id env with
+        | LocalDef (_,c,_) -> aux k l c b
+        | LocalAssum _ -> NotImmediatelyComputableHead)
   | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
        with Not_found ->
-         Errors.anomaly
+         CErrors.anomaly
            Pp.(str "constant not found in kind_of_head: " ++
                str (Names.Constant.to_string cst)))
   | Construct _ | CoFix _ ->
@@ -132,8 +133,8 @@ let compute_head = function
      | None -> RigidHead (RigidParameter cst)
      | Some c -> kind_of_head env c)
 | EvalVarRef id ->
-    (match pi2 (Global.lookup_named id) with
-     | Some c when not (Decls.variable_opacity id) ->
+    (match Global.lookup_named id with
+     | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
            kind_of_head (Global.env()) c
      | _ ->
            RigidHead (RigidVar id))
-- 
cgit v1.2.3