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

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d993821293..e13fb4f088 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)
-- 
cgit v1.2.3