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/global.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'library/global.ml')

diff --git a/library/global.ml b/library/global.ml
index cb6334c74..3a74f535d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -126,9 +126,8 @@ let opaque_tables () = Environ.opaque_tables (env ())
 let instantiate cb c =
   let open Declarations in
   match cb.const_universes with
-  | Monomorphic_const _ -> c
-  | Polymorphic_const ctx ->
-     Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
+  | Monomorphic_const _ -> c, Univ.AUContext.empty
+  | Polymorphic_const ctx -> c, ctx
 
 let body_of_constant_body cb =
   let open Declarations in
-- 
cgit v1.2.3