let uri = match uri with Some uri -> uri | None -> assert false in
let currentproof =
(*CSC: Wrong: [] is just plainly wrong *)
- Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])
in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof