From d9373d1ab9c84de43f212e11912178cabd5562ac Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 31 Jan 2008 15:06:31 +0000
Subject: [PATCH] new uri defined

---
 .../components/ng_kernel/nUriManager.ml       | 29 +++++++++++++------
 .../components/ng_kernel/nUriManager.mli      | 12 ++++++--
 2 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 95e3271b1..86cae6b6b 100644
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -23,18 +23,19 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*                order, uri,      (which, constructor)        *)
-type uri = Uri of int *  string *  (int  * int option ) option
+type spec = 
+ | Decl 
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | IConstr of int * int (* indtyno, constrno *)
+
+type uri = Uri of int *  string * spec
 
 let eq = (==);;
 
-let string_of_uri = function
-  | Uri (_,s,None) -> s
-  | Uri (_,s,Some (i,None)) -> 
-      s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ ")"
-  | Uri (_,s,Some (i, Some k)) -> 
-      s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ "/" ^ string_of_int (k+1) ^ ")"
-;;
+let string_of_uri (Uri (_,s,_)) = s ;;
 
 module OrderedStrings =
  struct
@@ -47,6 +48,16 @@ module MapStringsToUri = Map.Make(OrderedStrings);;
 
 let set_of_uri = ref MapStringsToUri.empty;;
 
+(* '.' not allowed in path and foo
+ *
+ * Decl                   cic:/path/foo.decl
+ * Def                    cic:/path/foo.def
+ * Fix of int * int       cic:/path/foo.fix(i,j)
+ * CoFix of int           cic:/path/foo.cofix(i)
+ * Ind of int             cic:/path/foo.ind(i)
+ * Constr of int * int    cic:/path/foo.constr(i,j)
+ *)
+
 let uri_of_string_aux =
   let counter = ref 0 in fun s ->
   incr counter;
diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli
index 9823719c3..911a1849b 100644
--- a/helm/software/components/ng_kernel/nUriManager.mli
+++ b/helm/software/components/ng_kernel/nUriManager.mli
@@ -23,9 +23,15 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*                        order, uri,      (which, constructor)        *)
-type spec = Normal of (int  * int option) option | 
-type uri = private Uri of int *  string * spec
+type spec = 
+ | Decl 
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | IConstr of int * int (* indtyno, constrno *)
+
+type uri = Uri of int *  string * spec
 
 val eq: uri -> uri -> bool
 val string_of_uri: uri -> string 
-- 
2.39.2