X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=227a524e2036ca126238288d7e061b7f4bd1c649;hb=68b5af5ca8f1e7f98485b92692b3dcb1ae240d19;hp=a7b5f4dd599738f584ee35ca512331f2beb27e7b;hpb=3e5683b1efeb08431c8bb34718920384bfe6625a;p=helm.git diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index a7b5f4dd5..227a524e2 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -9,17 +9,17 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Filename +module KF = Filename module C = Cps type uri_generator = string -> string -type kernel = Crg | Brg | Bag +type kernel = V4 | V3 | V0 (* interface functions ******************************************************) -let version_string = "Helena 0.8.2 M - November 2014" +let version_string = "Helena 0.8.2 M - December 2014" let stage = ref 3 (* stage *) @@ -29,7 +29,7 @@ let summary = ref false (* log summary information *) let xdir = ref "" (* directory for XML output *) -let kernel = ref Brg (* kernel type *) +let kernel = ref V3 (* kernel type *) let si = ref false (* use sort inclusion *) @@ -57,9 +57,9 @@ let alpha = ref "" (* prefix of numeric identifiers *) let kernel_id () = let id = match !kernel with - | Crg -> "crg" - | Brg -> "brg" - | Bag -> "bag" + | V4 -> "Environment" + | V3 -> "Environment_V3" + | V0 -> "Environment_V0" in let si = if !si then "_si" else "" in id ^ si @@ -69,11 +69,11 @@ let get_baseuri () = let get_mk_uri () = let bu = get_baseuri () in - fun s -> F.concat bu (s ^ ".ld") + fun s -> KF.concat bu (s ^ ".ld") let clear () = stage := 3; trace := 0; summary := false; - xdir := ""; kernel := Brg; si := false; cover := ""; + xdir := ""; kernel := V3; si := false; cover := ""; expand := false; indexes := false; icm := 0; unquote := false; debug_parser := false; debug_lexer := false; ma_dir := ""; ma_preamble := ""