From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 6 Nov 2017 23:27:09 +0100
Subject: [api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.
---
 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 d2cfc0990..8b8e407f7 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open Constr
 open Vars
 open Mod_subst
 open Environ
@@ -57,7 +58,7 @@ let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
 let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
 
 let kind_of_head env t =
-  let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta env t) with
+  let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with
   | Rel n when n > k -> NotImmediatelyComputableHead
   | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
   | Var id ->
-- 
cgit v1.2.3