Cleaning and documenting a bit the Proofview.Refine module.