let fake_constructor_tac ~n (proof, goal) =
let module C = Cic in
let module R = CicReduction in
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.MutInd (uri, typeno, exp_named_subst))