- (curi,metasenv',_subst,pbo,pty, attrs), [metano]
+ let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in
+ if with_cast then
+ let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in
+ let (newproof,_) =
+ let irl= CicMkImplicit.identity_relocation_list_for_metavariable context'
+ in
+ ProofEngineHelpers.subst_meta_in_proof
+ proof metano
+ (Cic.Cast (Cic.Meta(metano',irl),ty')) [metano',context',ty']
+ in
+ newproof, [metano']
+ else
+ proof,[goal]