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.

4 files changed, 30 insertions, 15 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d908bcbe2..4f1672884 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 } *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d99382129..e13fb4f08 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -298,9 +298,9 @@ let join_constant_body otab cb =
   | _ -> ()
 
 let string_of_side_effect = function
-  | SEsubproof (c,_) -> Names.string_of_con c
+  | SEsubproof (c,_,_) -> Names.string_of_con c
   | SEscheme (cl,_) ->
-      String.concat ", " (List.map (fun (_,c,_) -> Names.string_of_con c) cl)
+      String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl)
 type side_effects = side_effect list
 let no_seff = ([] : side_effects)
 let iter_side_effects f l = List.iter f (List.rev l)
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
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 415e91f70..8f41f356d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -49,9 +49,9 @@ let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
 let handle_side_effects env body side_eff =
   let handle_sideff t se =
     let cbl = match se with
-      | SEsubproof (c,cb) -> [c,cb]
-      | SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl in
-    let not_exists (c,_) =
+      | SEsubproof (c,cb,b) -> [c,cb,b]
+      | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
+    let not_exists (c,_,_) =
       try ignore(Environ.lookup_constant c env); false
       with Not_found -> true in 
     let cbl = List.filter not_exists cbl in
@@ -72,10 +72,9 @@ let handle_side_effects env body side_eff =
 	(*   Vars.subst_univs_level_constr subst b *)
 	Vars.subst_instance_constr u' b
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
-    let fix_body (c,cb) t =
-      match cb.const_body with
-      | Undef _ -> assert false
-      | Def b ->
+    let fix_body (c,cb,b) t =
+      match cb.const_body, b with
+      | Def b, _ ->
           let b = Mod_subst.force_constr b in
 	  let poly = cb.const_polymorphic in
 	    if not poly then
@@ -85,8 +84,7 @@ let handle_side_effects env body side_eff =
 	    else 
 	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
-      | OpaqueDef b -> 
-          let b = Opaqueproof.force_proof (opaque_tables env) b in
+      | OpaqueDef _, `Opaque (b,_) -> 
 	  let poly = cb.const_polymorphic in
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
@@ -95,6 +93,7 @@ let handle_side_effects env body side_eff =
 	    else
 	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+      | _ -> assert false
     in
       List.fold_right fix_body cbl t
   in