let set = function
    | Dep -> proofmode := Dep
    | No -> proofmode := No