| ["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]