X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=6e6ccfc288e34b0838232020c82574c32babe7f4;hb=be1700416b160f793c0368a39600b7f81bfb2e44;hp=3558dc8d00540d064c6bc3f0046ab59501e9e3d0;hpb=e3fc33cab9b7736c6475cf2c9cd7f91c5a4bd7f9;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 3558dc8d0..6e6ccfc28 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -24,7 +24,8 @@ module DA   = DrgAut
 module MA   = MetaAut
 module MO   = MetaOutput
 module ML   = MetaLibrary
-module DrgO = DrgOutput
+module DO   = DrgOutput
+module DBrg = DrgBrg
 module MBrg = MetaBrg
 module BrgO = BrgOutput
 module BrgR = BrgReduction
@@ -85,6 +86,8 @@ let print_counters st = match !kernel with
    | Bag -> BagO.print_counters C.start st.bagc
 
 let xlate f st entity = match !kernel, entity with
+   | Brg, DrgEntity e  -> 
+      let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_drg e
    | Brg, MetaEntity e -> 
       let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
    | Bag, MetaEntity e -> 
@@ -98,7 +101,7 @@ let count_entity st = function
    | _            -> st
 
 let export_entity si g moch = function
-   | DrgEntity e  -> X.export_entity DrgO.export_term si g e
+   | DrgEntity e  -> X.export_entity DO.export_term si g e
    | BrgEntity e  -> X.old_export_entity BrgO.export_term si g e
    | MetaEntity e ->
       begin match moch with