aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 047a1d6525..39cd4548f5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -671,6 +671,7 @@ module InductiveOrdered_env = struct
let compare = ind_user_ord
end
+module Indset = Set.Make(InductiveOrdered)
module Indmap = Map.Make(InductiveOrdered)
module Indmap_env = Map.Make(InductiveOrdered_env)