proofs/pfedit.mli


1
2
3
4
5
6
7
8
9
10


(* $Id$ *)

(*i*)
open Pp
(*i*)

val proof_prompt : unit -> string
val refining : unit -> bool
val msg_proofs : bool -> std_ppcmds