merged the proofgen3 branch into trunk: