- if not(len > 5) then parse_error ctxt "sort expected";
- if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
- let s = String.sub s 5 (len - 5) in
+ let sort_len, mk_sort =
+ if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x
+ else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x
+ else parse_error ctxt "sort expected"
+ in
+ let s = String.sub s sort_len (len - sort_len) in