aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/keys.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/keys.ml')
-rw-r--r--library/keys.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/library/keys.ml b/library/keys.ml
index 3d277476f..6b2466f3d 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -62,8 +62,6 @@ module Keyset = Keymap.Set
(* Mapping structure for references to be considered equivalent *)
-type keys = Keyset.t Keymap.t
-
let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
let add_kv k v m =