From 9938aed874d3e15e5d21689ea841bdc3e6ebb40e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 11 Jul 2017 21:51:23 +0200
Subject: Safer API for Global.body_of_constant and variants.

We aditionally return the abstract universe context inside the option. This
is relatively painless as most uses were using the option as a boolean.
---
 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 a1cb81242..c12fa9479 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -132,7 +132,7 @@ let compute_head = function
    in
      (match body with
      | None -> RigidHead (RigidParameter cst)
-     | Some c -> kind_of_head env c)
+     | Some (c, _) -> kind_of_head env c)
 | EvalVarRef id ->
     (match Global.lookup_named id with
      | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
-- 
cgit v1.2.3