aboutsummaryrefslogtreecommitdiff
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, 3 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 9802d4f531..b755ff0e08 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -675,6 +675,7 @@ module InductiveOrdered_env = struct
end
module Indset = Set.Make(InductiveOrdered)
+module Indset_env = Set.Make(InductiveOrdered_env)
module Indmap = Map.Make(InductiveOrdered)
module Indmap_env = Map.Make(InductiveOrdered_env)
@@ -688,6 +689,8 @@ module ConstructorOrdered_env = struct
let compare = constructor_user_ord
end
+module Constrset = Set.Make(ConstructorOrdered)
+module Constrset_env = Set.Make(ConstructorOrdered_env)
module Constrmap = Map.Make(ConstructorOrdered)
module Constrmap_env = Map.Make(ConstructorOrdered_env)