- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[helm.git] / helm / software / helena / src / common / options.ml

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 3ac27296dce78667cb9ec589b38ff6463dc84023..b2dc972925ac4e16a8c9ced43ec60bcd759b1120 100644 (file)
--- 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