(* The default of term is the thesis of the goal to be prooved *)
let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
let curi,metasenv,pbo,pty = proof in
(* The default of term is the thesis of the goal to be prooved *)
let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
let curi,metasenv,pbo,pty = proof in