let sort_of_string ctxt = function
| "Prop" -> Cic.Prop
| "Set" -> Cic.Set
- | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
-(* | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *)
| "CProp" -> Cic.CProp
- | _ -> parse_error ctxt "sort expected"
+ (* 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"
let patch_subst ctxt subst = function
| Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst)