aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/closure.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/closure.mli')
-rw-r--r--checker/closure.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/checker/closure.mli b/checker/closure.mli
index a1a23c6cb..8556f26af 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -30,6 +30,9 @@ type transparent_state = Idpred.t * Cpred.t
val all_opaque : transparent_state
val all_transparent : transparent_state
+val is_transparent_variable : transparent_state -> variable -> bool
+val is_transparent_constant : transparent_state -> constant -> bool
+
(* Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds