let (curi,metasenv,proofbo,proofty) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty = CicReduction.whd context termty in
let (termty,metasenv',arguments,fresh_meta) =
ProofEngineHelpers.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in