X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=b2dc972925ac4e16a8c9ced43ec60bcd759b1120;hb=2cf2e883f91164ce614bdc86b5c5e2419b98f68d;hp=3ac27296dce78667cb9ec589b38ff6463dc84023;hpb=98fef490e55d1d780e8c0bb19de0218e08ae73b1;p=helm.git

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 3ac27296d..b2dc97292 100644
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -27,7 +27,7 @@ type manager = Quiet
 
 (* interface functions ******************************************************)
 
-let version_string = "Helena 0.8.2 M (June 2015)"
+let version_string = "Helena 0.8.3 M (June 2015)"
 
 let stage = ref 3            (* stage *)
 
@@ -37,6 +37,8 @@ let ct = ref 0               (* current trace level *)
 
 let summary = ref false      (* log summary information *)
 
+let export = ref false       (* export entities to XML *)
+
 let xdir = ref ""            (* directory for XML output *)
 
 let kernel = ref V3          (* kernel type *)
@@ -73,6 +75,8 @@ let last = ref max_int       (* end trace here *)
 
 let extended = ref false     (* extended applications *) 
 
+let infinity = ref false     (* use ∞-abstractions in contexts *) 
+
 let short = ref false        (* short global constants *) 
 
 let set_current_trace n =
@@ -96,8 +100,8 @@ let get_mk_uri () =
    fun s -> KF.concat bu (s ^ ".ld")
 
 let clear () =
-   stage := 3; trace := 0; summary := false; first := 0; last := max_int;
-   xdir := ""; kernel := V3; si := false; extended := false; cover := ""; 
+   stage := 3; trace := 0; summary := false; export := false; first := 0; last := max_int;
+   xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false; short := false;
    debug_parser := false; debug_lexer := false;
    manager_dir := ""; manager := Quiet