aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml7
1 files changed, 0 insertions, 7 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 18560d5f8d..b2d6a489a6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -715,13 +715,6 @@ let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons
(*****************)
-type transparent_state = Id.Pred.t * Cpred.t
-
-let empty_transparent_state = (Id.Pred.empty, Cpred.empty)
-let full_transparent_state = (Id.Pred.full, Cpred.full)
-let var_full_transparent_state = (Id.Pred.full, Cpred.empty)
-let cst_full_transparent_state = (Id.Pred.empty, Cpred.full)
-
type 'a tableKey =
| ConstKey of 'a
| VarKey of Id.t