update in helena

[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 f268ba3443a138bd3decc13f1c217b70a969ba6d..71e55ececb796ea00dbfe30c05d5b51a696ee5e4 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -22,18 +22,20 @@ IFDEF MANAGER THEN
 type manager = Quiet
              | Coq
              | Matita
-             | LP1    (* newelpi *)
-             | LP2    (* newelpi *)
-             | TJ2    (* teyjus  *)
-             | TJ3    (* teyjus  *)
+             | LP1    (* elpi helena *)
+             | LP2    (* elpi helena *)
+             | TJ2    (* teyjus helena *)
+             | TJ3    (* teyjus helena *)
+             | CC0    (* elpi cic *)
+             | LYP    (* elpi lyp *)
 
 END
 
 (* interface functions ******************************************************)
 
 let version_string b =
-   if b then "Helena 0.8.3 M (December 2015)"
-   else "Helena 0.8.3 M - December 2015"
+   if b then "Helena 0.8.3 M (December 2017)"
+   else "Helena 0.8.3 M - December 2017"
 
 let kernel = ref V3          (* kernel type *)
 
@@ -51,12 +53,14 @@ let first = ref 0            (* begin trace here *)
 
 let last = ref max_int       (* end trace here *) 
 
-let extended = ref false     (* extended applications *) 
+let restricted = ref true    (* restricted applications *) 
 
 let infinity = ref false     (* use ∞-abstractions in contexts *) 
 
 let short = ref false        (* short global constants *) 
 
+let cast = ref false         (* anticipate cast *)
+
 let root = ref ""            (* initial segment of URI hierarchy *)
 
 let trace = ref 0            (* trace level *)
@@ -116,8 +120,8 @@ let kernel_id () =
       | V0 -> "Environment_V0"
    in
    let si = if !si then "_si" else "" in
-   let ext = if !extended then "_x" else "" in
-   id ^ si ^ ext
+   let rest = if !restricted then "" else "_x" in
+   id ^ si ^ rest
 
 let get_baseuri () =
    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
@@ -133,7 +137,7 @@ END
 
 let clear () =
    root := ""; first := 0; last := max_int;
-   kernel := V3; si := false; extended := false; infinity := false; cover := ""; 
+   kernel := V3; si := false; restricted := true; infinity := false; cast := false; cover := ""; 
    indexes := false; short := false; trace := 0;
    IFDEF LEXER THEN debug_lexer := false ELSE () END;
    IFDEF PARSER THEN debug_parser := false ELSE () END;