X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=71e55ececb796ea00dbfe30c05d5b51a696ee5e4;hp=f268ba3443a138bd3decc13f1c217b70a969ba6d;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hpb=fdb80b08af83b86759833142456ce3c4f84cd80e

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index f268ba344..71e55ecec 100644
--- 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;