]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/top.ml
new xml exportation procedure for basic_rg (10 times faster than previous). the stati...
[helm.git] / helm / software / lambda-delta / toplevel / top.ml
index 0c85bb0c5dab51560344bdc7b5189f578860a460..6f7d60e9ca93d35051916c2442bb46bf3424f851 100644 (file)
@@ -115,7 +115,7 @@ let count_entity st = function
 
 let export_entity si g moch = function
    | DrgEntity e  -> X.export_entity DO.export_term si g e
-   | BrgEntity e  -> X.old_export_entity BrgO.export_term si g e
+   | BrgEntity e  -> X.export_entity BrgO.export_term si g e
    | MetaEntity e ->
       begin match moch with
          | None     -> ()