let name,ty =
match defs with
| ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
- | ((Cic.Name name,None),_,_) :: _ ->
- fail loc ("No type given for " ^ name)
+ | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
| _ -> assert false
in
let body = CicAst.Ident (name,None) in