drg->brg translation contibued (still bugged though)

[helm.git] / helm / software / lambda-delta / toplevel / top.ml

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 3558dc8d00540d064c6bc3f0046ab59501e9e3d0..6e6ccfc288e34b0838232020c82574c32babe7f4 100644 (file)
--- 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