- initial support for sigma-types

[helm.git] / matita / components / binaries / matex / options.ml

diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml
index 165b2d9784cce5310ccca448dd5207b1deab33ec..b64fb605056972f34fb70a438216bd4c0ec17f7b 100644 (file)
--- a/matita/components/binaries/matex/options.ml
+++ b/matita/components/binaries/matex/options.ml
@@ -40,6 +40,8 @@ let default_alpha = []
 
 let default_macro = []
 
+let default_sigs = []
+
 (* interface ****************************************************************)
 
 let dno_id = "_"                            (* identifier for not-occurring premises *)
@@ -76,6 +78,8 @@ let alpha_gref = ref default_alpha          (* data for constant renaming *)
 
 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
 
@@ -98,4 +102,5 @@ let clear () =
    alpha_type := default_alpha;
    alpha_sort := default_alpha;
    alpha_gref := default_alpha;
-   macro_gref := default_macro
+   macro_gref := default_macro;
+   sigs_gref := default_sigs