let module R = CicReduction in
let module S = CicSubstitution in
let module PT = PrimitiveTactics in
- let _,metasenv,_subst,_,_, _ = proof in
+ let _,metasenv,_,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
hd::tl ->