Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
- Cic2acic.acic_object_of_cic_object currentproof
+ Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
in
let xml, bodyxml =
match
C.Rel _ -> []
| C.Meta (n,_) -> [n]
| C.Sort _
- | C.Implicit -> []
+ | C.Implicit _ -> []
| C.Cast (te,ty) -> (aux te) @ (aux ty)
| C.Prod (_,s,t) -> (aux s) @ (aux t)
| C.Lambda (_,s,t) -> (aux s) @ (aux t)