aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/closure.ml')
-rw-r--r--kernel/closure.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 078f46b8d..c3b828a39 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -52,10 +52,6 @@ let with_stats c =
end else
Lazy.force c
-type evaluable_global_reference =
- | EvalVarRef of identifier
- | EvalConstRef of constant
-
type transparent_state = Idpred.t * KNpred.t
let all_opaque = (Idpred.empty, KNpred.empty)