+ (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY
+ * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION
+ * IS FIXED *)
+ | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
+ | s ->
+ 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))) ())
+ with
+ | Failure "int_of_string"
+ | Invalid_argument _ -> parse_error ctxt "sort expected"