let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let absurd_URI =
match LibraryObjects.absurd_URI () with