One Obj.magic implemented, trust changed to false.

[helm.git] / helm / software / components / ng_kernel / nUriManager.mli

diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli
index 9823719c38e191a05167298451a339188afafe49..ae8f793e66374a80c1530a41c1c77b6b30e8b2d8 100644 (file)
--- a/helm/software/components/ng_kernel/nUriManager.mli
+++ b/helm/software/components/ng_kernel/nUriManager.mli
@@ -23,14 +23,22 @@
  * 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
+exception IllFormedUri of string Lazy.t
+
+type spec = 
+ | Decl 
+ | Def
+ | Fix of int * int (* fixno, recparamno *)
+ | CoFix of int
+ | Ind of int
+ | Con of int * int (* indtyno, constrno *)
+
+type uri = Uri of int *  string * spec
 
 val eq: uri -> uri -> bool
 val string_of_uri: uri -> string 
 
 
 (* CACCA *)
-val nuri_of_ouri: UriManager.uri -> (int * int option ) option -> uri
+val nuri_of_ouri: UriManager.uri -> spec ->  uri
 val ouri_of_nuri: uri -> UriManager.uri