val proc_id: string ref
-val test: bool ref
+val check: bool ref
val no_types: bool ref
+val no_proofs: bool ref
+
val global_alpha: bool ref
val log_alpha: bool ref
val macro_gref: (string * string * int * int) list ref
+val sigs_gref: (string * int * int) list ref
+
val clear: unit -> unit
val close_list: unit -> unit