(* interface ****************************************************************)
let dno_id = "_" (* identifier for not-occurring premises *)
(* interface ****************************************************************)
let dno_id = "_" (* identifier for not-occurring premises *)
alpha_type := default_alpha;
alpha_sort := default_alpha;
alpha_gref := default_alpha;
alpha_type := default_alpha;
alpha_sort := default_alpha;
alpha_gref := default_alpha;