]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nUriManager.mli
One Obj.magic implemented, trust changed to false.
[helm.git] / helm / software / components / ng_kernel / nUriManager.mli
index 911a1849b614a5b99c4f450f7b2cf9d8081675ae..ae8f793e66374a80c1530a41c1c77b6b30e8b2d8 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
+exception IllFormedUri of string Lazy.t
+
 type spec = 
  | Decl 
  | Def
  | Fix of int * int (* fixno, recparamno *)
  | CoFix of int
  | Ind of int
- | IConstr of int * int (* indtyno, constrno *)
+ | Con of int * int (* indtyno, constrno *)
 
 type uri = Uri of int *  string * spec
 
@@ -38,5 +40,5 @@ 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