let fold_tac ~reduction ~also_in_hypotheses ~term =
let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
let curi,metasenv,pbo,pty = proof in
let fold_tac ~reduction ~also_in_hypotheses ~term =
let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
let curi,metasenv,pbo,pty = proof in