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/term_typing.ml | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 415e91f706..8f41f356d5 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
-- 
cgit v1.2.3