From 81492757797caef50d4eb3eb185f813463da883d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 7 Jan 2014 10:24:12 +0100
Subject: STM: additional fix for STM + vm_compute

Thanks again Maximes.

This time the C value was stored in the env_(named|rel)_val of
the environment
---
 pretyping/evarutil.ml | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 7378467661..8e3057e8e7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -495,13 +495,17 @@ let clear_hyps_in_evi evdref hyps concl ids =
     let check_value vk =
       match !vk with
 	| VKnone -> vk
-	| VKvalue (v,d) ->
-	    if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
-	      (* v does depend on any of ids, it's ok *)
-	      vk
-	    else
-	      (* v depends on one of the cleared hyps: we forget the computed value *)
-	      ref VKnone
+	| VKvalue key ->
+            try
+              let _, d = Ephemeron.get key in
+	      if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
+	        (* v does depend on any of ids, it's ok *)
+	        vk
+	      else
+	        (* v depends on one of the cleared hyps:
+                   we forget the computed value *)
+	        ref VKnone
+            with Ephemeron.InvalidKey -> ref VKnone
     in
       remove_hyps ids check_context check_value hyps
   in
-- 
cgit v1.2.3