aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 047d8a88d..3de12b1bc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -19,7 +19,6 @@
Élie Soubiran, ... *)
open Pp
-open Errors
open Util
(** {6 Identifiers } *)
@@ -485,8 +484,6 @@ module KerPair = struct
the same user part implies having the same canonical part
(invariant of the system). *)
- open Hashset.Combine
-
let hash = function
| Same kn -> KerName.hash kn
| Dual (kn, _) -> KerName.hash kn