From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 10 Jul 2017 19:11:20 +0200
Subject: Safe API for accessing universe constraints of global references.

Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
---
 vernac/obligations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/obligations.ml')

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0acdaf57..5a1c260b1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -362,7 +362,7 @@ let get_body obl =
   match obl.obl_body with
   | None -> None
   | Some (DefinedObl c) ->
-    let u = Environ.constant_instance (Global.env ()) c in
+    let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in
     let pc = (c, u) in
       Some (DefinedObl pc)
   | Some (TermObl c) ->
-- 
cgit v1.2.3