X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=cdf88c308df83927b8309dc7c227a44f5d6689bf;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=dc63b1ca642a14265523ac2bd9ac9363e77d215d;hpb=849001febdebe045a1309e6c2c854e421e6e476b;p=helm.git

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index dc63b1ca6..cdf88c308 100644
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -22,18 +22,22 @@ 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 (June 2015)"
-   else "Helena 0.8.3 M - June 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 +55,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 *)
@@ -101,7 +107,7 @@ let preprocess = ref false   (* preprocess source *)
 END
 
 IFDEF QUOTE THEN
-let quote = ref false      (* quote identifiers when lexing *)
+let quote = ref false        (* quote identifiers when lexing *)
 END
 
 IFDEF TYPE THEN
@@ -116,8 +122,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 +139,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;