aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cClosure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cClosure.ml')
-rw-r--r--kernel/cClosure.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 7ed965b4c..219ea5b24 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -91,6 +91,7 @@ module type RedFlagsSig = sig
val red_add : reds -> red_kind -> reds
val red_sub : reds -> red_kind -> reds
val red_add_transparent : reds -> transparent_state -> reds
+ val red_transparent : reds -> transparent_state
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
val red_projection : reds -> projection -> bool
@@ -164,6 +165,8 @@ module RedFlags = (struct
let (l1,l2) = red.r_const in
{ red with r_const = Id.Pred.remove id l1, l2 }
+ let red_transparent red = red.r_const
+
let red_add_transparent red tr =
{ red with r_const = tr }