]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/options.ml
lddl update with the disambiguated "grundlagen"
[helm.git] / helm / software / helena / src / common / options.ml
index 3a394c5b7803191f47cddbafbdf98ac597b4147e..227a524e2036ca126238288d7e061b7f4bd1c649 100644 (file)
@@ -55,10 +55,14 @@ let ma_preamble = ref ""     (* location of grafite preamble file *)
 
 let alpha = ref ""           (* prefix of numeric identifiers *)
 
-let kernel_id () = match !kernel with
-   | V4 -> ""
-   | V3 -> "V3"
-   | V0 -> "V0"
+let kernel_id () = 
+   let id = match !kernel with
+      | V4 -> "Environment"
+      | V3 -> "Environment_V3"
+      | V0 -> "Environment_V0"
+   in
+   let si = if !si then "_si" else "" in
+   id ^ si
 
 let get_baseuri () =
    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]