(* interface ****************************************************************)
let dno_id = "_" (* identifier for not-occurring premises *)
(* interface ****************************************************************)
let dno_id = "_" (* identifier for not-occurring premises *)
let global_alpha = ref default_global_alpha (* log alpha-unconverted identifiers *)
let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *)
let global_alpha = ref default_global_alpha (* log alpha-unconverted identifiers *)
let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *)
no_init := default_no_init;
out_dir := default_out_dir;
proc_id := default_proc_id;
no_init := default_no_init;
out_dir := default_out_dir;
proc_id := default_proc_id;
global_alpha := default_global_alpha;
log_alpha := default_log_alpha;
log_missing := default_log_missing;
global_alpha := default_global_alpha;
log_alpha := default_log_alpha;
log_missing := default_log_missing;
alpha_type := default_alpha;
alpha_sort := default_alpha;
alpha_gref := default_alpha;
alpha_type := default_alpha;
alpha_sort := default_alpha;
alpha_gref := default_alpha;