fun s ->
List.map uri_of_string (Str.split space_RE s)
+let impredicative_set = ref true;;
+
let sort_of_string ctxt = function
| "Prop" -> Cic.Prop
- | "Set" -> Cic.Set
| "CProp" -> Cic.CProp
(* 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 ())
+ | "Set" when !impredicative_set -> Cic.Set
+ | "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
| s ->
let len = String.length s in
if not(len > 5) then parse_error ctxt "sort expected";
| ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "def" -> (* same as "decl" above *)
- let ty = pop_cic ctxt in
- let source = pop_cic ctxt in
+ let ty,source =
+ (*CSC: hack to parse Coq files where the LetIn is not typed *)
+ let ty = pop_cic ctxt in
+ try
+ let source = pop_cic ctxt in
+ ty,source
+ with
+ Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty
+ in
push ctxt
(match pop_tag_attrs ctxt with
| ["binder", binder; "id", id]