X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Foptions.ml;h=b64fb605056972f34fb70a438216bd4c0ec17f7b;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hp=165b2d9784cce5310ccca448dd5207b1deab33ec;hpb=28e8954fbe2e28f01ae918c8d0e0ef34bd84b48f;p=helm.git

diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml
index 165b2d978..b64fb6050 100644
--- 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