From bce50a4e984a4aaf4f6582f079d7c4bddf4d1ff8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 13 Oct 2014 16:33:28 +0200
Subject: STM: simplify how the term part of a side effect is retrieved

Now the seff contains it directly, no need to force the future
or to hope that it is a Direct opaque proof.
---
 kernel/declarations.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d908bcbe21..4f1672884f 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -76,9 +76,11 @@ type constant_body = {
     const_proj : projection_body option;
     const_inline_code : bool }
 
+type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
 type side_effect =
-  | SEsubproof of constant * constant_body
-  | SEscheme of (inductive * constant * constant_body) list * string
+  | SEsubproof of constant * constant_body * seff_env
+  | SEscheme of (inductive * constant * constant_body * seff_env) list * string
     
 (** {6 Representation of mutual inductive types in the kernel } *)
 
-- 
cgit v1.2.3