λδ site update

[helm.git] / helm / software / helena / src / toplevel / helena.ml

diff --git a/helm/software/helena/src/toplevel/helena.ml b/helm/software/helena/src/toplevel/helena.ml
index 1070dd9150748ca75c6456112ace31b3cd46d558..10c9f0f7f148d09c62f00fefc0cc1123f4b1454f 100644 (file)
--- a/helm/software/helena/src/toplevel/helena.ml
+++ b/helm/software/helena/src/toplevel/helena.ml
@@ -40,7 +40,7 @@ module BU = BrgUntrusted
 module BM = BrgMatita
 module BQ = BrgCoq
 module BH = BrgHelena
-(* module BC = BrgCC *)
+module BP = BrgPTS
 module BY = BrgLYP
 module ZD = BagCrg
 module ZO = BagOutput
@@ -386,16 +386,14 @@ END
 
 IFDEF MANAGER THEN
 
-let set_manager s = match KS.lowercase s with
+let set_manager s = match KS.lowercase_ascii s with
    | "v8"  -> G.manager := G.Coq
    | "ma2" -> G.manager := G.Matita
    | "lp1" -> G.manager := G.LP1
    | "lp2" -> G.manager := G.LP2
    | "tj2" -> G.manager := G.TJ2
    | "tj3" -> G.manager := G.TJ3
-(*
-   | "cc0" -> G.manager := G.CC0
-*)
+   | "pts" -> G.manager := G.PTS
    | "lyp" -> G.manager := G.LYP
    | s     -> L.warn level (KP.sprintf "Unknown manager: %s" s)
 
@@ -492,9 +490,7 @@ IFDEF MANAGER THEN
          | G.LP2    -> st := {!st with mst = Some (BH.open_out_lp2 base_name)}
          | G.TJ2    -> st := {!st with mst = Some (BH.open_out_tj2 base_name)}
          | G.TJ3    -> st := {!st with mst = Some (BH.open_out_tj3 base_name)}
-(*
-         | G.CC0    -> st := {!st with mst = Some (BC.open_out_cc0 base_name)}
-*)
+         | G.PTS    -> st := {!st with mst = Some (BP.open_out_pts2 base_name)}
          | G.LYP    -> st := {!st with mst = Some (BY.open_out_lyp2 base_name)}
          | G.Quiet  -> ()
       end
@@ -530,7 +526,7 @@ ELSE () END
       "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
       "              7 level disambiguation\n\n" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^
-      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"lyp\" (lambda-Prolog)\n" 
+      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"pts\" \"lyp\" (lambda-Prolog)\n" 
    in
    let help_L = "         [lexer]     Show lexer debug information" in 
    let help_M = "<dir>    [manager]   Set location of output directory (manager) to <dir> (default: current directory)" in