diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 17 | ||||
| -rw-r--r-- | kernel/names.mli | 2 |
2 files changed, 18 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index e15d4ab2f7..a2c41beb75 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -183,7 +183,6 @@ module Cmap = KNmap module Cpred = KNpred module Cset = KNset - let default_module_name = id_of_string "If you see this, it's a bug" let initial_dir = make_dirpath [default_module_name] @@ -210,6 +209,22 @@ let ith_constructor_of_inductive ind i = (ind,i) let inductive_of_constructor (ind,i) = ind let index_of_constructor (ind,i) = i +module InductiveOrdered = struct + type t = inductive + let compare (spx,ix) (spy,iy) = + let c = ix - iy in if c = 0 then KNord.compare spx spy else c +end + +module Indmap = Map.Make(InductiveOrdered) + +module ConstructorOrdered = struct + type t = constructor + let compare (indx,ix) (indy,iy) = + let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c +end + +module Constrmap = Map.Make(ConstructorOrdered) + (* Better to have it here that in closure, since used in grammar.cma *) type evaluable_global_reference = | EvalVarRef of identifier diff --git a/kernel/names.mli b/kernel/names.mli index 4350b231aa..0e65b65b40 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -123,6 +123,8 @@ type constructor = inductive * int module Cmap : Map.S with type key = constant module Cpred : Predicate.S with type elt = constant module Cset : Set.S with type elt = constant +module Indmap : Map.S with type key = inductive +module Constrmap : Map.S with type key = constructor val constant_of_kn : kernel_name -> constant val make_con : module_path -> dir_path -> label -> constant |