universes are written with the URI inside objects, this allows

[helm.git] / helm / software / components / cic / cicParser.ml

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 0f36f1a04d8b2ab886eb3861d904469efec20511..e61ee78eabd1a8bed218b2d75d569e6a6bc53dd9 100644 (file)
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -311,11 +311,12 @@ let sort_of_string ctxt = function
       let len = String.length s in
       if not(len > 5) then parse_error ctxt "sort expected";
       if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
-      try 
-        Cic.Type 
-          (CicUniv.fresh 
-            ~uri:ctxt.uri 
-            ~id:(int_of_string (String.sub s 5 (len - 5))) ())
+      let s = String.sub s 5 (len - 5) in
+      let i = String.index s ':' in  
+      let id =  int_of_string (String.sub s 0 i) in
+      let suri = String.sub s (i+1) (len - 5 - i - 1) in
+      let uri = UriManager.uri_of_string suri in
+      try Cic.Type (CicUniv.fresh ~uri ~id ())
       with
       | Failure "int_of_string" 
       | Invalid_argument _ -> parse_error ctxt "sort expected"