From 8c417a6d32e379d9642d6f2ef144f33d7df4832e Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 18 Feb 2005 22:15:17 +0000
Subject: Standardisation of constr_of_reference into constr_of_global + Moved
 Indmap and ConstrMap to Names

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6747 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/libnames.ml  | 30 +++++++++---------------------
 library/libnames.mli |  6 +++---
 2 files changed, 12 insertions(+), 24 deletions(-)

(limited to 'library')

diff --git a/library/libnames.ml b/library/libnames.ml
index f21b98698..361c01696 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -27,11 +27,12 @@ let subst_global subst ref = match ref with
      let kn',t = subst_con subst kn in
       if kn==kn' then ref, mkConst kn else ConstRef kn', t
   | IndRef (kn,i) ->
-      let kn' = subst_kn subst kn in if kn==kn' then ref, mkInd (kn,i) else
-          IndRef(kn',i), mkInd (kn',i)
+      let kn' = subst_kn subst kn in
+      if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
   | ConstructRef ((kn,i),j) ->
-      let kn' = subst_kn subst kn in if kn==kn' then ref, mkConstruct ((kn,i),j)
-          else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j)
+      let kn' = subst_kn subst kn in 
+      if kn==kn' then ref, mkConstruct ((kn,i),j)
+      else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j)
 
 let reference_of_constr c = match kind_of_term c with
   | Const sp -> ConstRef sp
@@ -40,12 +41,14 @@ let reference_of_constr c = match kind_of_term c with
   | Var id -> VarRef id
   |  _ -> raise Not_found
 
-let constr_of_reference = function
+let constr_of_global = function
   | VarRef id -> mkVar id
   | ConstRef sp -> mkConst sp
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
+let constr_of_reference = constr_of_global
+
 module RefOrdered =
   struct
     type t = global_reference
@@ -55,24 +58,8 @@ module RefOrdered =
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
 
-module InductiveOrdered = struct
-  type t = inductive
-  let compare (spx,ix) (spy,iy) = 
-    let c = ix - iy in if c = 0 then compare spx spy else c
-end
-
-module Indmap = Map.Make(InductiveOrdered)
-
 let inductives_table = ref Indmap.empty
 
-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)
-
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
@@ -267,3 +254,4 @@ let pr_reference = function
 let loc_of_reference = function
   | Qualid (loc,qid) -> loc
   | Ident (loc,id) -> loc
+
diff --git a/library/libnames.mli b/library/libnames.mli
index 8d4ba269d..43e31d08f 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -26,6 +26,9 @@ type global_reference =
 val subst_global : substitution -> global_reference -> global_reference * constr
 
 (* Turn a global reference into a construction *)
+val constr_of_global : global_reference -> constr
+
+(* Obsolete synonym for constr_of_global *)
 val constr_of_reference : global_reference -> constr
 
 (* Turn a construction denoting a global into a reference;
@@ -35,9 +38,6 @@ val reference_of_constr : constr -> global_reference
 module Refset : Set.S with type elt = global_reference 
 module Refmap : Map.S with type key = global_reference
 
-module Indmap : Map.S with type key = inductive
-module Constrmap : Map.S with type key = constructor
-
 (*s Dirpaths *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
-- 
cgit v1.2.3