aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-06-22 00:43:01 +0200
committerPierre-Marie Pédrot2018-11-19 13:29:55 +0100
commit96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 (patch)
tree9f54ad363b2c8f855be97860ba1900572353e164 /kernel/names.ml
parentecfbeaa62f9d8bd4dc4600cf39df2262af718313 (diff)
Move transparent_state to its own module.
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