let of_string = function
    | "no" -> No
    | "dep" -> Dep
    | str -> raise (Invalid_argument(str ^ " : no such proof mode"))