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/safe_typing.ml | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9aca7727b1..11079d25b1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -195,10 +195,24 @@ let set_type_in_type senv =
 
 (** {6 Stm machinery } *)
 
-let sideff_of_con env c = SEsubproof (c, Environ.lookup_constant c env.env)
+let get_opauqe_body env cbo =
+  match cbo.const_body with
+  | Undef _ -> assert false
+  | Def _ -> `Nothing
+  | OpaqueDef opaque ->
+      `Opaque
+        (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
+         Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
+
+let sideff_of_con env c =
+  let cbo = Environ.lookup_constant c env.env in
+  SEsubproof (c, cbo, get_opauqe_body env.env cbo)
 let sideff_of_scheme kind env cl =
   SEscheme(
-    List.map (fun (i,c) -> i, c, Environ.lookup_constant c env.env) cl,kind)
+    List.map (fun (i,c) ->
+      let cbo = Environ.lookup_constant c env.env in
+      i, c, cbo, get_opauqe_body env.env cbo) cl,
+    kind)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
-- 
cgit v1.2.3