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.

1 files changed, 16 insertions, 2 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9aca7727b..11079d25b 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