]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/top.ml
some renaming and some interfaces improved
[helm.git] / helm / software / lambda-delta / toplevel / top.ml
index 46907866834547ca38cf520b1a93cfbec60cdd3c..13887c6ef28e508258220d9e90687e974b6a590b 100644 (file)
@@ -25,10 +25,11 @@ module MBrg = MetaBrg
 module G    = Library
 module BrgO = BrgOutput
 module BrgR = BrgReduction
+module BrgT = BrgType
 module BrgU = BrgUntrusted
 module MBag = MetaBag
 module BagO = BagOutput
-module BagR = BagReduction
+module BagT = BagType
 module BagU = BagUntrusted
 
 type status = {
@@ -58,7 +59,7 @@ let bag_error s msg =
    L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush () 
 
 let brg_error s msg =
-   L.error BrgO.specs (L.Warn s :: L.Loc :: msg); flush () 
+   L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush () 
 
 let process_item f st =
    let f ast = f {st with ast = ast} in
@@ -106,7 +107,7 @@ let type_check f st si g k =
 
 let main =
 try 
-   let version_string = "Helena 0.8.0 M - August 2009" in
+   let version_string = "Helena 0.8.0 M - September 2009" in
    let stage = ref 3 in
    let moch = ref None in
    let meta = ref false in
@@ -238,5 +239,5 @@ try
       ("-s", Arg.Int set_stage, help_s);
       ("-x", Arg.Set export, help_x)
    ] read_file help;
-with BagR.TypeError msg -> bag_error "Type Error" msg
-   | BrgR.TypeError msg -> brg_error "Type Error" msg
+with BagT.TypeError msg -> bag_error "Type Error" msg
+   | BrgT.TypeError msg -> brg_error "Type Error" msg