Moved Indmap and ConstrMap from Libnames to Names for use in Cooking

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6736 85f007b7-540e-0410-9357-904b9bb8a0f7

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