let default_macro = []
+let default_sigs = []
+
(* interface ****************************************************************)
let dno_id = "_" (* identifier for not-occurring premises *)
let macro_gref = ref default_macro (* data for eta-conversion and constant rendering *)
+let sigs_gref = ref default_sigs (* data for sigma-type rendering *)
+
let is_global_id s =
!global_alpha && s <> dno_id
alpha_type := default_alpha;
alpha_sort := default_alpha;
alpha_gref := default_alpha;
- macro_gref := default_macro
+ macro_gref := default_macro;
+ sigs_gref := default_sigs