X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgEnvironment.ml;h=01a38f89ffeffa52e296b023b3816d083f0389f0;hb=2e97c767bc072f5ba238725ff1f738fc91a0135a;hp=0fbbd9a543072748d7968d4fc034cb88cdccd703;hpb=34e6104ef149e3776d0ab7f0930ae73f0e8de157;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml
index 0fbbd9a54..01a38f89f 100644
--- a/helm/software/helena/src/basic_rg/brgEnvironment.ml
+++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml
@@ -11,6 +11,7 @@
 
 module U  = NUri
 module UH = U.UriHash
+module G  = Options
 module E  = Entity
 
 let hsize = 7000 
@@ -20,8 +21,14 @@ let env = UH.create hsize
 
 (* decps *)
 let set_entity entity =
+IFDEF EXPAND THEN
+   let ra, na, uri, b = entity in
+   let entity0 = if !G.expand then ra, E.node_attrs ~apix:0 (), uri, b else entity in
+   UH.add env uri entity0; entity
+ELSE
    let _, _, uri, _ = entity in
    UH.add env uri entity; entity
+END
 
 let get_entity uri =
    try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void