From 6e9a1c4c71f58aba8bb0bb5942c5063a5984a1bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 9 Jul 2014 17:47:50 +0200
Subject: Fixing the previous patch to keep transparent states in sync.

---
 kernel/conv_oracle.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/conv_oracle.ml')

diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 6e4119f28..99849fc7a 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -58,7 +58,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
     in
     let var_trstate = match l with
     | Opaque -> Id.Pred.remove id oracle.var_trstate
-    | _ -> oracle.var_trstate
+    | _ -> Id.Pred.add id oracle.var_trstate
     in
     { oracle with var_opacity; var_trstate; }
   | ConstKey c ->
@@ -68,7 +68,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
     in
     let cst_trstate = match l with
     | Opaque -> Cpred.remove c oracle.cst_trstate
-    | _ -> oracle.cst_trstate
+    | _ -> Cpred.add c oracle.cst_trstate
     in
     { oracle with cst_opacity; cst_trstate; }
   | RelKey _ -> Errors.error "set_strategy: RelKey"
-- 
cgit v1.2.3