X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=3a394c5b7803191f47cddbafbdf98ac597b4147e;hb=9935a5bf5bdc98ad01a2b0234cf4e612a62c939f;hp=47ee342728631a9a4d6747900eab7c9556b6fa07;hpb=87e51ef39b7dc9eaeff2cf319038c8aaca1aeb91;p=helm.git

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 47ee34272..3a394c5b7 100644
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -9,13 +9,13 @@
      \ /   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 ******************************************************)
 
@@ -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 *)
 
@@ -55,25 +55,21 @@ let ma_preamble = ref ""     (* location of grafite preamble file *)
 
 let alpha = ref ""           (* prefix of numeric identifiers *)
 
-let kernel_id () = 
-   let id = match !kernel with
-      | Crg -> "crg"
-      | Brg -> "brg"
-      | Bag -> "bag"
-   in
-   let si = if !si then "_si" else "" in
-   id ^ si
+let kernel_id () = match !kernel with
+   | V4 -> ""
+   | V3 -> "V3"
+   | V0 -> "V0"
 
 let get_baseuri () =
    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
 
 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 := ""