X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;h=aad48387ebd1cda137b28399810e8ef9f6fc6016;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=b47d00725a9f056434c4523981ceb5adb4355a60;hpb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;p=helm.git

diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml
index b47d00725..aad48387e 100644
--- a/helm/software/lambda-delta/src/toplevel/top.ml
+++ b/helm/software/lambda-delta/src/toplevel/top.ml
@@ -31,6 +31,7 @@ module BD = BrgCrg
 module BO = BrgOutput
 module BR = BrgReduction
 module BU = BrgUntrusted
+module ZD = BagCrg
 module ZO = BagOutput
 module ZT = BagType
 module ZU = BagUntrusted
@@ -85,6 +86,8 @@ let print_counters st = function
 let xlate_entity entity = match !G.kernel, entity with
    | G.Brg, CrgEntity e -> 
       let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
+   | G.Bag, CrgEntity e -> 
+      let f e = (BagEntity e) in E.xlate f ZD.bag_of_crg e
    | _, entity          -> entity
 
 let pp_progress e =
@@ -107,7 +110,7 @@ let count_entity st = function
 let export_entity = function
    | CrgEntity e -> XL.export_entity XD.export_term e
    | BrgEntity e -> XL.export_entity BO.export_term e
-   | BagEntity _ -> ()
+   | BagEntity e -> XL.export_entity ZO.export_term e
 
 let type_check st k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in