aboutsummaryrefslogtreecommitdiff
path: root/kernel/conv_oracle.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-11-20 08:42:52 +0100
committerMaxime Dénès2018-11-20 08:42:52 +0100
commit4d26550af26c1dab464253cc470e8a876fee0025 (patch)
treef2594e7e0b7960c50d45d6cb2e782eb074d19150 /kernel/conv_oracle.ml
parent22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (diff)
parent4acdbe9be526dc7f646ab084e52fe4b9a6ad1399 (diff)
Merge PR #7925: Clean transparent state
Diffstat (limited to 'kernel/conv_oracle.ml')
-rw-r--r--kernel/conv_oracle.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index ac78064235..fe82353b70 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -81,7 +81,8 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
let accu = Id.Map.fold fvar var_opacity accu in
Cmap.fold fcst cst_opacity accu
-let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
+let get_transp_state { var_trstate; cst_trstate; _ } =
+ { TransparentState.tr_var = var_trstate; tr_cst = cst_trstate }
let dep_order l2r k1 k2 = match k1, k2 with
| RelKey _, RelKey _ -> l2r