From 085cfc8bc4f775e8879a31c6de35d08aed500332 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 5 Feb 2008 15:23:08 +0000
Subject: [PATCH] uri -> reference (2)

---
 helm/software/components/ng_kernel/.depend       |  8 +++-----
 helm/software/components/ng_kernel/Makefile      |  2 +-
 .../components/ng_kernel/nCicEnvironment.ml      |  4 ++--
 .../components/ng_kernel/nCicEnvironment.mli     |  2 +-
 .../ng_kernel/{nUriManager.ml => nReference.ml}  | 16 ++++++++--------
 .../{nUriManager.mli => nReference.mli}          |  0
 6 files changed, 15 insertions(+), 17 deletions(-)
 rename helm/software/components/ng_kernel/{nUriManager.ml => nReference.ml} (88%)
 rename helm/software/components/ng_kernel/{nUriManager.mli => nReference.mli} (100%)

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index 960471d4e..497730e2b 100644
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -1,14 +1,12 @@
-nCicEnvironment.cmi: nUriManager.cmi nCic.cmo 
+nCicEnvironment.cmi: nReference.cmi nCic.cmo 
 nCicTypeChecker.cmi: nCic.cmo 
 oCic2NCic.cmi: nCic.cmo 
-nCic.cmo: nUriManager.cmi 
-nCic.cmx: nUriManager.cmx 
 nCicEnvironment.cmo: oCic2NCic.cmi nCicEnvironment.cmi 
 nCicEnvironment.cmx: oCic2NCic.cmx nCicEnvironment.cmi 
 nCicTypeChecker.cmo: nCicTypeChecker.cmi 
 nCicTypeChecker.cmx: nCicTypeChecker.cmi 
-nUriManager.cmo: nUriManager.cmi 
-nUriManager.cmx: nUriManager.cmi 
+nReference.cmo: nReference.cmi 
+nReference.cmx: nReference.cmi 
 oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi 
 oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi 
 oCic2NCic.cmo: oCic2NCic.cmi 
diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile
index 143fefa1a..209170288 100644
--- a/helm/software/components/ng_kernel/Makefile
+++ b/helm/software/components/ng_kernel/Makefile
@@ -2,7 +2,7 @@ PACKAGE = ng_kernel
 PREDICATES =
 
 INTERFACE_FILES = \
-	nCicEnvironment.mli nCicTypeChecker.mli nUriManager.mli oCicTypeChecker.mli oCic2NCic.mli
+	nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli
 IMPLEMENTATION_FILES = \
   nCic.ml $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL = 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 10d3c198d..278f7fff5 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -1,6 +1,6 @@
 
-let get_checked_obj nuri =
-  let ouri = NUriManager.ouri_of_nuri nuri in
+let get_checked_obj reference =
+  let ouri = NReference.ouri_of_reference reference in
   let o,_ = 
     CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph 
       ouri 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index d8b733dc3..20945d08d 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -26,6 +26,6 @@
 (* NG: minimal wrapper on the old cicEnvironment, should provide only the
  * functions strictly necessary to the typechecking algorithm *)
 
-val get_checked_obj : NUriManager.uri -> NCic.obj
+val get_checked_obj : NReference.reference -> NCic.obj
 
 (* EOF *)
diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nReference.ml
similarity index 88%
rename from helm/software/components/ng_kernel/nUriManager.ml
rename to helm/software/components/ng_kernel/nReference.ml
index 745f9359c..bcdd4713e 100644
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nReference.ml
@@ -37,7 +37,7 @@ type reference = Ref of int * string * spec
 
 let eq = (==);;
 
-let string_of_reference (Uri (_,s,_)) = s;;
+let string_of_reference (Ref (_,s,_)) = s;;
 
 module OrderedStrings =
  struct
@@ -81,14 +81,14 @@ fun s ->
         let dot = String.rindex s '.' in
         let suffix = String.sub s (dot+1) 3 in
         match suffix with
-        | "dec" -> Uri (c (), s, Decl)
-        | "def" -> Uri (c (), s, Def)
-        | "fix" -> let i,j = get2 s dot in Uri (c (), s, Fix (i,j))
-        | "cfx" -> let i = get1 s dot in Uri (c (), s, CoFix (i))
-        | "ind" -> let i = get1 s dot in Uri (c (), s, Ind (i))
-        | "con" -> let i,j = get2 s dot in Uri (c (), s, Con (i,j))
+        | "dec" -> Ref (c (), s, Decl)
+        | "def" -> Ref (c (), s, Def)
+        | "fix" -> let i,j = get2 s dot in Ref (c (), s, Fix (i,j))
+        | "cfx" -> let i = get1 s dot in Ref (c (), s, CoFix (i))
+        | "ind" -> let i = get1 s dot in Ref (c (), s, Ind (i))
+        | "con" -> let i,j = get2 s dot in Ref (c (), s, Con (i,j))
         | _ -> raise Not_found
-      with Not_found -> raise (IllFormedUri (lazy s))
+      with Not_found -> raise (IllFormedReference (lazy s))
     in
     set_of_reference := MapStringsToUri.add s new_reference !set_of_reference;
     new_reference
diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nReference.mli
similarity index 100%
rename from helm/software/components/ng_kernel/nUriManager.mli
rename to helm/software/components/ng_kernel/nReference.mli
-- 
2.39.2