From 9938aed874d3e15e5d21689ea841bdc3e6ebb40e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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.
---
 stm/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index fd3d418c10..d38491fec2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1576,8 +1576,9 @@ end = struct (* {{{ *)
         let uc =
           Option.get
             (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
         let pr =
-          Future.from_val (Option.get (Global.body_of_constant_body c)) in
+          Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
         let uc =
           Future.chain
             ~pure:true uc Univ.hcons_universe_context_set in
-- 
cgit v1.2.3